Law of Excluded Middle

The principle that every proposition is either true or false, with no third possibility. In classical logic, it is expressed as P ∨ ¬P.

Propositional logic: A formal system for reasoning with propositions and logical connectives. This is the setting in which the principle is expressed as P ∨ ¬P.
Intuitionistic logic: A logic that treats truth as tied to proof and does not generally accept excluded middle. It rejects the law as a universal principle when no proof of either alternative is available.
Aristotle: An ancient Greek philosopher whose works shaped logic, metaphysics, and natural philosophy. His discussion of future contingents distinguishes excluded middle from the claim that every future event is already determined.
Decidability: The property of a problem for which an algorithm can always determine the correct answer in finite time. For a proposition with decidable truth, excluded middle can be established constructively.
Excluded middle: The logical disjunction of a proposition and its negation, written P ∨ ¬P. This formula directly states the principle for any proposition P.
Constructive mathematics: Mathematics that requires explicit constructions or proofs for existence claims and disjunctions. Its standards of proof often prevent asserting P ∨ ¬P without resolving which side holds.
Principle of noncontradiction: The principle that a proposition and its negation cannot both be true in the same respect. Aristotle treated it as a distinct foundational law, often discussed alongside excluded middle.
Curry–Howard correspondence: The correspondence between propositions and types, and between proofs and programs. Under this correspondence, a constructive proof of P ∨ ¬P requires a program deciding P.
Double negation elimination: The inference rule that permits deriving P from ¬¬P. In intuitionistic logic, accepting this rule is equivalent to accepting excluded middle.
Paraconsistent logic: A logic in which contradictions do not entail every proposition. Some paraconsistent systems also reject excluded middle, though that rejection is independent of tolerating contradictions.

Linked from 15 pages