Foundation·F08
Excluded middle
Every proposition is true or false: the classical assumption.
Built from disjunction and negation. This is the one axiom separating classical logic from intuitionistic logic.
In words
For every proposition A, either A holds or its negation holds; there is no third possibility.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
Everything before this point is intuitionistically acceptable; excluded middle is the genuinely classical step. Over the other rules it is equivalent to double negation elimination (
) and to Peirce's law. Intuitionists reject it, on the ground that asserting a disjunction should require knowing which side holds; classical mathematics, and ZFC with it, assumes it freely, and this wiki is classical throughout. It is what licenses proof by contradiction: to prove
, refute
. In Lean, Classical.em is not an axiom but a theorem, derived by Diaconescu's argument from choice (A09), propositional extensionality, and function extensionality.
Used by
Propose an edit4 published revisions
- 7/12/2026 · Benjamin· Split into A, the or symbol, and its negation individually instead of one combined chunk.what changed →
- 7/12/2026 · Benjamin· Add word-notation highlight markup linking the disjunction and its universal scope to the In words reading.what changed →
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Logic layer: connectives and quantifierswhat changed →