Topic · Paradox

Gödel's Incompleteness

Mathematics will never be complete.

Kurt Gödel, Vienna, 1931. In any consistent formal system rich enough to express arithmetic, there are true statements the system itself cannot prove. The Explorer walks you through Gödel numbering and the construction of the self-referential sentence G that says, in arithmetic, «I am not provable».

Discover the story → Open the Explorer

Step one · Hilbert's dream

Mechanise all of mathematics

Early twentieth century. Whitehead and Russell's Principia Mathematica (1910–1913) tried to derive every theorem of arithmetic from a single tower of logical axioms. David Hilbert, in his 1900 Paris programme and then his 1920s formalist push, asked for a finite, mechanical system from which every true statement could be proved, and whose consistency could be proved from inside. A complete, consistent, decidable formal mathematics. Anyone with paper and patience could, in principle, settle every mathematical question. That was the dream.

Step two · Gödel numbering

Arithmetic that talks about itself

Gödel's first move was a coding trick. Assign each symbol of the formal language a number — ¬ → 1, ∨ → 2, ∀ → 3, =, +, ·, parentheses, variables, and so on. Then encode a whole formula (s₁, s₂, …, sₖ) as the single natural number 2^s₁ · 3^s₂ · 5^s₃ · … using consecutive primes. By the uniqueness of prime factorisation the encoding is reversible. Proofs — sequences of formulas — get numbers too. Suddenly properties like «x is a proof of y» become arithmetic predicates Prov(x, y) that the formal system can express about its own statements.

Gödel numbering · a sample of symbol codes

Each symbol of the formal language gets its own natural number. A full formula s₁s₂s₃… is then encoded as the single integer 2^s₁·3^s₂·5^s₃·… — unique because every integer has a unique prime factorisation.

symbol	meaning	Gödel #
¬	not	1
∨	or	2
∀	for all	3
∃	there exists	4
=	equals	5
0	zero	6
S	successor	7
+	plus	8
(	open	9

Example: the tiny formula 0 = 0 (symbols 0, =, 0 → codes 6, 5, 6) becomes the Gödel number2⁶·3⁵·5⁶ = 64 · 243 · 15625 = 243 000 000.

Step three · The diagonal trick

G says: «G is not provable»

Using the diagonal lemma — descended directly from Cantor's 1891 diagonal argument — Gödel constructed a sentence G whose Gödel number is ⌜G⌝, and which is arithmetically equivalent to ¬∃x Prov(x, ⌜G⌝): «no number x is a proof of the formula with Gödel number ⌜G⌝». In plain language: G says «I am not provable in this system». Now the squeeze. If G is provable, the system proves a false statement and is inconsistent. If G is unprovable, then what G claims is exactly true — but the system cannot prove it. Either way Hilbert's dream of a complete consistent arithmetic collapses. The Second Incompleteness Theorem follows almost immediately: such a system cannot prove its own consistency, for if it could, it would also prove G, contradicting the First.

The self-reference loop

G's content and G's Gödel number are wired together. G asserts that the formula numbered ⌜G⌝ has no proof — and the formula numbered ⌜G⌝ is G itself. The loop closes on the diagonal.

sentence

«I am not provable in S»

↔

arithmetic equivalence

Gödel number

⌜G⌝

the natural number that encodes G itself

if G is provable

S proves a sentence that says «I have no proof» — the system is inconsistent.

if G is not provable

Then what G claims is exactly true — true, yet unprovable in S.

Step four · Where it spread

Tarski, Turing, Church, and every proof assistant since

The same diagonal trick keeps reappearing. Alfred Tarski (1933) proved that truth in arithmetic is not definable inside arithmetic — undefinability of truth. Alan Turing (1936) showed the halting problem is undecidable by diagonalising over Turing machines. Alonzo Church (1936) proved that first-order logic itself is undecidable. Each result is, structurally, a cousin of Gödel's: a system rich enough to describe itself contains a question it cannot answer about itself. Modern proof assistants — Coq, Lean, Isabelle, HOL — operate under Gödel's bounds: they can mechanise an enormous amount of mathematics, but they cannot prove their own consistency, and there are concrete number-theoretic statements (Goodstein's theorem, Paris–Harrington) that are true and provably unprovable in Peano arithmetic. The dream is gone; the building is bigger than ever.

Where you meet it

How and where this technique lives in the world today.

Foundations of mathematics

Gödel ended Hilbert's programme of mechanising mathematics; it reshaped what mathematicians believe is provable in principle.

Computer science

Tarski's undefinability of truth, Turing's halting problem and Rice's theorem are all direct descendants — used in every undergraduate logic and computability course.

Philosophy of mind

Penrose's argument that human minds are not purely algorithmic (The Emperor's New Mind, 1989) leans heavily on Gödel — controversial but influential.

Verified software

Modern proof assistants (Coq, Lean, Isabelle) confront Gödel's limits every day; their entire usefulness lies in formalising what is provable inside an explicit system.