Brouwer's Big Idea: Why Some Statements Have No 'Yes' or 'No'
The Great “Yes or No” Debate
Imagine you and a friend are locked in an argument. Your friend claims: “There is a pair of twin primes — two prime numbers just two apart, like 17 and 19 — that are larger than any number you can pick.” You think for a moment. Is that statement true or false? Most of us grew up believing that every statement must be either true or false, even if we haven’t figured out which one yet. This rule is called the law of excluded middle (LEM) : for any claim A, either A is true or its negation “not A” is true. You can’t have a middle ground.
In 1908, a Dutch mathematician named L.E.J. Brouwer (1881–1966) kicked over that comfortable rule. He said that when we talk about infinite collections — like all the whole numbers — we cannot always assume that every statement about them is either true or false. Some questions, like the twin prime puzzle, have no answer we can effectively find with a guaranteed method. Brouwer launched a new kind of thinking called intuitionistic logic, which takes away the automatic right to say “either this or that.”
Building a Logic Without “Either/Or”
Brouwer believed that mathematics is something human beings construct in their minds. To him, saying a statement is true means we have a proof — a step-by-step mental construction — that shows it must be so. This is the heart of intuitionism. A statement isn’t just “true” out there in some abstract heaven waiting to be discovered; it becomes true only when a mathematician builds its proof.
From this view, the logical connectives work differently. A proof of “A and B” is a pair: a proof of A and a proof of B. A proof of “A or B” is a construction that tells you which one you have and gives you its proof. A proof of “if A then B” is a method that can turn any proof of A into a proof of B. A proof of “not A” is a method that shows that supposing A would lead to a contradiction. And a proof of “there exists an x such that A(x)” means you can actually produce a specific x and a proof that A holds for it.
Now watch what happens to the law of excluded middle. To prove “A or not A” in intuitionistic logic, you would need either a proof of A or a proof that A is impossible — right now. But for statements about infinite sets, like “every even number greater than 2 is the sum of two primes” (Goldbach’s conjecture), no one has yet found a proof or a disproof. So an intuitionist refuses to assert that the statement is either true or false. The law of excluded middle simply isn’t a logical law here.
The twin primes example hits even harder. Let A(x) mean “there exists a twin prime pair larger than x.” To claim “for every x, A(x) or not A(x)” intuitionistically, you would need an effective method — a guaranteed recipe — that, given any number x, decides whether there is a twin prime pair beyond it. Mathematicians still don’t have such a method. So the statement is undecidable for now. Intuitionistic logic does not force you to pretend you know.
The Strange Life of “Not Not A”
In the classical logic you may have seen in school, a statement and its double negation are the same. If “it’s not true that it’s not raining,” then it must be raining. In intuitionistic logic, that move — called double negation elimination — is no longer allowed. You can only conclude A from “not not A” if you have an extra reason to think A is stable in this way.
Many formulas are stable, especially negative ones. For example, “not A” is always stable: Brouwer himself showed that the absurdity of absurdity of absurdity is equivalent to absurdity. But a plain statement like “there is a pair of twin primes larger than 1,000” is not automatically stable. You might be unable to find such a pair, yet also unable to prove that none exist. So intuitionistic logic keeps the two ideas separate.
This change has far-reaching effects. Classical propositional logic has a simple truth-table test — just check the true/false assignments. Intuitionistic propositional logic has no finite truth tables; it needs infinite families of models. Yet intuitionistic logic comes with a beautiful property called the disjunction property: if you prove “A or B” without any assumptions, then you must have proved A alone, or proved B alone. There’s no bluffing. And predicate logic — logic with “for all” and “there exists” — has the existence property: if you prove “there exists an x such that A(x)”, you can actually name a specific x that works.
The Hidden Bridge Between Two Logics
You might worry: if intuitionistic logic rejects such a basic rule, isn’t it a weaker, less useful system? Here comes a twist. In 1929, Valery Glivenko showed that a classical propositional formula A is provable if and only if its double negation “not not A” is provable intuitionistically. Later, Kurt Gödel (1906–1978) and Gerhard Gentzen independently developed a deeper negative translation that converts every classical formula into an intuitionistic one — without changing its classical truth value.
The trick is to double-negate certain parts: for instance, “A or B” becomes “not (not A and not B).” After the translation, if classical logic proves A, then intuitionistic logic proves the translated version g(A). This means the two logics are equiconsistent: if one is free of contradictions, so is the other. Classical mathematics can, in a precise sense, be embedded inside the intuitionistic world. The two systems aren’t enemies; they’re different languages that can describe the same landscape.
Even more surprisingly, intuitionistic arithmetic — called Heyting arithmetic after Brouwer’s student Arend Heyting (1898–1980) — can consistently contain axioms that contradict classical arithmetic, like Church’s thesis, which says every function is computable. So intuitionistic logic opens a door to new kinds of mathematics that classical logic cannot explore.
Why a 100-Year-Old Idea Still Matters
Today, Brouwer’s brainchild lives far beyond the philosophy seminar. In computer science, proof assistants like Coq and Agda are built on intuitionistic logic. When you write a program, you can also write a proof that it works correctly, and the computer checks your reasoning. Because intuitionistic proofs are constructive — they build the very objects they talk about — you can actually extract a program from a proof. This deep connection is called the Curry-Howard correspondence: propositions are like data types, and proofs are like programs.
Think of it this way: in classical logic, you can prove “there exists a number with property P” just by showing that it’s impossible for all numbers to lack P. That’s a non-constructive proof — it doesn’t give you the number. In intuitionistic logic, you can’t cheat. You must hand over a concrete example. When you’re designing software, that concreteness is gold.
Brouwer’s challenge also reminds us that the rules of thinking aren’t written in stone. The law of excluded middle felt obvious for over two thousand years. But once mathematicians started reasoning about infinite sets, its limits became clear. Intuitionistic logic didn’t destroy classical mathematics; it added a second toolbox — one that demands more precision, more building, and sometimes less certainty. Next time you’re in a heated debate with a friend, you might ask: Can we really say this is just true or false, or are we missing a constructive proof?
Think about it
- If a truth is impossible to ever prove, does it still count as “true”?
- Imagine a video game where some doors only open if you can prove you have the right key. Could the game world exist without these doors ever being decided? What would that world feel like?
- Is it fair to say “there’s no largest prime number” if we can’t check every number? (We actually can prove it without checking each one — does that change your answer?)
