excluded middle



In logic, the principle of excluded middle states that every truth value is either true or false. (This is sometimes called the ‘axiom’ or ‘law’ of excluded middle, either to emphasise that it is or is not optional; ‘principle’ is a relatively neutral term.) One of the many meanings of classical logic is to emphasise that this principle holds in the logic; in contrast, it fails in intuitionistic logic.

The principle of excluded middle (hereafter, PEM), as a statement about truth values themselves, is accepted by nearly all mathematicians; those who doubt or deny it are a distinct minority, the constructivists. However, when one internalises mathematics in categories other than the category of sets, there is no doubt, though, that excluded middle often fails internally. See the examples listed at internal logic. (Those categories in which excluded middle holds are called Boolean; in general, the adjective ‘Boolean’ is often used to indicate the applicability of PEM.)

Although the term ‘excluded middle’ (sometimes even excluded third) suggests that the principle does not apply in many-valued logics, that is not the point; many-valued logics are many-valued externally but may still be two-valued internally. In the language of categorial logic, whether a category has exactly two subterminal objects is in general independent of whether it is Boolean; instead, the category is Boolean iff the statement that it has exactly two subterminal objects holds in its internal logic (which is in general independent of whether that statement is true).

In fact, intuitionistic logic proves that there is no truth value that is neither true nor false; in this sense, the possibility of a ‘middle’ or ‘third’ truth value is still ‘excluded’. But since the relevant de Morgan law fails in intuitionistic logic, we may not conclude that every truth value is either true or false, which is the actual PEM.

PEM versus AC

Excluded middle can be seen as a very weak form of the axiom of choice (a slightly more controversial principle, doubted or denied by a slightly larger minority, and true internally in even fewer categories). In fact, the following are equivalent.

  1. The principle of excluded middle.
  2. Finitely indexed sets are projective (in fact, it suffices 2-indexed sets to be projective).
  3. Finite sets are choice (in fact, it suffices for 2 to be choice).

(Here, a set AA is finite or finitely-indexed (respectively) if, for some natural number nn, there is a bijection or surjection (respectively) {0,,n1}A\{0, \ldots, n - 1\} \to A.)

The proof is as follows. If pp is a truth value, then divide {0,1}\{0,1\} by the equivalence relation where 010 \equiv 1 iff pp holds. Then we have a surjection 2A2\to A, whose domain is 22 (and in particular, finite), and whose codomain AA is finitely-indexed. But this surjection splits iff pp is true or false, so if either 22 is choice or 22-indexed sets are projective, then PEM holds.

On the other hand, if PEM holds, then we can show by induction that if AA and BB are choice, so is ABA\sqcup B (add details). Thus, all finite sets are choice. Now if nAn\to A is a surjection, exhibiting AA as finitely indexed, it has a section AnA\to n. Since a finite set is always projective, and any retract of a projective object is projective, this shows that AA is projective.

In particular, the axiom of choice implies PEM. This argument, due originally to Diaconescu, can be internalized in any topos. However, other weak versions of choice such as countable choice (any surjection to a countable set (which for this purpose is any set isomorphic to the set of natural numbers) has a section), dependent choice, or even COSHEP do not imply PEM. In fact, it is often claimed that axiom of choice is true in constructive mathematics (by the BHK or Brouwer-Heyting-Kolmogorov interpretation of predicate logic), leading to much argument about exactly what that means.

Double-negated PEM

While PEM is not valid in constructive mathematics, its double negation

¬¬(A¬A) \neg\neg(A\vee \neg A)

is valid. Ony way to see this is to note that ¬(AB)=¬A¬B\neg (A\vee B) = \neg A \wedge \neg B is one of de Morgan's laws that is constructively valid, and ¬(¬A¬¬A)\neg (\neg A \wedge \neg\neg A) is easy to prove (it is an instance of the law of non-contradiction?).

However, a more direct argument makes the structure of the proof more clear. When beta-reduced, the proof term? is λx.x(inr(λa.x(inl(a))))\lambda x. x(inr(\lambda a. x(inl(a)))). This means that we first assume ¬(A¬A)\neg (A\vee \neg A) for a contradiction, for which it suffices (by assumption) to prove A¬AA\vee \neg A. We prove that by proving ¬A\neg A, which we prove by assuming AA for a contradiction. But now we can reach a contradiction by invoking (again) our assumption of ¬(A¬A)\neg (A\vee \neg A) and proving A¬AA\vee \neg A this time using our new assumption of AA. In other words, we start out claiming that ¬A\neg A, but whenever that “bluff gets called” by someone supplying an AA and asking us to yield a contradiction, we retroactively change our minds and claim that AA instead, using the AA that we were just given as evidence.

In particular, this shows how the double negation modality can be regarded computationally as a sort of continuation-passing transform.



In homotopy type theory

In homotopy type theory:

Revised on April 5, 2017 16:52:48 by Urs Schreiber (