excluded middle in nLab

Contents

Contents

Idea

In logic, the principle of excluded middle states that every truth value is either true or false (Aristotle, MP1011b24). (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 (classical mathematics); 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 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.

In set theory

In material set theory, Shulman 18 makes the distinction between full classical logic, where the principle of excluded middle holds for all logical formulae in the material set theory, and Δ 0\Delta_0-classical logic, where the principle of excluded middle holds for only holds for Δ 0\Delta_0-formulae. Δ 0\Delta_0-formulae are logical formulae where every quantifier QQ has to be bounded by the membership relation; i.e. Qx∈y.P(x)≔Qx.x∈y∧P(x)Q x \in y.P(x) \coloneqq Q x.x \in y \wedge P(x). In structural set theory, the above difference between full classical logic and Δ 0\Delta_0-classical logic in material set theory is the difference between defining structural set theory as a well-pointed Boolean topos in classical logic and in intuitionistic logic respectively.

In type theory

In dependent type theory, there are many statements of excluded middle.

Truncated excluded middle

The statement which directly corresponds to excluded middle in logic states that given a type PP, if PP is a mere proposition, then either PP or the negation of PP holds

Γ⊢PtypeΓ⊢lem P:isProp(P)→(P∨¬P)\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to (P \vee \neg P)}

where isProp\mathrm{isProp} is the isProp modality commonly defined as ∏ x:P∏ y:PId P(x,y)\prod_{x:P} \prod_{y:P} \mathrm{Id}_P(x, y), negation ¬P\neg P is simply the the function type P→𝟘P \to \mathbb{0} into the empty type and disjunction A∨BA \vee B is the bracket type of the sum type [A+B][A + B].

If one additionally has a Russell type of all propositions Ω\Omega or a Tarski type of all propositions (Ω,El Ω)(\Omega, \mathrm{El}_\Omega), the law of truncated excluded middle could be expressed as an axiom:

ΓctxΓ⊢doubleneg:∏ P:ΩP∨¬PRussellΓctxΓ⊢doubleneg:∏ P:ΩEl Ω(P)∨¬El Ω(P)Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} P \vee \neg P}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} \mathrm{El}_\Omega(P) \vee \neg \mathrm{El}_\Omega(P)}\mathrm{Tarski}

If the type theory has a boolean domain Bit\mathrm{Bit} which is a univalent Tarski universe with type family El Bit\mathrm{El}_\mathrm{Bit} and thus satisfies the extensionality principle, truncated excluded middle could be stated as given a type PP, if PP is a mere proposition, then there exists a boolean QQ such that PP is equivalent to the type reflection of QQ:

Γ⊢PtypeΓ⊢lem P:isProp(P)→∃Q:Bit.P≃El Bit(Q)\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to \exists Q:\mathrm{Bit}.P \simeq \mathrm{El}_\mathrm{Bit}(Q)}

By definition, the only two booleans are 00 representing false and 11 representing true.

Untruncated excluded middle

There is also an untruncated version of excluded middle, which uses the sum type instead of the disjunciton:

Γ⊢PtypeΓ⊢lem P:isProp(P)→(P+¬P)\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to (P + \neg P)}

In the untruncated case, the requirement that PP be an h-proposition is necessary; the untruncated law of excluded middle for h-sets is the set-theoretic choice operator, which implies the set-theoretic axiom of choice in addition to excluded middle, and the untruncated law of excluded middle for general types is the type-theoretic choice operator, which implies UIP in addition to the set-theoretic axiom of choice and excluded middle.

If one additionally has a Russell type of all propositions Ω\Omega or a Tarski type of all propositions (Ω,El Ω)(\Omega, \mathrm{El}_\Omega), the law of untruncated excluded middle could be expressed as an axiom:

ΓctxΓ⊢doubleneg:∏ P:ΩP+¬PRussellΓctxΓ⊢doubleneg:∏ P:ΩEl Ω(P)+¬El Ω(P)Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} P + \neg P}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} \mathrm{El}_\Omega(P) + \neg \mathrm{El}_\Omega(P)}\mathrm{Tarski}

Similarly as above, if the type theory has a boolean domain Bit\mathrm{Bit} which is a univalent Tarski universe with type family El Bit\mathrm{El}_\mathrm{Bit} and thus satisfies the extensionality principle, there is also an untruncated version of excluded middle using the boolean domain and dependent sum types:

Γ⊢PtypeΓ⊢lem P:isProp(P)→∑ Q:BitP≃El Bit(Q)\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to \sum_{Q:\mathrm{Bit}} P \simeq \mathrm{El}_\mathrm{Bit}(Q)}

By definition, the only two booleans are 00 representing false and 11 representing true.

Contractible excluded middle

There is also a version of excluded middle, which uses contractibility instead of pointedness to express truth:

Γ⊢AtypeΓ⊢lem A:isProp(A)→isContr(A+¬A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_A:\mathrm{isProp}(A) \to \mathrm{isContr}(A + \neg A)}

