What if truth requires proof? Drop the excluded middle and logic becomes constructive — and accidentally invents the theoretical foundation of programming.
Links: A History of Logic, Aristotelian Logic, The Formal Revolution, Gödel’s Incompleteness, Logic and Mathematics, Computation and Information Theory
L.E.J. Brouwer (1881–1966), a Dutch mathematician, looked at the edifice of formal logic that Frege, Russell, and Hilbert were building and said: you’re doing math wrong.
His objection wasn’t technical — it was philosophical. Classical mathematics treats truth as a property that exists independently of whether anyone can demonstrate it. Goldbach’s conjecture (every even number greater than 2 is the sum of two primes) is either true or false RIGHT NOW, regardless of whether anyone has proven it. This is the Law of Excluded Middle applied to mathematical statements: P or not-P, always, even if we don’t know which.
Brouwer rejected this. His position: a mathematical statement is not true until you can construct a proof of it. Truth isn’t something that exists “out there” waiting to be discovered. It’s something that comes into being when a mathematician (or a mind, or a process) constructs a demonstration.
This sounds like a minor philosophical quibble. It isn’t. It changes the logic itself.
Classical logic: For any proposition P, either P is true or ¬P is true. Always. No exceptions.
Intuitionistic logic: P ∨ ¬P is not assumed. It might be true in specific cases (when you have a proof of P or a proof of ¬P), but it’s not a general law. For unproven propositions, the intuitionist says: I don’t know yet. Neither P nor ¬P has been established.
Proof by contradiction is restricted. In classical logic, to prove P, you can assume ¬P, derive a contradiction, and conclude P. This works because if ¬P leads to contradiction, then ¬P is false, and by excluded middle, P must be true.
In intuitionistic logic, this only gets you ¬¬P (it’s not the case that P is false). Without excluded middle, ¬¬P does NOT collapse to P. Double negation elimination fails. “It’s not the case that it’s not raining” does NOT mean “it’s raining” — it means you’ve refuted the claim that it isn’t raining, but you haven’t constructed rain.
This is a real restriction. Many classical theorems that depend on proof by contradiction don’t have intuitionistic proofs. They might still be true — but the intuitionist won’t assert them until someone finds a constructive proof.
Everything else in classical logic still holds:
Intuitionistic logic is classical logic minus excluded middle and double negation elimination. Everything provable intuitionistically is also provable classically. Intuitionistic logic is a subset of classical logic — more conservative, harder to prove things in, but everything it does prove is rock-solid.
Arend Heyting (Brouwer’s student) formalized intuitionistic logic in the 1930s. The key: reinterpret what “proof” means for each connective.
The Brouwer-Heyting-Kolmogorov (BHK) interpretation:
| Statement | Classical meaning | Intuitionistic meaning |
|---|---|---|
| P ∧ Q | P is true and Q is true | I have a proof of P AND a proof of Q |
| P ∨ Q | P is true or Q is true (or both) | I have a proof of P OR a proof of Q (and I know which) |
| P → Q | If P is true then Q is true | I have a method that converts any proof of P into a proof of Q |
| ¬P | P is false | I have a method that converts any proof of P into a contradiction |
| ∃x.F(x) | There exists an x such that F(x) | I can construct a specific x and a proof that F(x) |
| ∀x.F(x) | For all x, F(x) is true | I have a method that, given any x, produces a proof of F(x) |
Notice the pattern: everything is about having a construction or having a method. Nothing is asserted without a witness. You can’t say “there exists a number with property X” unless you can actually produce the number. You can’t say “P or Q” unless you know which one.
This is the most surprising change. In classical logic, “P or Q” is true if at least one is true — but you don’t need to know which. In intuitionistic logic, “P or Q” means you KNOW which one is true and can demonstrate it.
Example: “Every real number is rational or irrational.” Classically, this is obviously true — excluded middle. Intuitionistically, this requires: for any given real number, you can determine which it is and prove it. For most real numbers, we CAN do this. But for some (e.g., numbers defined by unsolved conjectures), we can’t currently say which they are. So the intuitionist won’t assert the universal statement.
Classical existence: “There exists a solution” — true even if you can’t find it. Intuitionistic existence: “There exists a solution” — only true if you can construct one.
This has real consequences. Many classical existence proofs are non-constructive — they show something must exist without producing it. The most famous: proofs that irrational numbers exist without constructing any specific one. Intuitionists reject these proofs. They’re not wrong — they just don’t count as proofs in the stricter system.
Here’s where it gets extraordinary. Haskell Curry (1958) and William Howard (1969) independently noticed a deep structural correspondence:
Proofs in intuitionistic logic ARE programs in typed lambda calculus.
| Logic | Computation |
|---|---|
| Propositions | Types |
| Proofs | Programs |
| P → Q (implication) | Function from type P to type Q |
| P ∧ Q (conjunction) | Pair type (P, Q) |
| P ∨ Q (disjunction) | Sum type (either P or Q) |
| ∃x.F(x) (existence) | A value x paired with evidence F(x) |
| Proof simplification | Program execution |
This isn’t a metaphor. It’s a precise mathematical equivalence. Writing a proof that P implies Q is literally the same formal object as writing a function that takes a P and returns a Q. Checking that a proof is valid is literally the same operation as type-checking a program.
1. Proofs are programs. If you have a constructive proof that a solution exists, you can extract a program that computes the solution. The proof IS the algorithm. This is why intuitionistic logic powers modern proof assistants (Coq, Agda, Lean) — you write proofs and get verified programs for free.
2. Programs are proofs. If you write a well-typed program, you’ve implicitly proven a theorem. The type system is a logic, and type-checking is proof-checking. Every time a compiler verifies your program’s types, it’s verifying a logical proof.
3. Excluded middle is non-constructive because it would be a magic oracle. In computational terms, P ∨ ¬P would be a program that, given any proposition, immediately returns either a proof or a disproof. That’s a halting oracle — which Turing proved can’t exist. Excluded middle is computationally impossible. Intuitionistic logic rejects it for good reason: it demands something that no computation can provide.
Vault connection: This is the deepest link between logic and computation. Boolean algebra (Boole) maps logic to circuits — the hardware level. Curry-Howard maps logic to programs — the software level. Logic doesn’t just run on computers (Shannon’s bridge). Logic is computation (Curry-Howard). They’re the same formal structure viewed from two perspectives.
This connects directly to Computation and Information Theory: computationally irreducible systems can’t be shortcut. Intuitionistic logic formalizes exactly which mathematical truths CAN be computed (constructive proofs) and which can’t (non-constructive classical proofs that require excluded middle). The boundary between intuitionistic and classical logic IS the boundary between what’s computable and what isn’t.
The disagreement between Brouwer and Hilbert wasn’t polite. Hilbert considered intuitionism a threat to mathematics. His famous remark: “Taking the principle of excluded middle from the mathematician would be the same as prohibiting the astronomer his telescope or the boxer the use of his fists.”
Brouwer’s response, essentially: the telescope shouldn’t show you things that aren’t there. If you can’t construct it, you don’t have it. Claiming existence without construction is like claiming you’ve been to a country because you can prove it’s not impossible to go there.
Who won? Neither, in a sense. Classical mathematics continues to use excluded middle freely and produce correct, useful results. Intuitionistic mathematics developed its own rich theory. And the Curry-Howard correspondence showed that intuitionistic logic has a computational interpretation that classical logic lacks — which turned out to be enormously practical for computer science.
The modern consensus: both are legitimate. Classical logic is the right tool when you don’t care about computability. Intuitionistic logic is the right tool when you do. This is exactly the vault’s position — different logics for different domains, none uniquely “correct.”
Typed functional programming languages (Haskell, ML, Agda, Coq, Lean) are built on the Curry-Howard correspondence. Their type systems ARE intuitionistic logics. When you write a function with type A → B, you’re proving that A implies B. When the compiler accepts your program, it’s verified your proof.
Software like Coq and Lean allows mathematicians to write machine-verified proofs. The proofs are intuitionistic by default (constructive). Results verified in these systems are as certain as anything can be — the proof has been mechanically checked step by step. The four-color theorem was verified this way (2005). Homotopy type theory is being developed in proof assistants.
Some formal verification systems for smart contracts use intuitionistic type theory. If a contract’s behavior has been proven correct in the type system, it CAN’T have the bug — the proof IS the program, and the program IS the proof.
Excluded middle is not self-evident. For 2,300 years it was treated as axiomatic. Brouwer showed you can do coherent, powerful mathematics without it. An axiom you can drop without losing coherence isn’t a law of reality — it’s a design choice.
Truth and proof can come apart. Classical logic assumes every truth is in principle provable. Gödel showed this is false (some truths are provable in no system). Brouwer went further: he refused to assert truths that couldn’t be demonstrated. This is a more conservative, more honest epistemology.
Logic and computation are the same thing. Curry-Howard is not a loose analogy. It’s a theorem. This means the question “what can logic do?” and the question “what can computers do?” have the same answer. The limits of logic ARE the limits of computation. Gödel’s incompleteness and Turing’s halting problem are the same theorem in different notation.
Different logics for different domains. You wouldn’t use a screwdriver as a hammer. You shouldn’t use classical logic when you need computability guarantees, and you shouldn’t use intuitionistic logic when you just need to know whether a conjecture is true or false. The toolkit has multiple tools. Using the right one is wisdom, not relativism.