Law of Excluded Middle
The Law of Excluded Middle (LEM) is the logical principle that for any proposition P, either P or its negation is true: P ∨ ¬P. In classical logic, it is an axiom or theorem of every standard system. In intuitionistic logic, it is neither provable nor assumed — its status as a universal truth is precisely what separates constructive from classical mathematics.
The law has a seductive simplicity. Every proposition is either true or false; there is no middle ground. But this simplicity conceals a hidden assumption: that propositions have truth values independently of anyone's ability to determine them. That hidden assumption is a philosophical commitment, not a logical necessity, and it is one of the most contested commitments in all of the philosophy of mathematics.
Classical and Constructive Interpretations
In classical logic, LEM is uncontroversial: it follows from model-theoretic semantics in which the truth values {true, false} form the only possible assignment. A proposition is true if and only if it is satisfied in every model. Under these semantics, P ∨ ¬P is valid for exactly the same reason that a coin lands heads or tails — there are only two outcomes, and one must obtain.
In intuitionistic logic, the picture changes because truth is not satisfaction-in-a-model but provability. Under the Brouwer-Heyting-Kolmogorov interpretation, a proof of P ∨ ¬P requires either a proof of P or a proof that P is refutable. For propositions about infinite mathematical structures — whether every even number greater than 2 is the sum of two primes (Goldbach's conjecture), whether the Riemann hypothesis holds — we currently have neither. LEM, applied to these propositions, asserts a fact we have no right to assert.
L.E.J. Brouwer was explicit about this: LEM may be a property of finite domains (where we can in principle check every case) but cannot be assumed as a universal principle of mathematics. His rejection of LEM was not skepticism about truth — it was a demand for intellectual honesty about what we know versus what we assume.
The Stakes: What Follows From LEM?
LEM is not merely a logical technicality. It licenses entire classes of proof strategy:
- Non-constructive existence proofs: You can prove that a solution exists by showing that its non-existence leads to contradiction — without producing the solution. The Axiom of Choice is the most powerful classical tool of this kind: it asserts the existence of a selection function over any collection of non-empty sets, without specifying how the selection is made.
- Proof by contradiction in its full classical form: To prove P, assume ¬P and derive a contradiction. In intuitionistic logic, this gives you ¬¬P — which is strictly weaker than P.
- Decidability assumptions: Classical number theory assumes every arithmetic statement is either true or false. Gödel's incompleteness theorems showed that provability diverges from truth: there are true arithmetic statements that are unprovable. LEM insists these statements are still true — they just cannot be verified. Constructivists question whether this notion of truth is coherent.
The Categorical View: LEM as a Special Case
In topos theory, classical logic is the internal logic of a topos with a two-valued subobject classifier — a topos where every proposition is either true or false in a specific technical sense. Intuitionistic logic is the internal logic of any topos. This means classical logic is a special case of intuitionistic logic, not its rival.
LEM corresponds to the assumption that the topos is Boolean — that the subobject classifier is complemented. In a general topos, this need not hold. What this reveals: the choice between accepting and rejecting LEM is not a choice between two philosophies of truth. It is a choice of which mathematical universe you are working in. Different universes validate different logical principles, and there is no universe-independent standpoint from which to declare one the correct logic.
The law of excluded middle is not a law about reality. It is a law about the expressive poverty of a logic that cannot tolerate uncertainty. When mathematics abandoned the requirement that existence means construction, it gained power and lost accountability. Whether that trade was worth it remains genuinely open.