3.4 Classical vs. intuitionistic logic

With the notion of mere proposition in hand, we can now give the proper formulation of the law of excluded middleMathworldPlanetmathPlanetmath in homotopy type theory:

𝖫𝖤𝖬:A:𝒰(𝗂𝗌𝖯𝗋𝗈𝗉(A)(A+¬A)). (3.4.1)

Similarly, the law of double negation is

A:𝒰(𝗂𝗌𝖯𝗋𝗈𝗉(A)(¬¬AA)). (3.4.2)

The two are also easily seen to be equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to each other—see http://planetmath.org/node/87834Exercise 3.18—so from now on we will generally speak only of 𝖫𝖤𝖬.

This formulation of 𝖫𝖤𝖬 avoids the “paradoxesMathworldPlanetmath” of Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1),Corollary 3.2.7 (http://planetmath.org/32propositionsastypes#Thmprecor1), since 𝟐 is not a mere proposition. In order to distinguish it from the more general propositions-as-types formulation, we rename the latter:


For emphasis, the proper version (3.4.1) may be denoted 𝖫𝖤𝖬-1; see also http://planetmath.org/node/87790Exercise 7.7. Although 𝖫𝖤𝖬 is not a consequence of the basic type theoryPlanetmathPlanetmath described in http://planetmath.org/node/87533Chapter 1, it may be consistently assumed as an axiom (unlike its -counterpart). For instance, we will assume it in §10.4 (http://planetmath.org/104classicalwellorderings).

However, it can be surprising how far we can get without using 𝖫𝖤𝖬. Quite often, a simple reformulation of a definition or theorem enables us to avoid invoking excluded middle. While this takes a little getting used to sometimes, it is often worth the hassle, resulting in more elegant and more general proofs. We discussed some of the benefits of this in the introduction.

For instance, in classical mathematics, double negations are frequently used unnecessarily. A very simple example is the common assumptionPlanetmathPlanetmath that a set A is “nonempty”, which literally means it is not the case that A contains no elements. Almost always what is really meant is the positive assertion that A does contain at least one element, and by removing the double negation we make the statement less dependent on 𝖫𝖤𝖬. Recall that we say that a type A is inhabited when we assert A itself as a propositionPlanetmathPlanetmath (i.e. we construct an element of A, usually unnamed). Thus, often when translating a classical proof into constructive logic, we replace the word “nonempty” by “inhabited” (although sometimes we must replace it instead by “merely inhabited”; see §3.7 (http://planetmath.org/37propositionaltruncation)).

Similarly, it is not uncommon in classical mathematics to find unnecessary proofs by contradictionMathworldPlanetmathPlanetmath. Of course, the classical form of proof by contradiction proceeds by way of the law of double negation: we assume ¬A and derive a contradictionMathworldPlanetmathPlanetmath, thereby deducing ¬¬A, and thus by double negation we obtain A. However, often the derivation of a contradiction from ¬A can be rephrased slightly so as to yield a direct proof of A, avoiding the need for 𝖫𝖤𝖬.

It is also important to note that if the goal is to prove a negationMathworldPlanetmath, then “proof by contradiction” does not involve 𝖫𝖤𝖬. In fact, since ¬A is by definition the type A𝟎, by definition to prove ¬A is to prove a contradiction (𝟎) under the assumption of A. Similarly, the law of double negation does hold for negated propositions: ¬¬¬A¬A. With practice, one learns to distinguish more carefully between negated and non-negated propositions and to notice when 𝖫𝖤𝖬 is being used and when it is not.

Thus, contrary to how it may appear on the surface, doing mathematics “constructively” does not usually involve giving up important theorems, but rather finding the best way to state the definitions so as to make the important theorems constructively provable. That is, we may freely use the 𝖫𝖤𝖬 when first investigating a subject, but once that subject is better understood, we can hope to refine its definitions and proofs so as to avoid that axiom. This sort of observation is even more pronounced in homotopy type theory, where the powerful tools of univalence and higher inductive types allow us to constructively attack many problems that traditionally would require classical reasoning. We will see several examples of this in http://planetmath.org/node/87879Part II.

It is also worth mentioning that even in constructive mathematics, the law of excluded middle can hold for some propositions. The name traditionally given to such propositions is decidable.

Definition 3.4.3.

  1. 1.

    A type A is called decidable if A+¬A.

  2. 2.

    Similarly, a type family B:A𝒰 is decidable if (a:A)(B(a)+¬B(a)).

  3. 3.

    In particular, A has decidable equality if (a,b:A)((a=b)+¬(a=b)).

Thus, 𝖫𝖤𝖬 is exactly the statement that all mere propositions are decidable, and hence so are all families of mere propositions. In particular, 𝖫𝖤𝖬 implies that all sets (in the sense of §3.1 (http://planetmath.org/31setsandntypes)) have decidable equality. Having decidable equality in this sense is very strong; see Theorem 7.2.5 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm3).

Title 3.4 Classical vs. intuitionistic logicMathworldPlanetmath