How Gödel Killed Hilbert's Dream in One Paper

In 1928 David Hilbert stood in Bologna and laid out a program: find a finite set of axioms from which every true mathematical statement can be derived, and prove from inside the system that those axioms cannot contradict themselves. He wanted mathematics on bedrock.

Three years later, a 25-year-old logician named Kurt Gödel published "On Formally Undecidable Propositions of Principia Mathematica and Related Systems." Two theorems. First: any consistent formal system strong enough to express elementary arithmetic contains statements that are true but cannot be proved within the system. Second: such a system cannot prove its own consistency.

The construction is the famous part. Gödel coded formulas as integers — every symbol a number, every formula and proof a number built from its parts. Provability then becomes an arithmetical relation between integers. Inside this coding, Gödel built a sentence G that says, in effect, "the number that codes me is not the code of any provable formula." If G is provable, the system is inconsistent. If G is not provable, then G is true — and the system has a true statement it cannot prove.

John von Neumann was in the audience when Gödel announced the result at a 1930 conference in Königsberg, and grasped within days that it sank Hilbert's program. Hilbert had wanted the consistency proof to live inside the system; Gödel's second theorem said it could not. Von Neumann wrote to Gödel a few months later with his own derivation. Gödel had already proved it.

The theorems do not say mathematics is broken, or that some truths are unknowable. They say any single, sufficiently rich formal system has gaps it cannot close from inside. You can step outside, add axioms, prove the old G — at the cost of new gaps in the larger system. Hilbert wanted closure. Closure was not on offer.