The law of excluded middle (tertium non datur: no third is given) states that for any proposition P, either P is true or its negation ¬P is true — there is no middle ground. In classical logic, this is an axiom: every proposition is either true or false, and no other status is possible. It underwrites proof by contradiction (to prove P, assume ¬P and derive a contradiction) and the classical treatment of disjunction (A ∨ ¬A is always true).
Mathematical constructivism and intuitionistic logic reject this principle for infinite domains. L. E. J. Brouwer argued that to assert P ∨ ¬P is to claim that one possesses either a proof of P or a proof of ¬P — but for many mathematical propositions (e.g., whether a particular infinite decimal expansion contains a certain digit), neither proof is available. The law of excluded middle, applied indiscriminately, asserts the existence of knowledge that has not been constructed. Intuitionistic logic replaces it with a constructive interpretation of disjunction: A ∨ B is provable only when A is provable or B is provable (and we know which).
The rejection of the law of excluded middle produces a weaker but more nuanced logic. In classical logic, double negation elimination holds (¬¬P implies P); in intuitionistic logic, it does not — knowing that the denial of P leads to contradiction does not provide a construction of P. This distinction matters when logic is interpreted computationally: under the Curry-Howard correspondence, an intuitionistic proof of P is a program that computes a witness for P, and there is no general program that transforms the absence of a counterexample into the presence of an example.
For this research program, the rejection of the law of excluded middle is not a technical restriction but a philosophical commitment. The semiotic universe is built on Heyting algebras (the algebraic semantics of intuitionistic logic) rather than Boolean algebras (the algebraic semantics of classical logic) because meaning is not binary. A sign is not simply “meaningful” or “meaningless,” true or false — it occupies a position in a lattice of semantic values, and that position is achieved through constructive interpretive processes (the closure operators), not given in advance by a law that partitions everything into one of two categories.
Related terms
- Mathematical constructivism — the philosophy that rejects excluded middle
- L. E. J. Brouwer — who first rejected it for mathematics
- Arend Heyting — who formalized the logic without it
- Relational ontology — the broader rejection of binary partitions