⁂ Concepts · Logic · No. 64
Excluded middle

Constructive proof: a proof that does not produce the thing does not do the job.

Excluded middle

The principle that every proposition is either true or false, with no third option - and the traditions that decline it.

Theme
Logic, language and interpretation
Tradition
Greek
Term fixed
c. 330 BC

In plain terms

Either it is raining or it is not. There is no third possibility, and the principle says that holds for every statement whatever.

It sounds as unassailable as non-contradiction and it is not. Take a heap of sand and remove grains one at a time. At some point it stops being a heap, and there is no grain at which that happens. Is this is a heap true or false at grain four hundred? Saying it must be one or the other, though nobody could ever say which, is a substantial claim rather than an obvious one.

And there is a second doubt, sharper in mathematics. If you prove a number exists by showing that its non-existence leads to contradiction, you have not produced the number. Whether that counts as knowing it exists is exactly what the argument is about.

As a philosopher would put it

The excluded middle - that P or not-P - is distinct from bivalence, that every proposition has exactly one of two truth values, though the two travel together in classical logic. Aristotle's own worry concerns future contingents: if it is now true that there will be a sea battle tomorrow, the future looks fixed, and he appears to consider restricting the principle for such statements.

Intuitionism is the sustained rejection. Brouwer holds that mathematical objects are mental constructions and that a proof is a construction, so asserting P or not-P without a method of deciding which is unwarranted. This invalidates proofs by contradiction for existence claims, and the resulting mathematics is weaker and constructively meaningful - every proof yields a procedure.

The practical consequence is large and modern. Proof assistants built on constructive logic - Coq, Agda, Lean - extract executable programs directly from proofs, which is possible precisely because a constructive existence proof contains the object. Vagueness supplies a separate line of attack, with supervaluationism and many-valued logics as the main alternatives.

Where you meet it

Formal verification tools used for critical software are built on constructive logic, and the reason is entirely practical.

In a constructive system, a proof that a value with some property exists is a procedure for producing it. The Curry-Howard correspondence makes proofs and programs the same objects, so a verified proof compiles into code that is correct by construction. CompCert, a C compiler verified in Coq, is the standard example: its correctness proof is machine-checked, and a well-known study of compiler testing found bugs in every mainstream compiler examined and none in CompCert's verified core.

A classical proof by contradiction would establish that a correct compiler exists without producing one, which is of no use to anyone shipping software. Excluded middle is not banned from these systems out of philosophical scruple; it is set aside because a proof that does not construct the thing does not do the job. That is a two-thousand-year-old dispute settled, in one domain, by engineering.

What is actually disputed

Whether excluded middle holds universally.

Classicists hold that it does, that intuitionist scruples confuse truth with our capacity to establish truth, and that a statement about an undecided mathematical question is true or false whether or not we can tell. Intuitionists reply that this treats mathematical objects as discovered rather than constructed, and that the classical position quietly assumes a Platonism it has not argued for.

Vagueness is the harder case for both. If there is a precise grain at which the heap ceases to be a heap, the principle is saved at the cost of a fact nobody could know and nothing determines. If there is not, either the principle fails or truth values must be more than two. Epistemicism, supervaluationism and degree theories each take one of those exits, and each is regarded by the others as paying too much.

Commonly confused with

  • Non-contradiction c. 330 BC That says not both; this says at least one. Intuitionists keep the first and reject the second, which shows they are independent.
  • black-and-white thinking Refusing to see nuance is a habit of mind. The principle is about propositions, and a proposition can be as nuanced as you like.
  • Determinism 1677 Aristotle worried that fixed truth values for future statements imply a fixed future. Whether that follows is a separate and much-argued question.

Defined against

  • Catuṣkoṭi Four exhaustive options where this principle recognises two, which is the sharpest cross-tradition disagreement in logic

Philosophers

  • Aristotle States it, and raises the future-contingents worry against it
  • Ludwig Wittgenstein Bivalence assumed in the Tractatus and questioned later
  • Rudolf Carnap Where the choice of logic becomes a choice of framework
  • Nagarjuna Where four corners replace two

Works

Schools

Related concepts

Non-contradiction c. 330 BC · Catuṣkoṭi c. 150 · Validity c. 330 BC · Paradox c. 450 BC · Truth c. 330 BC

Aristotle states it and immediately worries about future contingents - whether there will be a sea battle tomorrow - which is the first recorded doubt about it and still one of the best.