In dependent type theory as foundations of mathematics, the requirement that AA be an h-proposition is also necessary. This alternate law of untruncated excluded middle for general types implies that every type is a h-proposition a la propositional logic as a dependent type theory, because the only types PP such that P+¬PP + \neg P is equivalent to the unit type are the empty type and the unit type, which are h-propositions:

Γ⊢AtypeΓ⊢lem A:isContr(A+¬A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_A:\mathrm{isContr}(A + \neg A)}

If one additionally has a Russell type of all propositions Ω\Omega or a Tarski type of all propositions (Ω,El Ω)(\Omega, \mathrm{El}_\Omega), the law of excluded middle could be expressed as an axiom:

ΓctxΓ⊢doubleneg:∏ P:ΩisContr(P+¬P)RussellΓctxΓ⊢doubleneg:∏ P:ΩisContr(El Ω(P)+¬El Ω(P))Tarski\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} \mathrm{isContr}(P + \neg P)}\mathrm{Russell} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{doubleneg}:\prod_{P:\Omega} \mathrm{isContr}(\mathrm{El}_\Omega(P) + \neg \mathrm{El}_\Omega(P))}\mathrm{Tarski}

Similarly as above, if the type theory has a boolean domain Bit\mathrm{Bit} which is a univalent Tarski universe with type family El Bit\mathrm{El}_\mathrm{Bit} and thus satisfies the extensionality principle, there is also an contractible version of excluded middle using the boolean domain and dependent sum types:

Γ⊢PtypeΓ⊢lem P:isProp(P)→isContr(∑ Q:BitP≃El Bit(Q))\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to \mathrm{isContr}\left(\sum_{Q:\mathrm{Bit}} P \simeq \mathrm{El}_\mathrm{Bit}(Q)\right)}

or equivalently, using the boolean domain and the uniqueness quantifier:

Γ⊢PtypeΓ⊢lem P:isProp(P)→∃!Q:Bit.P≃El Bit(Q)\frac{\Gamma \vdash P \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_P:\mathrm{isProp}(P) \to \exists!Q:\mathrm{Bit}.P \simeq \mathrm{El}_\mathrm{Bit}(Q)}

By definition, the only two booleans are 00 representing false and 11 representing true.

Relations between the notions of excluded middle

