◄ UD0   ← Frege   LOGIKĒ · X
LOGIKĒ · X · the limits of proof

Kurt Gödel

1906 – 1978 · Brno & Princeton · the Institute for Advanced Study · Einstein's closest friend there
Leibniz dreamed of a calculation that settles every question; Hilbert turned it into a program — find one complete, consistent, mechanical system that proves all of mathematics. In 1931 a shy twenty-five-year-old ended that dream forever. Gödel showed that any system strong enough to do arithmetic, if it is consistent, must contain statements that are true but that it cannot prove — and can never prove its own consistency. His trick was to make the system talk about itself by turning its sentences into numbers — the same move that lets a program be data, and that the whole of computing would be built on.
✓ STRONG

Proven, and profound. The two incompleteness theorems are rigorous and among the deepest results in all of mathematics — true-but-unprovable statements exist; no consistent arithmetic proves its own consistency.

◐ LIMITED SCOPE

It bounds formalism, not truth. It applies only to consistent systems strong enough for arithmetic, and is about formal provability — not knowledge, certainty, or whether math "works." It does not say math is broken.

◔ MOST MISQUOTED

Beware the pop version. It's endlessly abused for relativism, "no absolute truth," theology and consciousness. Nearly all such uses are wrong — it's a precise theorem, not a mood.

I · Gödel numbering — a statement becomes a number

The key idea, and it's gorgeous: give each symbol a code, then encode a whole formula as a single number by raising successive primes to those codes and multiplying. By unique factorisation, that number decodes back to exactly one formula. So every statement is a number — which means arithmetic, the thing the system reasons about, can secretly encode statements about the system itself. Build a formula and watch it become an integer.

tap symbols to build a formula
0 = 0
A formula and a number are now interchangeable — this is the rigorous form of Leibniz's prime trick, and the exact reason code can be data: a program is just a (very large) number. Stored-program computing lives here.

II · The sentence that defeats proof

Now point the encoding at itself. Using numbering, Gödel built a sentence G that, decoded, says precisely: "G is not provable in this system." A statement about provability — which is now just arithmetic — that refers to its own number. Then ask whether the system can prove it.

G says:  "G cannot be proved in this system."   Can the system prove G?
Pick one — and corner the system.
Both doors lead the same place: a consistent system has true statements it cannot reach. Truth outruns proof.
"The more I think about language, the more it amazes me that people ever understand each other at all." — Kurt Gödel

III · The two theorems, the fall, the man

FIRST INCOMPLETENESS

Any consistent formal system rich enough for arithmetic has true statements it cannot prove. Completeness and consistency cannot both be had.

SECOND INCOMPLETENESS

Such a system cannot prove its own consistency — no formal foundation can certify itself from the inside.

This detonated Hilbert's program — and with it the formal heir of Leibniz's "Calculemus." There is no single machine that decides all mathematical truth. Five years later Turing would recast the same diagonal as the halting problem: not only is truth unreachable, some questions are uncomputable. Reasoning can be mechanised — that became your computer — but it cannot be completed.

Gate kept on. Hold two things at once. The theorems are airtight and shattering — among the summits of human thought. And they are the most abused results in history: incompleteness does not say "nothing can be proven," "there is no truth," or "everything is uncertain." It is narrow and exact — about formal provability inside consistent systems that can express arithmetic — and the Gödel sentence is in fact true (we can see it from outside); it simply can't be proved inside. Mathematics did not break; it learned its own horizon. The man: Gödel escaped Austria via the Trans-Siberian railway, became Einstein's daily walking companion at Princeton, found a supposed loophole for a dictatorship in the U.S. Constitution at his own citizenship hearing, and — gripped by a paranoid fear of poisoning — would eat only food his wife prepared. When she was hospitalised in 1977, he stopped eating, and died of starvation at 71. The logician who proved the limits of certainty was undone by an excess of doubt.