Gödel's Incompleteness Theorems

The dream Gödel killed

By 1900, mathematicians had survived two foundational crises: the irrationality of √2 (which broke Pythagorean numerology), and Russell's paradox (which collapsed naive set theory in 1901). David Hilbert, the leading mathematician in Germany, proposed a programme to prevent a third. Mathematics, he argued, should be reformulated as a purely formal game with a finite list of axioms, in which:

1. Every true mathematical statement is provable. (Completeness.)
2. No false statement is provable. (Consistency.)
3. An algorithm decides whether any given statement is provable. (Decidability — the Entscheidungsproblem.)
4. Consistency itself is provable using only finitistic, indisputable methods.

This was the agenda of the 1925 manifesto "On the Infinite". By 1928 Hilbert had operationalised it as concrete questions about Peano arithmetic and Zermelo-Fraenkel set theory. The expectation was that proofs of (1) and (4) would arrive within a generation.

Three years later, the dream was over. Kurt Gödel, a 25-year-old logic researcher in Vienna, presented his paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" — On formally undecidable sentences of Principia Mathematica and related systems — at a conference in Königsberg in September 1930 and published the full version in 1931. The first theorem killed (1). The second killed (4). In 1936 Church and Turing independently killed (3). Hilbert's programme survived only as a slogan.

What "formal system" means

A formal system T consists of:

• A language: symbols (variables, logical connectives, quantifiers, function and relation symbols).
• A set of axioms: distinguished sentences in the language. The "recursively axiomatised" condition means there is an algorithm that decides, given a string, whether it is an axiom.
• A set of inference rules: typically modus ponens and generalisation.
• A definition of proof: a finite sequence of sentences, each of which is an axiom or follows from earlier ones by an inference rule, with the target sentence at the end.

The system T is consistent if no contradiction is provable. T is complete if for every sentence φ in its language, either φ or ¬φ is provable. T is sound if every provable sentence is true (in some intended interpretation, e.g., the natural numbers). For Gödel's theorem, T must be strong enough to interpret Robinson's arithmetic Q — informally, it must talk about natural numbers with addition and multiplication.

Gödel numbering: code becomes data

Gödel's first innovation was an encoding of syntax as arithmetic. Every symbol of the language gets an integer code; every formula is a sequence of symbols, encoded as the product of primes raised to those codes; every proof is a sequence of formulas, encoded the same way at the next level.

For example, with codes ¬↦1, ∧↦2, →↦3, ∀↦4, x↦5, =↦6, 0↦7, S↦8, +↦9, ·↦10, the formula "0=0" (codes 7, 6, 7) becomes 2⁷ · 3⁶ · 5⁷ = 128 · 729 · 78125 = 7,290,000,000. Every formula has a unique numerical name.

The crucial fact is that syntactic predicates become arithmetical. "n is the Gödel number of a well-formed formula", "n is the Gödel number of an axiom", "the formula with Gödel number m results from those with numbers k and l by modus ponens", "n encodes a proof of the formula with number m" — all of these can be written as primitive recursive predicates of n, m, k, l. Predicates that simple are expressible inside any system that contains Q. So the system can talk about its own proofs using only arithmetic.

The diagonal lemma

The next move is the diagonal lemma. For any formula B(x) with one free variable, there is a sentence G such that

T ⊢ G ↔ B(⌜G⌝)

where ⌜G⌝ is the numeral denoting G's Gödel number. In words: G says "B holds of my own Gödel number". The construction is purely formal — substitute carefully into "B(x ∘ x)" where ∘ denotes a syntactic operation that builds a fixed point. This is the same logical move that makes the liar paradox work, but executed in a system where it does not blow up because we are talking about truth, not asserting it directly.

Now apply the diagonal lemma with B(x) = ¬Prov_T(x), where Prov_T(x) is the arithmetical predicate "x is the Gödel number of a sentence provable in T". You get a sentence G with

T ⊢ G ↔ ¬Prov_T(⌜G⌝)

That is: G says "I am not provable in T".

First incompleteness: G is true but unprovable

Suppose T is consistent. We claim G is not provable in T. Proof: if T proved G, then by the equivalence above T would prove ¬Prov_T(⌜G⌝), i.e., T proves "G is not provable". But if T actually proves G, the predicate Prov_T(⌜G⌝) is in fact true, so its arithmetical witness can be exhibited inside T, meaning T also proves Prov_T(⌜G⌝). Both Prov_T(⌜G⌝) and ¬Prov_T(⌜G⌝) provable in T contradicts consistency.

So G is not provable in T. But that is exactly what G asserts. So G is true (when interpreted in the standard model of arithmetic). T is therefore incomplete: there is a true statement of arithmetic, namely G, that T does not prove.

