Can Math Prove That It Has No Contradictions?
The Greatest Unsolved Puzzle of 1900
In August 1900, the German mathematician David Hilbert (1862–1943) stepped onto a stage in Paris. There, before the world’s finest mathematical minds, he read a list of 23 unsolved problems. The second problem on that list was deceptively simple: prove that ordinary arithmetic — the kind you use to add apples or multiply recipe ingredients — contains no hidden contradictions.
You might think arithmetic is the safest thing there is. Two plus two is four, always. But can we be absolutely certain that if we keep following the rules of arithmetic, we will never end up proving that two plus two equals five?
For thousands of years, mathematicians had dreamed of a perfect, unshakable foundation for all of mathematics. Hilbert’s challenge turned that dream into a race.
Building with Axioms: The Perfect Dream
Long before Hilbert, the ancient Greek thinker Aristotle (384–322 BC) described how a proof should work. You start with a handful of axioms — statements so basic and obvious that everyone accepts them without further argument. Then, using strict logical steps, you build up theorems, one after another, like laying bricks on a solid foundation.
The geometer Euclid (around 300 BC) turned this idea into a masterpiece. He opened his Elements with just five postulates about points and lines, then derived a whole universe of geometry from them. The chain was so clear that each new conclusion followed necessarily from the ones before — no guesswork, no gaps.
Centuries later, Gottlob Frege (1848–1925) pushed the dream further. In 1879 he invented a symbolic language for logic, aiming to make mathematical reasoning so precise that a machine could check every step. The hope was that, with careful enough rules, mathematicians would never again have to worry about hidden mistakes or contradictions. The perfect building would stand forever.
Hilbert’s Master Plan: Prove It’s Safe
Hilbert turned the dream into a concrete research program. He imagined formalizing all of arithmetic as a precise symbolic game. In this game, you begin with a small set of agreed-upon axioms — strings of symbols like “a + 0 = a.” You also fix a few rules of inference, much like the rules of chess: if you have certain strings in your proof, you are allowed to write down certain new strings. A proof becomes nothing more than a sequence of symbols produced by these rules, checkerboard-step by checkerboard-step.
Hilbert wanted to answer four big questions about this game. First, formalize it — spell out its basic objects and axioms. Second, prove its consistency: guarantee that you can never derive a contradiction, such as “0 = 1.” Third, check that the axioms are independent — none is a hidden consequence of the others. Fourth, solve the decision problem: find a mechanical method that could answer any arithmetic question thrown at it.
Crucially, Hilbert insisted that the consistency proof must be finitary. That means using only reasoning about finite, concrete symbol-patterns — nothing blurry about infinite sets, nothing that required imagining a completed infinity. He wanted a proof so elementary that even the most skeptical mathematician would trust it. If such a proof existed, mathematics would be safe forever.
The Bombshell: Gödel’s Loop
In 1930, a young Austrian logician named Kurt Gödel (1906–1978) published a paper that broke Hilbert’s dream. His result arrived like a thunderclap. A student named Carl Hempel later recalled that the great mathematician John von Neumann was teaching a course on Hilbert’s program when news came in. Von Neumann interrupted the lecture and spent the rest of the semester explaining Gödel’s discovery instead. The goal Hilbert had set, von Neumann announced, could not be achieved.
Gödel had proved two devastating things. First, any formal system rich enough to handle ordinary arithmetic is necessarily incomplete: there will always be true statements about numbers that the system cannot prove. Second, and even worse for Hilbert, such a system cannot prove its own consistency. If you try to show that your axioms will never lead to a contradiction, you will need reasoning that steps outside the system — reasoning that the system itself cannot capture. To prove arithmetic safe, you must already trust something stronger than arithmetic.
At the heart of the proof lay a trick of self-reference. Gödel showed how to encode statements about proofs as numbers. In effect, he constructed an arithmetic sentence that says, in code, that it is not provable. If the system could prove it, the system would be inconsistent. If the system is consistent, the sentence must be true but unprovable. The logicians’ perfect house of cards had turned into a hall of mirrors.
The Clever Rescue: Gentzen’s Infinite Ladder
Gödel’s result seemed to close the door. But a young German mathematician, Gerhard Gentzen (1909–1945), refused to give up. He asked: what if we allow a kind of proof that Hilbert rejected — something beyond finitary methods, yet still trustworthy in a deeper sense?
Gentzen began by reinventing the way proofs themselves are written. In his natural deduction system, proofs flow more like the way you actually think: you make temporary assumptions, derive conclusions, then discharge the assumptions at the end. He then transformed this into an even more powerful tool, the sequent calculus, which let him study proofs as mathematical objects in their own right. Using the sequent calculus, Gentzen proved a remarkable theorem: every proof can be cleaned up so that it contains no “shortcuts,” or cuts, that skip over intermediate ideas. This cut elimination offered a new kind of guarantee: if a contradiction is provable, then you can trace it back to an obvious inconsistency in the axioms themselves.
Still, a consistency proof for all of arithmetic remained out of reach — until Gentzen found a bold escape. He introduced a principle called transfinite induction up to ε₀ (pronounced “epsilon zero”). To understand this, imagine counting: 1, 2, 3, … all the finite numbers. Then imagine gathering all of them into a single new number that lives after every finite number — call it ω. Then keep going: ω+1, ω+2, … and gather those into a still larger number, and so on, until you reach the towering ordinal ε₀. Gentzen showed that if you accept this kind of infinite counting — a leap of imagination that ordinary arithmetic cannot justify — you can prove that arithmetic will never produce a contradiction. And with a twist, he also proved that ε₀ induction itself cannot be proved within ordinary arithmetic. The rescue relied on a ladder anchored just beyond the system’s reach.
Gentzen’s work was largely overlooked for decades, and his life was tragically cut short during the Second World War. But his insight gave birth to ordinal proof theory, a field that measures the “strength” of mathematical theories by the infinite heights they need to prove themselves safe.
Why Your Phone Cares About Proofs
Today, proof theory is not just a story about numbers in dusty books — it lives inside the devices you use every day. Through a deep connection called the Curry‑Howard correspondence, a mathematical proof and a computer program turn out to be two sides of the same coin. A proof of a statement “If A then B” can be read as a program that takes input of type A and produces output of type B. When your phone runs an app, careful logical rules — often built on Gentzen’s sequent calculus — help verify that the program won’t get stuck or spiral into nonsense.
So the old puzzle Hilbert posed in Paris is still with us, but in a new shape. We cannot prove arithmetic safe using only arithmetic’s own tools. But by stepping back, climbing a little further into the infinite, we have found ways to be reasonably confident that two plus two will never equal five. And in the process, we learned something even larger: a proof is not just a chain of words that persuades a person. It is a precise structure that can be studied, transformed, and — in some cases — executed by a machine. That understanding is why your technology can be trusted, and it all began with a question about a simple sum.
Think about it
- If someone showed you a proof that mathematics is free of contradictions, would you trust it any more than you already trust math? Why or why not?
- Imagine a video game world where the rules of logic sometimes lead to a paradox. Could you still have fun playing? Would you expect the game to “make sense” in the same way real life does?
- Does the fact that we cannot prove arithmetic’s consistency from within arithmetic make you less confident that 2+2=4, or does it not matter? Why?
