Law of Excluded Middle

The law of excluded middle is a principle of logic asserting that, for any proposition $P$, the disjunction $P\lor\neg P$ holds: either $P$ or its negation. It is valid in classical logic, but is not accepted as an unrestricted principle in intuitionistic logic. The law concerns a proposition and its precise negation, not any arbitrary pair of opposing alternatives. Its acceptance does not mean that the truth of every proposition can be discovered or computed. (docs.lean-lang.org)

Formal statement and classical interpretation

In propositional logic, excluded middle is written

Here $\lor$ denotes inclusive disjunction and $\neg$ denotes negation. More precisely, the expression is a schema: substituting any formula for $P$ gives an instance of the principle. Depending on the chosen deductive system, these instances may be introduced as axioms or derived as theorems. The schema also applies to formulas containing quantifiers in classical first-order logic. (builds.openlogicproject.org)

Under classical semantics, every proposition receives one of two truth values. Negation reverses that value, while a disjunction is true whenever at least one disjunct is true. Consequently, excluded middle is a tautology, as shown by its truth table: (builds.openlogicproject.org)

This establishes its validity in classical semantics, independently of the subject matter of $P$. It does not establish either disjunct separately: a proof of the disjunction need not determine whether $P$ holds. (builds.openlogicproject.org)

Historical background

An influential ancient formulation appears in Aristotle’s Metaphysics, Book IV, chapter 7. Aristotle argues that there is no intermediate between contradictory assertions: an attribute must be affirmed or denied of a subject. His discussion distinguishes contradiction from contrariety. Black and white, for example, can have intermediate colors; being white and not being white are contradictory alternatives rather than contrary extremes. (classics.mit.edu)

The traditional Latin expression tertium non datur means that no third alternative is given. In modern logic, the principle is formulated using connectives and explicit deductive rules, rather than solely through the language of attributes and their opposites. This formalization makes it possible to compare systems that validate excluded middle with systems that do not. (plato.stanford.edu)

Distinction from related principles

Excluded middle should be distinguished from the principle of bivalence, which says that every proposition has exactly one of the truth values true and false. Bivalence is a claim about truth-value assignments; excluded middle is a formula involving negation and disjunction. They are closely connected under classical interpretations, but need not coincide under other interpretations. For example, supervaluationist semantics can preserve excluded-middle formulas while allowing some propositions to lack a determinate truth value. (plato.stanford.edu)

The law of noncontradiction is instead expressed as

It rules out a proposition holding together with its negation. Excluded middle requires their disjunction to hold. Intuitionistic logic validates noncontradiction without validating unrestricted excluded middle, demonstrating that accepting one need not require accepting the other. (plato.stanford.edu)

Nor does excluded middle justify a false dilemma. “This object is red or blue” is not an instance unless “blue” genuinely expresses “not red” in the relevant domain. Aristotle’s distinction between contradictories and contraries already addresses this difference. (classics.mit.edu)

Role in mathematical proof

Excluded middle supports mathematical proofs by exhaustive case analysis. To establish $Q$, one may show that $P$ implies $Q$ and that $\neg P$ implies $Q$, then use $P\lor\neg P$. In natural deduction, the final step is disjunction elimination. Case analysis itself is available intuitionistically; the specifically classical step is supplying an arbitrary excluded-middle disjunction without further justification. (leanprover.github.io)

Over intuitionistic logic, unrestricted excluded middle is equivalent to double-negation elimination,

Assume excluded middle and $\neg\neg P$. The $P$ case immediately yields $P$; the $\neg P$ case gives a contradiction, from which intuitionistic logic permits $P$. Conversely, intuitionistic reasoning proves $\neg\neg(P\lor\neg P)$, and double-negation elimination yields excluded middle. (docs.lean-lang.org)

This explains its connection with classical proof by contradiction: deriving a contradiction from $\neg P$ establishes $\neg\neg P$, and concluding $P$ requires the classical step. By contrast, deriving a contradiction from $P$ to prove $\neg P$ is intuitionistically legitimate. (lipn.fr)

Constructive interpretation and computation

Under the Brouwer–Heyting–Kolmogorov interpretation, a proof of a disjunction provides a proof of one disjunct and identifies which one. Unrestricted excluded middle would therefore require a general justification for choosing between every proposition and its negation. Intuitionistic logic does not supply such a justification. Nevertheless, it accepts particular instances when the proposition is decidable, such as whether a specified natural number is prime. (plato.stanford.edu)

Failure to prove unrestricted excluded middle is not equivalent to proving its negation. Its double negation is intuitionistically provable. The distinction concerns what a proof must provide, rather than merely whether an observer currently knows the answer. (lipn.fr)

In proof assistants, classical principles can be made explicit. Lean supplies Classical.em P as a proof of $P ∨ ¬P$. Its documentation distinguishes constructive from classical reasoning: classical access to such a disjunction does not by itself provide an executable decision procedure for arbitrary propositions. (lean-lang.org)