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 middle in homotopy type theory:

$\mathsf{LEM}\;:\!\!\equiv\;\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{% \textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:% \mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}\Big{(}% \mathsf{isProp}(A)\to(A+\neg A)\Big{)}.$

(3.4.1)

Similarly, the law of double negation is

$\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A:\mathcal% {U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U% })}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}% }{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{% \prod_{(A:\mathcal{U})}}}\Big{(}\mathsf{isProp}(A)\to(\neg\neg A\to A)\Big{)}.$

(3.4.2)

The two are also easily seen to be equivalent to each other—see http://planetmath.org/node/87834Exercise 3.18—so from now on we will generally speak only of $\mathsf{LEM}$ .

This formulation of $\mathsf{LEM}$ avoids the “paradoxes” of Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1),Corollary 3.2.7 (http://planetmath.org/32propositionsastypes#Thmprecor1), since $\mathbf{2}$ is not a mere proposition. In order to distinguish it from the more general propositions-as-types formulation, we rename the latter:

$\mathsf{LEM}_{\infty}:\!\!\equiv\mathchoice{\prod_{A:\mathcal{U}}\,}{% \mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{% \prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{% \prod_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{% \prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}(A+% \neg A).$

For emphasis, the proper version (3.4.1) may be denoted $\mathsf{LEM}_{-1}$ ; see also http://planetmath.org/node/87790Exercise 7.7. Although $\mathsf{LEM}$ is not a consequence of the basic type theory described in http://planetmath.org/node/87533Chapter 1, it may be consistently assumed as an axiom (unlike its $\infty$ -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 $\mathsf{LEM}$ . 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 assumption 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 $\mathsf{LEM}$ . Recall that we say that a type $A$ is inhabited when we assert $A$ itself as a proposition (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 contradiction. Of course, the classical form of proof by contradiction proceeds by way of the law of double negation: we assume $\neg A$ and derive a contradiction, thereby deducing $\neg\neg A$ , and thus by double negation we obtain $A$ . However, often the derivation of a contradiction from $\neg A$ can be rephrased slightly so as to yield a direct proof of $A$ , avoiding the need for $\mathsf{LEM}$ .

It is also important to note that if the goal is to prove a negation, then “proof by contradiction” does not involve $\mathsf{LEM}$ . In fact, since $\neg A$ is by definition the type $A\to\mathbf{0}$ , by definition to prove $\neg A$ is to prove a contradiction ( $\mathbf{0}$ ) under the assumption of $A$ . Similarly, the law of double negation does hold for negated propositions: $\neg\neg\neg A\to\neg A$ . With practice, one learns to distinguish more carefully between negated and non-negated propositions and to notice when $\mathsf{LEM}$ 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 $\mathsf{LEM}$ 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.

A type $A$ is called decidable if $A+\neg A$ .
2.

Similarly, a type family $B:A\to\mathcal{U}$ is decidable if $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(B(a)+\neg B(a)).$
3.

In particular, $A$ has decidable equality if $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }((a=b)+\neg(a=b)).$

Thus, $\mathsf{LEM}$ is exactly the statement that all mere propositions are decidable, and hence so are all families of mere propositions. In particular, $\mathsf{LEM}$ 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 logic
\metatable