Kurt Gödel, 1931

The sentence that can't be proved

In 1931 Kurt Gödel showed that every consistent formal system with mechanically checkable proofs that can do basic arithmetic leaves some statements about numbers that it can neither prove nor disprove. Then he showed such a system can't even prove its own consistency.

The full proof is long, but it runs on a handful of ideas. Here they are, one at a time, in a little paper world.

scroll down ↓

1 · the machine

A machine that prints theorems

A formal system is a machine. Load it with a few starting strings (the axioms) and a few rules for turning strings into new ones, and it prints everything it can reach.

Here is a tiny one, the MIU system from Douglas Hofstadter's Gödel, Escher, Bach. Its only axiom is MI. Press a rule to print the next string.

MI

Rules: I a string ending in I can get a U added. II Mx can become Mxx. III any III can become U. IV any UU can be dropped.

That is all provable means: the machine can print it. It never knows what a string means. It only follows the rules.

Can it ever print MU?

No. Count the I's. You start with 1. Rule II doubles the count, rule III removes 3, and the other rules leave it alone. Neither move can turn a count that isn't a multiple of 3 into one that is, so the count never reaches 0, and MU has no I's.

Notice where that argument happened: outside the machine, reasoning about it. Keep that in mind.

2 · statements are numbers

Every formula is a number

The systems Gödel cared about print statements about numbers, such as 1 + 1 = 2, written S0+S0=SS0 (S means "the next number after", so SS0 is 2).

His trick: give each symbol a code, then pack a formula into one number. The first symbol's code is the power of 2, the second's the power of 3, then 5, 7, 11, through the primes.

Type or tap. On a keyboard, * is ×, ~ is ¬, -> is →, A is ∀.

its Gödel number

Every whole number splits into primes in exactly one way, so the number can always be decoded back into the formula. Try one:

A proof is a list of formulas, so it gets a number too: 2 to the first line's number, times 3 to the second line's, and so on.

3 · provable(n)

"Provable" is a property of numbers

Checking a proof is mechanical. Each line must be an axiom or follow from earlier lines by a rule. Here the axioms are ∀x(x+0=x) ("adding zero changes nothing") and "anything true for all x is true for a particular number". The rule: from A and A→(B), get B. Edit lines 2 and 3.

  1. ∀x(x+0=x)

Since formulas are numbers, this check is arithmetic. So there is a formula Proof(p, n) that holds exactly when p is the number of a valid proof whose last line has number n.

Now define Prov(n): "there is some p with Proof(p, n)". The sentence "the formula numbered n is provable" has become a statement about numbers, written in the system's own language.

Checking a given proof always finishes. Searching for one might not: if no proof exists, the search never stops. That difference matters later.

4 · self-reference

A sentence about itself

Can a sentence talk about itself without saying "this sentence"? The philosopher W. V. Quine showed how in plain English. Step through it:

Gödel did the same inside arithmetic. Quoting becomes taking a Gödel number, and "preceded by its quotation" becomes a calculation on numbers (feed a formula its own number). The result is a sentence G for which the system itself proves

G ↔ ¬Prov(⌜G⌝)

⌜G⌝ is G's Gödel number. In words: G is true exactly when G has no proof.

5 · the fork

The fork in the road

Call the system T, and assume it is consistent: it never proves a statement and its negation. Does T prove G? Pick a road.

    The fine print

    First incompleteness theorem. Let T be a consistent formal system whose axioms can be listed by a program, and which proves some basic facts of arithmetic (Robinson's arithmetic Q is enough). Then there is a sentence in T's language that T can neither prove nor disprove.

    Why can't T prove ¬G either? ¬G says that G has a proof, which is false. But a consistent system can still prove some false statements of this kind, so consistency alone doesn't rule it out for this G. Gödel ruled it out with a slightly stronger assumption, ω-consistency. In 1936 J. Barkley Rosser built a cleverer sentence for which plain consistency is enough.

    "G is true" means true about the actual numbers 0, 1, 2, and so on. We know it is true only because we assumed T is consistent.

    6 · the second theorem

    The machine can't vouch for itself

    "T is consistent" is also a statement about numbers. Write Con(T) for "no number is the code of a T-proof of 0 = 1". T can state it. Can T prove it?

    This doesn't mean T is inconsistent, or even suspect. A stronger system can prove Con(T): Gerhard Gentzen proved Peano arithmetic consistent in 1936 with a principle beyond Peano arithmetic, and set theory proves it too. And an inconsistent system proves everything, its own consistency included, so a self-certificate would be worthless anyway.

    7 · misquotes

    What it does not say

    Few theorems are quoted as often, or stretched as far. Tap a card.

    go deeper

    Further reading

    • Kurt Gödel, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" (1931). The original.
    • Ernest Nagel and James R. Newman, Gödel's Proof (1958). The classic short explanation.
    • Douglas Hofstadter, Gödel, Escher, Bach (1979). Home of the MIU puzzle, and a long, playful tour of self-reference.
    • Torkel Franzén, Gödel's Theorem: An Incomplete Guide to Its Use and Abuse (2005). The best antidote to the misquotes.
    • Raymond Smullyan, Gödel's Incompleteness Theorems (1992), and the puzzle book Forever Undecided (1987).
    • Peter Smith, An Introduction to Gödel's Theorems (2nd ed., 2013). A careful textbook.

    Written and drawn by Chad Smith, 2026. MIU puzzle after Hofstadter, the quotation trick after Quine. chadsmith.dev