Logic · self-reference · the limits of proof

The Sentence That Says It Can't Be Proved

In 1931 Kurt Gödel built, inside arithmetic, a sentence that asserts its own unprovability — and showed it must be true and yet unreachable. Almost everything you've heard him quoted as proving, he didn't. Here are the two gears of the actual proof, to turn with your own hands.

Gödel is the most misquoted mathematician alive or dead. He is enlisted to prove that nothing can be known for certain, that mathematics is broken, that truth is whatever you want it to be, that the mind beats every computer, even that God exists. He proved none of those. What he proved is narrower, stranger, and far more beautiful — and it is built from two ordinary parts you can operate below before we say, precisely, what they add up to.

Gear one — arithmetic can talk about itself

The whole trick begins with a bookkeeping idea so plain it looks like nothing. Give every symbol a number; then any string of symbols — any formula — gets a single number too, by a recipe that can be undone. Once formulas are numbers, a statement about formulas (“such-and-such is provable”) becomes a statement about numbers — the kind arithmetic can already make. Build a formula and watch it turn into its number.

The arithmetization machine

Formula

The recipe — k-th symbol rides the k-th prime

Its Gödel number

The code table is a convention — any one-to-one assignment works, and the exact number you get depends on the table chosen (ours is shown by the buttons; the method is Gödel's own prime-power coding¹). What matters is not the particular number but that the coding is injective and decodable: every formula gets exactly one number, and the number alone tells you the formula back. Hit decode and watch the factorisation hand the formula back, symbol for symbol. The numbers explode — “S0=S0” is already 808,500 — and that explosion is real, but it's the price of this coding, not of arithmetisation itself: the prime-power scheme buys clean, factor-it-back decodability at the cost of size (other one-to-one codes pack the same sentence far more compactly).

Gear two — a thing that describes itself

Numbering lets arithmetic mention formulas. The second gear lets a formula mention itself. That sounds like it should require magic or an infinite regress; it requires neither. The cleanest place to see it isn't logic at all — it's a program. A quine is a program that takes no input and prints its own source code, exactly, with no cheating (it can't read its own file). Run this one and compare the output to the source, character for character.

The self-reference engine

A program (JavaScript)

What it printed

The program never looks at itself from the outside. It carries a description of its own body as data (the string s), and then it uses that description twice: once as text to print, once as code to run. Quote it, then mention the quote. That double use is the entire move — and it is exactly the move Gödel makes. His diagonal lemma proves that for any property P expressible in arithmetic (a formula with one free variable, of any complexity), there is a sentence G for which the system itself proves that G holds exactly when G's own Gödel number has property P — so G, in effect, ascribes property P to itself. (This needs the system to represent its own substitution function, which any system with a little arithmetic does.) The quine and the Gödel sentence are not a loose metaphor for each other: they are two instances of one fixed-point phenomenon (Kleene's recursion theorem is the computability twin of the diagonal lemma⁵; both fall out of a single abstract diagonal argument¹⁰).

Now point the diagonal lemma at one specific property: “…is not provable in this system.” Out comes a sentence G that says, in the pure language of numbers, “G is not provable here.” And the trap springs shut:

why G must be true and unprovable

If the system could prove G, then there would be a proof — so the system also proves the arithmetical statement “G is provable.” But G itself says the opposite: “G is not provable.” The system would then prove both a statement and its negation — it would be inconsistent. So a consistent system cannot prove G. But that is exactly what G claims, so what G says is the case: G is true — and unprovable in the system. Truth has outrun proof, with nothing up anyone's sleeve.

What he actually proved

Stated carefully — every clause below is load-bearing, and dropping one is where the popular versions go wrong:

First incompleteness theorem (Gödel 1931¹; Rosser 1936³)

Any consistent, effectively axiomatised formal system strong enough to interpret a modest amount of arithmetic contains a sentence that is true (of the natural numbers) but neither provable nor refutable within the system. You can add it as a new axiom — and the bigger system has its own new unprovable truth. The holes can't all be filled at once. (Gödel 1931 proved this assuming ω-consistency; Rosser 1936 weakened the hypothesis to plain consistency.)

Second incompleteness theorem (Gödel 1931¹)

No such system can prove a statement expressing its own consistency — written the standard way⁹ — unless it is in fact inconsistent (in which case it proves everything). A consistent system cannot certify, from the inside, that it is trustworthy — not, at least, through the natural statement of its own consistency.

The conditions are the theorem

“Every formal system has unprovable truths” is false. The theorem needs all three conditions, and you can watch each one matter. Drop “strong enough for arithmetic” and complete, decidable systems appear — real ones, not toys:

Which systems escape?

Presburger arithmetic — the whole numbers with addition but no multiplication — is consistent, complete, and decidable: a machine can settle every statement (Presburger 1929⁴). Tarski showed the same for the first-order theory of real closed fields, which contains all of high-school algebra and Euclidean geometry (Tarski 1951⁶). Multiplication of integers is the spark that lets a system encode its own syntax — and so lights the fuse. Incompleteness is not a curse on all formal reasoning; it is the specific price of being rich enough to talk about yourself.

What people wish he'd proved

With the real statement in hand, the famous misuses are easy to sort. Each card pairs the popular claim with what the theorems actually license.

Gödel proved mathematics is inconsistent / broken — that arithmetic might secretly contradict itself.

Inverted. Incompleteness is not inconsistency. The theorems assume consistency and derive a true-but-unprovable sentence from it; no contradiction in arithmetic is produced or known. If anything they show how robust the system is: it can't even prove a falsehood about itself. Franzén 2005, ch. 2.²

Gödel proved nothing can ever really be proven — certainty is an illusion.

No. Endless things are provable; the theorem locates a specific limit of specific formal systems. The proof of incompleteness is itself a fully rigorous proof — self-undermining if the slogan were true. Franzén 2005, ch. 1–2.²

Gödel proved truth is subjective / relative — there are no objective facts.

Backwards. The theorem turns on a sharp, objective gap between arithmetical truth and formal provability, and shows truth exceeds proof. Gödel himself was a thoroughgoing mathematical realist. It is an anti-relativist result wearing a relativist disguise. Franzén 2005, ch. 4–5; Sokal & Bricmont 1998 catalogue the postmodern misreadings.²⁷

Gödel proved the human mind is not a machine — that we surpass any computer.

A real argument (Lucas 1961, Penrose 1989) — but a contested philosophical one, not a theorem. The standard objection: to “see” that G is true you must assume the system is consistent, and the Second theorem says you can't establish that from inside either. Genuinely open; honestly disputed both ways. Franzén 2005, ch. 6; Lucas 1961; Penrose 1989; rebuttals by Putnam, Feferman.²⁸

Gödel proved that God exists.

A conflation of two unrelated things. Gödel did write a modal-logic ontological argument — but it is a separate piece of work with no connection to incompleteness, which is about formal systems and arithmetic. Gödel's ontological proof (written c. 1941; first published 1987 by J. H. Sobel; in his Collected Works Vol. III, 1995) ≠ the 1931 theorems.

Gödel's theorem applies to everything — every system, all of science, any self-reference.

Over-extended. It needs an effectively axiomatised system rich enough to interpret arithmetic. Presburger arithmetic and real closed fields are complete and decidable; physical theories aren't formal systems in the required sense. Self-reference alone isn't enough — you need self-reference plus arithmetic. Franzén 2005, ch. 2 & 8; Presburger 1929; Tarski 1951.²⁴⁶

The check

Nothing here is asserted on trust. The verifier (research/godel-incompleteness/verify.mjs) recomputes, offline and independently of this page:

the Gödel numbers of six sample formulas by the same prime-power coding — e.g. 0=0 → 270, S0=S0 → 808500 — as exact BigInts;
that each number decodes back to its original formula by prime factorisation (the injectivity the whole construction rests on), for every sample;
that the quine above is a byte-exact self-reproducer: node quine.js prints its own source, confirmed by file comparison.

The honest gap. This page operates the two gears — arithmetisation and self-reference — and states the theorems exactly. It does not build the full proof: writing out the arithmetical predicate Proof(m, n) (“m codes a proof of the formula coded by n”) and deriving the Gödel sentence inside a formal system is the work of a machine-checked development, not a browser toy. What's shown is the mechanism and the precise claim; what's cited is the rest. The slogans corrected above are checked against the primary and standard secondary sources listed below — chiefly Franzén's Incomplete Guide to Its Use and Abuse, the field's reference for exactly this.