The sentence that says it has no proof

A formal system for arithmetic is a finite list of axioms and a mechanical rule for what counts as a proof. Gödel’s theorem is that any such system, if it is consistent and can express ordinary arithmetic, has a true sentence it cannot prove.

The construction is the diagonal a third time, and the reason it produces something new is a single technical step that has nothing to do with logic.

The step that makes it possible #

A formal system is a system of symbols. Its sentences are strings; its proofs are lists of strings obeying rules; and none of that is arithmetic. So a system about numbers cannot obviously say anything about itself.

Arithmetisation removes that obstacle. Assign a number to every symbol, then to every string, then to every list of strings, in a way that can be decoded — Gödel used products of prime powers, and any injective encoding does. Now every sentence has a number, every proof has a number, and the relation

the list with number $p$ is a proof of the sentence with number $s$

is a relation between two whole numbers. Crucially, it is a checkable one: given $p$ and $s$, decoding and verifying each step is a finite mechanical procedure with no judgement in it.

And a checkable relation between whole numbers is expressible in arithmetic. That is the hard technical content of the theorem — showing that the syntactic notion of proof can be written as an arithmetic formula — and it is where nearly all of Gödel’s 1931 paper goes. Once it is done, the system can state facts about its own proofs, because those facts are now facts about numbers, and the system is about numbers.

That is the whole of what makes the theorem possible. A system rich enough to describe checkable relations between numbers is rich enough to describe itself.

The table, and the diagonal on it #

With arithmetisation in hand, lay out a table.

Rows are sentences with one free variable — properties of numbers, in effect. Columns are numbers. The entry at row $F$, column $n$ records whether the system proves $F(n)$.

The rows and the columns are now indexed by the same thing, because every row is a sentence and every sentence has a number. That is exactly the arrangement Russell’s table had and Cantor’s did not, and it is the arrangement in which the diagonal produces something that has to be a row and cannot be.

Read the diagonal: for each sentence $F$, does the system prove $F$ applied to $F$’s own number? Now build a sentence $G$ that says, of each $F$, the opposite of what the diagonal says. Since $G$ is itself a sentence with a number, ask what $G$ says about itself.

It says: this sentence is not provable.

Why that finishes the argument #

Suppose the system proves $G$. Then $G$ is provable. But $G$ says it is not provable, so the system has proved something false — and a system that proves a false arithmetic statement proves everything, which is inconsistency.

Suppose instead the system disproves $G$, that is, proves $¬G$. Then the system proves “$G$ is provable”. If the system is consistent and its proofs are checkable, that in turn means a proof of $G$ exists, so the system proves both $G$ and $¬G$ — inconsistent again.

So a consistent system neither proves $G$ nor disproves it. And $G$ says it is unprovable, which — given that the system is consistent, and therefore does not prove it — is true.

There is a true sentence of arithmetic that the system does not prove.

The fixed-point lemma, which is the reusable part #

The sentence $G$ looks like a trick and it is an instance of a general fact worth stating on its own, because it is what the rest of the subject actually uses.

Fixed-point lemma. For any property $P$ expressible in the system, there is a sentence $S$ such that the system proves $S \leftrightarrow P(n_S)$, where $n_S$ is $S$’s own number.

In words: for any nameable property of sentences, there is a sentence asserting that it has that property. Take $P$ to be is not provable and $S$ is Gödel’s $G$. Take $P$ to be is provable and $S$ is Henkin’s sentence, which asserts its own provability and — for reasons that took until 1955 to settle — is provable. Take $P$ to be is false and out comes the liar sentence, which is where the whole family comes from and which shows that truth cannot be one of the properties expressible in the system, on pain of contradiction.

That last one is Tarski’s theorem and it is a genuine bonus. Provability is expressible — it is a checkable relation on numbers — and truth is not, and the liar sentence is the proof: if truth were expressible, the fixed-point lemma would hand over a sentence asserting its own falsity, and there is no consistent answer.

So the same construction, pointed at three different properties, gives incompleteness, a curiosity, and the inexpressibility of truth. The construction is the object worth having; $G$ is one of its outputs.

The three things it does not say #

The theorem is misquoted more than any other in mathematics, and the misquotations are all weakenings or wild overstatements of the same thing.

It does not say there are unknowable truths. $G$ is not mysterious. It is a specific sentence, it is true, and the argument above is a proof that it is true. What the argument uses is an assumption — that the system is consistent — which is not available inside the system. Step outside, assume consistency, and $G$ is settled. Nothing is beyond knowledge; something is beyond a particular system.

It does not say mathematics is uncertain or incomplete in an everyday sense. No theorem anybody cares about was thrown into doubt in 1931 and none has been since. What was refuted is a specific programme — Hilbert’s proposal to establish, by finite means, that a formal system for all of mathematics is complete and consistent — and the refutation is of the programme rather than of the mathematics.

It does not apply to every formal system. A system too weak to express arithmetic can be complete. The theory of the real numbers as an ordered field is complete and decidable, by Tarski’s theorem; so is Presburger arithmetic, which has addition and not multiplication. The hypothesis “can express arithmetic” is doing real work, and dropping it changes everything.

That third point is worth an extra sentence because it is the one that makes the theorem informative rather than merely grim. Multiplication is where it starts. Addition alone is safe; addition with multiplication is not. Something about the interaction of the two operations supplies enough expressive power for a system to encode its own syntax, and that is a surprisingly sharp boundary for such a sweeping-sounding result.

The second theorem, which is worse #

Gödel’s second theorem takes the same construction one step further, and it is the one that ended Hilbert’s programme.

