Do You Need a Proof to Say It’s True?
The Problem with “Either It Happens or It Doesn’t”
In 1907 the Dutch mathematician L.E.J. Brouwer (1881–1966) asked a question that made mathematicians squirm. Picture the endless decimal expansion of π: 3.14159… stretching out forever. Right now, no one knows whether the digit 7 eventually appears more often than any other digit. Classical logic says: either it does or it doesn’t. That feels obvious. But Brouwer disagreed. He argued that you have no right to claim “either A or not-A” until you actually possess a proof one way or the other — or at least a method that would definitely find one. For infinite collections like the digits of π, you can’t just check every case, so the comfortable “either/or” may be a promise you can’t keep.
That challenge pulled a loose thread in the fabric of mathematics. It unravelled into a whole new kind of logic, one built entirely on what we can construct rather than what we merely hope is true.
Building Math in Your Mind, Not on Paper
Brouwer’s starting point was simple but radical. Mathematics, he said, is not a game of pushing symbols around on paper. It is a mental activity — the act of making constructions in your mind. The raw material is your intuition of time: one moment, then another, and a continuous stretch between them. Brouwer called the pattern of “one thing and then another, with a flow in between” the empty two-ity. From that seed, by repeating the pattern, you can build numbers, shapes, and eventually all of mathematics — not by discovering facts about some invisible world, but by constructing them step by step inside your own thinking.
Because math lives in the mind, language and logic are just tools for communicating and remembering what has already been built. A musical score helps you perform a symphony, but the music itself is not the ink on the page. Brouwer said that formal language accompanies mathematics the way a score accompanies a Bach oratorio. Logic can describe your constructions, but it can’t create new mathematical truths on its own. This flips the usual picture: for Brouwer, mathematics rules logic, not the other way around.
The Law You Thought Was Always Right
The logical principle Brouwer challenged is the Law of Excluded Middle (often abbreviated PEM): for any statement A, either A is true or A is false. It works perfectly in finite situations. If you have a bag of marbles, you can in principle check each color and decide “either all marbles are red or at least one is not.” But infinite sets — like all the digits of π — are different. You can’t inspect the whole infinite sequence.
Brouwer called such situations weak counterexamples. They don’t prove PEM is false; they show we currently have no justification for claiming it. For instance: consider the claim “There is a digit that occurs more often than any other in the decimal expansion of π.” No one has proved that, and no one has proved it impossible. So we can’t honestly assert “either it’s true or it’s false” as a piece of knowledge — we have neither a proof nor a disproof. Brouwer was careful: he didn’t say PEM is false (that would itself require a proof). He said it’s unreliable when extended beyond the finite, because it pretends a decision exists where one hasn’t been built yet.
At first he himself had missed this point. In his 1907 dissertation he accepted PEM, mistaking it for a harmless tautology. By 1908 he realized his error: the principle is only justified when a finite checking procedure is available. Applying it everywhere, he argued, is like assuming every dark room has a light switch — just because some rooms do.
The Proof Interpretation: Logic as a Construction Manual
If logic really comes from the way we build mathematical objects, what do the words “and,” “or,” “if-then,” and “not” actually mean? Brouwer’s student Arend Heyting (1898–1980) and the Russian mathematician Andrei Kolmogorov (1903–1987) later spelled out the answer. It’s called the Proof Interpretation (or BHK Interpretation). It works like a construction manual:
- A ∧ B (A and B): you have a proof of A and a proof of B.
- A ∨ B (A or B): you have either a proof of A or a proof of B, and you can tell which one.
- A → B (if A then B): you possess a general method that turns any proof of A into a proof of B, like a blueprint or a recipe.
- ¬A (not A): you have a proof that assuming A would lead to a contradiction — a dead end.
- ∀x A(x) (for all x): you have a method that, given any specific object, produces a proof about that object.
- ∃x A(x) (there exists an x): you can actually produce a concrete object and a proof that the object has property A.
Heyting formalized a logic based on these ideas in 1930. Kolmogorov then re‑interpreted the whole thing as a logic of problems and solutions: “A → B” means you can reduce the problem of solving B to the problem of solving A. Both agreed the meaning always comes back to construction — you have to build something, not just talk about it.
You can now see exactly why the Law of Excluded Middle fails. To assert “A ∨ ¬A” for every mathematical statement, you would need a universal decision machine: hand it any statement, and it churns out either a proof of A or a proof that A leads to contradiction. No such machine exists. Until one does, PEM is a wish, not a guaranteed tool.
When Logic Changes the Math
Choosing a constructive logic doesn’t just shuffle the rules — it reshapes what mathematics looks like. One startling result is that in intuitionistic real analysis, every function from real numbers to real numbers is continuous. In classical math, you can define functions that jump; in Brouwer’s universe, a function must be given by a rule that works for any real number (including numbers that are still being chosen, digit by digit, over time). That forces the function to be smooth and unbroken. It sounds impossible, but it follows from the demand that everything be constructed.
Brouwer also produced strong counterexamples: classical principles that not only lack proof but are flat‑out contradictory under the constructive reading. For instance, “every real number is either rational or not” is provably false intuitionistically. These examples don’t just say “we don’t know yet” — they say “no, that way of speaking is inconsistent with constructive truth.”
Such results make it clear that logic is not a neutral wrapper. The rules you adopt shape the things you can build. That’s a deep philosophical discovery, not merely a technical tweak.
So What? Truth, Knowledge, and the Game of Asking “Why?”
You don’t need to do high‑level math to meet Brouwer’s challenge every day. When you tell a friend, “There’s definitely a lake on that hill,” and they ask, “Have you seen it?”, you’re in exactly the situation the intuitionist describes. You might believe it’s there, you might have reasons to expect it, but do you know it? The intuitionist says: until you produce a construction — a photo, a map, a path you’ve walked — you don’t get to assert “either there’s a lake or there isn’t” as a settled fact. You simply don’t yet know which side of the “or” holds.
This demand made intuitionistic logic unexpectedly important in computer science, where a constructive proof that something exists is effectively an algorithm that finds it. But the philosophical point is even closer to home: it asks you to examine what “true” means. Can a statement be true if no one ever has a proof? If you say yes, you’re in classical territory. If you say truth is always tied to evidence you could, in principle, build, you’re thinking like Brouwer. The debate is still alive.
Think about it
- If no one can prove or disprove that there is life on a planet in a galaxy far away, is it fair to say “either there is life or there isn’t” as a definite fact? Why or why not?
- A friend claims, “All even numbers greater than 2 are the sum of two primes.” Nobody has found a counterexample, and nobody has a complete proof. Is the claim true right now, or is its truth still undecided?
- Think of a time you were completely sure about something but later found out you were wrong. Did your strong belief make the statement true before you discovered your mistake? What does that say about when we’re allowed to say “I know”?