What about ¬G? If T is sound (proves only truths), then ¬G is also unprovable (since G is true). Gödel's original paper used the technical condition "ω-consistency" — slightly stronger than consistency — to handle ¬G. Rosser strengthened the result in 1936 to need only consistency.

Second incompleteness: T cannot prove its own consistency

The argument that "if T is consistent then G is unprovable" is itself a piece of mathematical reasoning. Gödel showed it can be carried out inside T. So T proves the implication

Con(T) → ¬Prov_T(⌜G⌝)

where Con(T) is the formula expressing T's consistency. By the diagonal equivalence, ¬Prov_T(⌜G⌝) is just G. So T proves Con(T) → G. If T also proved Con(T), then T would prove G, contradicting the first theorem. Therefore T cannot prove Con(T) — assuming T is consistent.

This is the second incompleteness theorem. Its philosophical impact was even larger than the first: Hilbert's plan to prove the consistency of arithmetic by finitistic means could not work, because the proof would need methods at least as strong as arithmetic itself, defeating the whole point.

Worked example: encoding "0 = 1" and the diagonal sentence

Here is a small worked illustration of Gödel numbering and the diagonal construction. Use this symbol table:

0 ↦ 1     S ↦ 2     = ↦ 3     ¬ ↦ 4     → ↦ 5
∧ ↦ 6     ∨ ↦ 7     ∀ ↦ 8     ∃ ↦ 9     ( ↦ 10
) ↦ 11    , ↦ 12    x ↦ 13    y ↦ 14    z ↦ 15

The formula "0 = S0" reads: 0  =  S  0
                  symbols:    1  3  2  1
Gödel number = 2¹ · 3³ · 5² · 7¹
             = 2 · 27 · 25 · 7
             = 9450

The formula "¬(0 = S0)" reads: ¬ ( 0 = S 0 )
                     symbols: 4 10 1 3 2 1 11
Gödel number = 2⁴ · 3¹⁰ · 5¹ · 7³ · 11² · 13¹ · 17¹¹
             ≈ 1.27 × 10²²
             (an enormous but well-defined integer).

Once formulas have numbers, the predicate "Pf(n, m)" — meaning "n encodes a proof in T of the formula with Gödel number m" — is primitive recursive: it just walks down the sequence checking that each step is an axiom or a valid inference. We define Prov_T(m) ≡ ∃n Pf(n, m).

The diagonal lemma constructs G with G ↔ ¬Prov_T(⌜G⌝)
as follows. Define D(x) ≡ ∃y (sub(x, x, y) ∧ ¬Prov_T(y)),
where sub(a, b, y) is the arithmetical relation
"y is the Gödel number of the formula obtained by
substituting the numeral for b into the free variable
of the formula with Gödel number a".
Let d be the Gödel number of the formula D(x).
Define G ≡ D(⌜d⌝). Then G says
"the formula obtained by substituting d into D(x) is not provable",
which is exactly ¬Prov_T(⌜G⌝). Done.

That construction looks sleight-of-hand but is mechanical once the encoding is set up. Gödel's 1931 paper executes the whole thing in 30 pages, including the explicit primitive-recursive definitions of the syntax predicates.

First vs second incompleteness

	First incompleteness	Second incompleteness
Statement	If T is consistent, ∃ true sentence T can't prove	If T is consistent, T can't prove Con(T)
The undecidable sentence	The Gödel sentence G ≡ ¬Prov_T(⌜G⌝)	Con(T) itself
Strength needed	Robinson arithmetic Q	A bit more (Hilbert-Bernays conditions on Prov)
Construction	Diagonal lemma + Prov_T predicate	Internalise the first theorem's proof in T
What it killed	Hilbert's completeness goal	Hilbert's consistency-proof goal
Generalisation	Rosser (1936): only need consistency, not ω-consistency	Löb's theorem (1955): T proves Prov_T(⌜φ⌝) → φ only when T proves φ
Practical demonstration	Goodstein, Paris-Harrington — natural unprovable truths	ZFC's consistency provable in ZFC + "an inaccessible cardinal exists"

Why doesn't it apply to all of mathematics?

Gödel's theorem requires the system to encode multiplication on the natural numbers. Some mathematical systems are weaker and escape the theorem entirely:

• Presburger arithmetic (naturals with addition only, no multiplication, 1929) is consistent, complete, and decidable. There is an explicit algorithm — the Cooper algorithm — that decides any sentence in worst-case 2^{2^{cn}} time. It is too weak to encode multiplication, hence escapes Gödel.
• Tarski's theorem on real closed fields (1948) shows the elementary theory of (R, +, ·, <, 0, 1) is decidable, despite multiplication. The trick: real numbers have no analogue of "x is even" or "x is prime" because intermediate-value-style arguments smooth out the integer structure. Cylindrical algebraic decomposition is the modern algorithm.
• The theory of algebraically closed fields of fixed characteristic is complete and decidable. Every two algebraically closed fields of characteristic 0 with cardinality ℵ₁ are isomorphic.