The whole argument above — if the system is consistent, then $G$ is unprovable — is itself a piece of finite reasoning, and it can be arithmetised like everything else. So the system can prove the sentence asserting if this system is consistent, then $G$.

Now suppose the system could prove its own consistency. Then it could prove the antecedent, hence prove $G$, which the first theorem says it cannot. So it cannot prove its own consistency.

No consistent system that can express arithmetic can prove itself consistent.

That is why the consistency results this field does have are all relative — this system is consistent if that one is, as with the disc that settles the parallel postulate. There is no bottom to the chain and there is not going to be one. Gentzen proved arithmetic consistent in 1936, by an argument using induction up to a particular infinite ordinal; the proof is correct and it uses a principle arithmetic itself cannot justify, which is exactly what the second theorem says it must.

What “consistent” is doing in the statement #

Every version of the theorem carries the hypothesis if the system is consistent, and it is not a formality.

An inconsistent system proves everything, including $G$ and $¬G$, so it is complete in the literal sense of leaving no sentence undecided. Completeness on its own is therefore worthless — it is trivially available, at the cost of being worthless in every other way — and what the theorem says is that completeness and consistency cannot both be had, not that completeness is unattainable.

That framing is worth adopting because it makes the result a trade rather than a defeat. A system may be consistent and incomplete, which is the ordinary situation and is what arithmetic is; or complete and inconsistent, which is useless; or too weak to express arithmetic, in which case both are available and the system cannot say much. Three options, and mathematics picked the first without much difficulty.

The original 1931 paper needed a slightly stronger hypothesis than consistency — Gödel called it ω-consistency — for the second half of the argument. Rosser removed it in 1936 with a cleverer sentence, one that says for every proof of me there is a shorter proof of my negation, and plain consistency suffices for that. The improvement is technical and is worth a mention only because it is the kind of detail that gets flattened out of popular accounts, and because it shows the theorem was sharpened rather than merely repeated.

What a proof system can and cannot be #

It is worth putting the levels side by side, because the theorem is often heard as applying to logic generally, and it does not.

Propositional logic is complete and decidable. Every valid formula has a proof, every tableau finishes, and the truth table settles anything.

First-order logic is complete — Gödel proved that too, in 1929, and it is a different theorem with a confusingly similar name. Every logically valid sentence has a proof. What is lost is decidability: there is no procedure that always halts and reports whether a sentence is valid.

First-order arithmetic, meaning logic plus axioms for the numbers, is where incompleteness bites. Here valid and provable still coincide for pure logic, but the axioms fail to pin down the numbers, and true-in-the-numbers is strictly more than provable-from-the-axioms.

Those are three different situations and the third is the only one the incompleteness theorem is about. The distinction between the completeness theorem and the incompleteness theorem — same author, two years apart — is that the first is about logical consequence and the second is about a particular subject matter.

Why the picture is a table and not a proof #

This is the one essay in this field whose figures cannot be the argument, and it is worth saying so plainly rather than pretending otherwise.

The tables above show the arrangement — rows and columns indexed by the same thing, a diagonal, a constructed row that cannot be one of the rows. That arrangement is genuinely what the proof uses, and the figures assert it on the instance they draw: the built row differs from row $n$ at column $n$, checked for every drawn row.

What they cannot show is that the arrangement is available for a formal system, which is the arithmetisation step and which is a page of careful encoding rather than a picture. Nor can they show that the constructed sentence is expressible in the system’s own language, which is the other half.

So the honest description is: the figures show the shape of the argument, on a finite table where the shape can be checked, and the two facts that make the shape apply to arithmetic are not drawable and are stated. That is a weaker claim than this collection usually makes, and making it is better than drawing something suggestive and letting it look like more.

The figure is the right place to see how little the propositional case has to say. $p \leftrightarrow ¬p$ is a formula with a variable in it, and the variable can simply be given a value; both values fail, and the formula is unsatisfiable, and that is the end of the matter. There is no paradox because there is no self-reference — $p$ does not denote this formula, it denotes a truth value.

Everything Gödel’s construction adds is the machinery for making $p$ denote the formula it occurs in. That machinery is arithmetisation plus the fixed-point lemma, and once it exists, an unsatisfiable formula becomes a sentence with a truth value that the system cannot reach.

What is actually independent #

A reader who has followed the argument may reasonably feel that $G$ is a contrivance — a sentence built to defeat the system, of no interest in itself. That was the standard reaction for forty years and it turned out to be wrong.

There are natural statements — about ordinary finite combinatorics, of the kind somebody might have asked without ever hearing of this subject — that are true and not provable in arithmetic. The Paris–Harrington theorem of 1977 is a strengthening of Ramsey’s theorem of exactly that kind, and Goodstein’s theorem is another: a statement about sequences of whole numbers, provable using infinite ordinals and not provable without them.

That changes the character of the result. Incompleteness is not a curiosity confined to self-referential sentences; it reaches statements nobody constructed for the purpose. The next essay is one of them, and it is drawable in a way this one is not.

The boundary this essay stays inside #

There is a second reading of everything above, in which the system is a machine, the sentences are programs, and the unprovable statement is a question no procedure answers. That reading is real, it is due to Turing five years later, and it is a different subject with a different rule — its claims are about what can be computed and at what cost, measured on a named machine.

This field takes only what it needs of it, which is nothing: the argument above is about provability in a formal system, and every step of it is a statement about sentences and derivations rather than about procedures. The two subjects share a diagonal and share very little else, and it is worth keeping the shared move separate from the two conclusions it produces.