Relation to the axiom of choice

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. (this is the Diaconescu-Goodman-Myhill theorem due to Diaconescu 75, see also McLarty 96, theorem 19.7, )

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,…,n−1}→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 0≡10 \equiv 1 iff pp holds. Then we have a surjection 2→A2\to A, whose domain is 22 (and in particular, finite), and whose codomain AA is 2-indexed (and thus 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 A⊔BA\sqcup B (add details). Thus, all finite sets are choice. Now if n→An\to A is a surjection, exhibiting AA as finitely indexed, it has a section A→nA\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.

While is often claimed that axiom of choice is true in constructive mathematics (by the BHK or Brouwer-Heyting-Kolmogorov interpretation of predicate logic), the BHK interpretation of the “axiom of choice” is simply the always true statement that indexed cartesian products distribute over indexed disjoint unions

(∏ x∈A⨄ y∈B(x){⊤|P(x,y)})→(⨄ g∈∏ x∈AB(x){⊤|P(x,g(x))})\left(\prod_{x \in A} \biguplus_{y \in B(x)} \{\top \vert P(x, y)\}\right) \to \left(\biguplus_{g \in \prod_{x \in A} B(x)} \{\top \vert P(x, g(x))\}\right)

or the always true statement that every split surjection splits.

Other equivalent statements

• Every set AA with a surjection from the boolean domain to AA is either a singleton or in bijection with the boolean domain.

• The set of equivalence relations on the boolean domain is in bijection with the boolean domain.

• Morgan Rogers showed here that the fact that the category of sets is a Boolean topos is equivalent to the fact that every pointed set is a free pointed set.

• compact spaces equivalently have converging subnets

• James Hanson showed here that every lower real number being a Dedekind real number is equivalent to LEM. Similarly, every upper real number being a Dedekind real number is equivalent to LEM.

• Every subcountable set is a countable set.

• The limited principle of omniscience holds for all subsingletons.

• Sets with decidable tight apartness relations form a cartesian closed category.

• Assuming function sets, every tight apartness relation on a set is decidable.

• The boolean domain 22 is a frame iff the category of sets is a Boolean topos. This implies that one can do topology (using topological spaces, locales, formal topologies, etc) directly using the boolean domain as the frame of open truth values.

• The poset of truth values has a tight apartness relation.

• The partial function classifier of any singleton is the boolean domain.

• Every ideal of a discrete Bézout unique factorization domain is a principal ideal.

Double-negated PEM

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

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

is valid. One way to see this is to note that ¬(A∨B)=¬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.

However, there is another meaning of “double negated PEM” that is not valid. The above argument shows that

∀A,¬¬(A∨¬A). \forall A, \neg\neg(A\vee \neg A).

But a stronger statement is

¬¬∀A,(A∨¬A). \neg\neg \forall A, (A \vee \neg A).

This is related to the above valid statement by a double-negation shift; and in fact, the truth of ¬¬∀A,(A∨¬A) \neg\neg \forall A, (A \vee \neg A) is equivalent to the principle of double-negation shift. In particular, it is not constructively provable.

Other variants of excluded middle

In intuitionistic logic, there are a number of logical operations on two propositions which are equivalent in classical logic to the disjunction of said propositions, but which are weaker in intuitionistic logic. Each of these weaker versions of disjunction can be applied to the law of excluded middle, some of which are equivalent to excluded middle and others which are automatically true. Here is a Hasse diagram of some of them, with the strongest statement at the bottom and the weakest at the top (so that each statement entails those above it):

¬(¬P∧¬¬P) ⇗ ⇖ ¬P→¬P P←¬¬P ⇖ ⇗ (¬P→¬P)∧(P←¬¬P) ⇑ P∨¬P \array { & & \neg(\neg{P} \wedge \neg{\neg{P}}) \\ & ⇗ & & ⇖ \\ \neg{P} \rightarrow \neg{P} & & & & P \leftarrow \neg{\neg{P}} \\ & ⇖ & & ⇗ \\ & & (\neg{P} \rightarrow \neg{P}) \wedge (P \leftarrow \neg{\neg{P}}) \\ & & \Uparrow \\ & & P \vee \neg{P} }

(A single arrow is implication in the object language; a double arrow is entailment in the metalanguage.) Note that the false statement ¬P∧¬¬P\neg{P} \wedge \neg{\neg{P}} is the negation of every item in this diagram.

• ¬(¬P∧¬¬P)\neg(\neg{P} \wedge \neg{\neg{P}}) and ¬P→¬P\neg{P} \rightarrow \neg{P} are always true in intuitionistic logic

• P←¬¬PP \leftarrow \neg{\neg{P}}, (¬P→¬P)∧(P←¬¬P)(\neg{P} \rightarrow \neg{P}) \wedge (P \leftarrow \neg{\neg{P}}), and P∨¬PP \vee \neg{P} are equivalent to excluded middle, since P←¬¬PP \leftarrow \neg{\neg{P}} is the double negation law, which is equivalent to excluded middle, and (¬P→¬P)∧(P←¬¬P)(\neg{P} \rightarrow \neg{P}) \wedge (P \leftarrow \neg{\neg{P}}) is the conjunction of the double negation law with an intuitionistically true statement.

Sharp excluded middle

One could add to cohesive homotopy type theory a version of excluded middle called the sharp law of excluded middle, given by the following rule:

Ξ|Γ⊢PtypeΞ|Γ⊢p:isProp(P)Ξ|Γ⊢lem ♯:♯(P∨¬P)\frac{\Xi \vert \Gamma \vdash P \; \mathrm{type} \quad \Xi \vert \Gamma \vdash p:\mathrm{isProp}(P)}{\Xi \vert \Gamma \vdash \mathrm{lem}^\sharp:\sharp(P \vee \neg P)}

where A∨B≔[A+B]A \vee B \coloneqq \left[A + B\right] and ¬A≔A→𝟘\neg A \coloneqq A \to \mathbb{0}, and ♯A\sharp A is the sharp modality of AA, [A]\left[A\right] is the propositional truncation of AA and 𝟘\mathbb{0} is the empty type.

• axiom of choice

• law of double negation

• ex falso quodlibet

• proof by contradiction

• De Morgan law

• Cantor-Schroeder-Bernstein theorem

References

General

• Colin McLarty, Elementary Categories, Elementary Toposes, Oxford University Press, 1996

• Mike Shulman, Comparing material and structural set theories, Annals of Pure and Applied Logic, Volume 170, Issue 4, April 2019, Pages 465-504 (doi:10.1016/j.apal.2018.11.002, arXiv:1808.05204)

Relation to other axioms:

Relation to the axiom of choice (Diaconescu-Goodman-Myhill theorem):

• Radu Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:176-178 (1975) (doi:10.1090/S0002-9939-1975-0373893-X)

• N. D. Goodman J. Myhill, Choice Implies Excluded Middle, Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 24:461 (1978)

Relation to ex falso quodlibet and the law of double negation:

• Pedro Francisco, Valencia Vizcaíno, Relations between ex falso, tertium non datur, and double negation elimination [arXiv:1304.0272]

In homotopy type theory

• Aristotle, Metaphysics, 1011b24: “Of any one subject, one thing must be either asserted or denied”

In homotopy type theory:

• Univalent Foundations Project, section 3.5 Homotopy Type Theory – Univalent Foundations of Mathematics

In cohesive homotopy type theory:

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)