The threshold is sharp: as soon as you can express both addition and multiplication on a domain in which "natural number" is definable, Gödel applies. ZFC (set theory), PA (Peano arithmetic), HOL (higher-order logic), Heyting arithmetic, all standard foundational systems are above the threshold.

Variants and extensions

• Rosser's theorem (1936). Replaces ω-consistency with plain consistency by using a sharper diagonal sentence: "for every proof of me there is a shorter proof of my negation". Same conclusion, weaker hypothesis.
• Löb's theorem (1955). If T proves Prov_T(⌜φ⌝) → φ then T proves φ. The provability operator behaves like a modal □ satisfying the Gödel-Löb axioms (GL is the canonical provability logic).
• Tarski's undefinability of truth (1936). No formula True_T(x) inside T captures "x is the Gödel number of a true sentence", or T would prove a contradiction by diagonalising. Truth in T cannot be expressed inside T.
• Chaitin's incompleteness via Kolmogorov complexity. For any formal system T, there is a constant c such that T cannot prove "the Kolmogorov complexity of n is greater than c" for any specific n. The constant equals the size of T's axioms in a suitable encoding.
• Concrete unprovable theorems. Goodstein's theorem, the Paris-Harrington Ramsey-style theorem, and Friedman's combinatorial principles are all true natural-number statements unprovable in PA. Each requires transfinite induction up to specific countable ordinals (ε₀ for Goodstein).

Where Gödel's theorems show up

• Computer science: undecidability of the halting problem. Turing's 1936 proof that no algorithm decides whether a Turing machine halts uses the same diagonal pattern. The connection runs deep: provability in T reduces to a recursively enumerable set, and the halting problem is the universal recursively enumerable set. Modern compilers cannot guarantee termination of arbitrary user code; they instead run conservative analyses (rank functions, bounded loops).
• Automated theorem proving. ATP systems (Lean, Coq, Isabelle) are recursively axiomatised and so are subject to incompleteness. Lean's mathlib, with 1.5 million+ lines as of 2026, contains theorems like the four-colour theorem and the prime number theorem but cannot internally prove its own consistency — that proof would require a stronger meta-theory.
• Cryptographic foundations. Modern public-key cryptography rests on assumed-hard problems (factoring, discrete log) whose hardness has not been proven within standard frameworks. The unconditional security would require lower bounds we cannot prove, partly because we lack natural P ≠ NP arguments — themselves believed to be independent of fragments of arithmetic.
• ZFC and the continuum hypothesis. Gödel showed (1940) that CH is consistent with ZFC; Cohen showed (1963) that ¬CH is too. CH is independent of ZFC — neither provable nor refutable from the standard axioms. Set theorists today work in extensions of ZFC (with large cardinals, forcing axioms, V = L, etc.) to settle CH-flavoured questions. The independence is a direct consequence of the Gödel-style limitation: the axioms underdetermine the universe of sets.
• Mathematical logic curricula and AI safety. Every undergraduate logic course teaches Gödel as the canonical example of a self-reference argument. AI alignment researchers study Löb's theorem because reflective agents that try to prove their own actions safe run into provability-logic obstacles (the Löbian obstacle to self-trust).

Common pitfalls

• Reading "incomplete" as "broken". ZFC is incomplete but not inconsistent; mathematics works fine. Incompleteness only says no finite axiomatisation captures every truth; it does not say truths are arbitrary or unreliable.
• Quoting Gödel to defend mysticism. The theorem applies to formal systems with specific properties. It does not say "some things are unknowable" or "logic is limited" in any global sense. Pop-philosophy invocations almost always leave out the hypothesis "consistent recursively-axiomatised system encoding arithmetic".
• Confusing the theorem with the Liar paradox. The Liar ("This sentence is false") refers to truth, which is not formalisable in T (Tarski). Gödel's G refers to provability, which is formalisable. The two arguments share a diagonal flavour but operate on different objects; only Gödel's avoids contradiction by going up a level.
• Thinking the Gödel sentence is "weird" or contrived. Goodstein's theorem and the Paris-Harrington theorem are natural combinatorial statements unprovable in PA. The Gödel sentence's self-reference is a teaching device; many ordinary statements are independent for the same structural reason.
• Believing Gödel disproves AI or formal verification. A specific verifier T cannot prove its own consistency, but it can verify enormous quantities of mathematics. The four-colour theorem and Kepler conjecture have been formally verified. Incompleteness limits self-reference, not external reach.