On Formally Undecidable Propositions

A formal system is deliberately blind. It is a machine for shuffling strings of symbols according to rules that never mention what the symbols are about, and that blindness is the whole point: it is what makes a proof checkable by someone who understands nothing. The central claim of this chapter is that such a machine, once it is strong enough to talk about ordinary arithmetic, must contain a statement that is true of the numbers and that the machine cannot derive — and that this is not a trick, a paradox, or a sign that something was smuggled in.

The construction has exactly three moving parts, and everything else today is detail hung on them. First, a system whose only notion of correctness is "derivable by the rules". Second, a coding that turns every string of that system into a single number, so that claims about strings become claims about arithmetic — which the system already talks about. Third, a self-application: a formula that is handed its own code number.

Today's boundary is worth stating plainly. Inside: what a formal system is, what a theorem is, how strings become numbers, how the property "is a proof of" becomes arithmetic, how the self-referential sentence is assembled, and how both branches of the resulting fork close. Outside: the full proof that the proof relation is expressible in arithmetic — that is the technical heart, it is genuinely hard, and Hofstadter sketches rather than proves it. Also outside: any claim about minds, computers, or the limits of science, which arrive in the closing section only to be taken away again.

Two things carry over from earlier days and nothing else is assumed. From Day 01: a level of description is a vocabulary in which a system can be described, and a level can be sealed off — used without looking underneath — only while the detail beneath it is irrelevant to the question being asked. From Day 02: a diagonal argument builds a new object by walking down a list and deliberately differing from the list's nth entry at position n, so the new object cannot be anywhere on the list.

That is the smallest complete model of a formal system: a supply of strings, a derivation process, and the strings that come out of it. Every later diagram today keeps these three boxes unchanged and adds one layer to them.

Nothing in the argument works until "theorem" stops being a compliment and becomes a mechanical fact. Typographical Number Theory, Hofstadter's name for a formal system that talks about the natural numbers, is defined by three finite things: an alphabet, a short list of axioms, and a list of rules of inference.

The alphabet is small and fixed.

numbers      0   S   +   and the raised dot for multiplication
relation     =
variables    a   b   c   a'   b'   and so on
logic        ~ for not, plus and, or, implies, ∃, ∀
grouping     (   )   and the angle brackets and colon

S means "the successor of", so 0 is zero, S0 is one, SS0 is two, and the number 5 is written as five S symbols in front of 0. A string is any finite sequence of these symbols. A well-formed formula is a string built by the grammar rules — SS0=SSS0 is well formed and false, S0=)(+ is not well formed at all.

Five axioms describe addition, multiplication and zero. Two of them are all we need here.

axiom 2     ∀a:(a+0)=a
axiom 3     ∀a:∀b:(a+Sb)=S(a+b)

The rules of inference are typographical operations. Specification lets you drop a ∀a: and replace every a by any chosen term. Add S lets you put an S in front of both sides of an equality. Transitivity lets you pass from r=s and s=t to r=t. Here is a complete derivation, with every step licensed by one of those rules.

1.  ∀a:(a+0)=a                axiom 2
2.  (0+0)=0                   specification of line 1, a becomes 0
3.  S(0+0)=S0                 add S to both sides of line 2
4.  ∀a:∀b:(a+Sb)=S(a+b)       axiom 3
5.  ∀b:(0+Sb)=S(0+b)          specification of line 4, a becomes 0
6.  (0+S0)=S(0+0)             specification of line 5, b becomes 0
7.  (0+S0)=S0                 transitivity of lines 6 and 3

Line 7 is a theorem: a string that stands at the end of a finite chain in which every line is an axiom or follows from earlier lines by a rule. That is the entire definition, and it says nothing about truth. Checking the derivation above requires no arithmetic ability whatsoever — only the patience to confirm that each line matches the shape the rule permits. That mechanical checkability is not a limitation of the system. It is the property the rest of the argument will exploit.

The word "theorem" invites a confusion that ruins everything downstream, so it is worth separating two properties that a string can have and that live on different levels. Derivability is a fact about the string and the rule book. Truth is a fact about the numbers, obtained by reading the string as a claim.

Read (0+S0)=S0 as a claim and it says that zero plus one is one, which is true. But the derivation did not consult that fact, and the rules had no access to it. The interpretation is a second level of description laid over the same object, and the machine is sealed off from it completely. That is why the table below has a column the machine can never read.

The system talks about numbers. It does not talk about strings — there is no symbol in the alphabet for "string", "derivation" or "theorem". Gödel's first move removes that separation by giving every string a number, so that any claim about strings can be restated as a claim about arithmetic, which the system does talk about.

The coding is mechanical. Assign each symbol a three-digit code, called a codon, then write the codons of a string one after another and read the result as a single number. The particular codes below are a convention chosen for this course; Hofstadter chooses a different table, and any other choice would work identically.

Coding strings as numbers is only useful if the interesting properties of strings survive the translation. The property that matters is "this sequence of lines is a derivation ending in that string" — and that property is purely mechanical, checkable by symbol comparison with no arithmetic insight, which is exactly what makes it expressible as a statement about numbers.

Give a whole derivation a number too, by coding its lines and joining them. Then define a relation between two numbers.

TNT-PROOF-PAIR{a, a'}
    reads as - a codes a derivation whose last line is the string coded by a'

Deciding whether a pair of numbers stands in this relation requires only decoding, grammar checking and rule matching — the same finite, dull work performed on the seven-line derivation earlier. Any relation that can be decided by such a bounded procedure can be represented in the system: there is a formula of TNT, written only with 0, S, +, multiplication, = and quantifiers, that is derivable exactly of those numeral pairs that stand in the relation, and whose negation is derivable of the pairs that do not. The derivation process, which lives on the left of every diagram so far, has become a relation among numbers, which lives on the right.

This is the load-bearing step of the whole theorem, and it is the step Hofstadter sketches rather than proves. Turning "is a derivation" into an arithmetical formula takes many pages of careful construction — coding sequences, defining substitution, showing each piece is built from bounded operations — and Chapter XIV shows the shape of that work while pointing at the original paper for the substance. Treat the representability claim as reported, not demonstrated, and do not let the ease of the sentence "so it can be written arithmetically" hide where the difficulty lives.

One consequence is worth pausing on, because it constrains everything after it. The system's axioms must be effectively given — there must be a mechanical way to recognise an axiom — or the proof-pair relation is not decidable and none of this translation happens. That condition looks like bookkeeping. It is not, and the limits section returns to it.

Self-reference in ordinary language usually needs a pointing word like "this sentence", and pointing words are exactly what a formal language lacks. Quining is the trick that produces self-reference without pointing at anything: it applies a phrase to a copy of itself.

To quine a phrase is to write the phrase in quotation marks and then write the phrase again after it. Quining is short gives:

"is short" is short

which is true, since the quoted phrase really is short. Quining has thirty letters gives a sentence that is false, since the quoted phrase does not have thirty letters. Nothing self-referential has happened yet — each sentence is simply about the quoted phrase sitting inside it. The twist appears when the phrase is chosen so that the quoted copy is also the whole sentence's subject. Quine's own example, quining yields falsehood when preceded by its own quotation, produces a sentence whose subject is a phrase that, when so preceded, is that very sentence.

Arithmoquining is the same operation with numbers doing the work of quotation marks. Take a formula with one free variable. Its quotation is its Gödel number. Instead of placing the quotation next to the formula, substitute that number — written out as a numeral, S applied to 0 that many times — for the free variable inside the formula. The result is a sentence with no free variables that talks about the number of the formula it came from.

Now the assembly. Start from a formula with one free variable, a'', built from the two relations available: the proof-pair relation, and a second relation ARITHMOQUINE{a'', a'} saying that a' is the number of the arithmoquinification of the string numbered a''. Hofstadter calls this formula the uncle.

the uncle, with one free variable a''

~∃a:∃a':<TNT-PROOF-PAIR{a, a'} ∧ ARITHMOQUINE{a'', a'}>

reads as - there is no number a coding a derivation whose last line is the
arithmoquinification of a'', that is, the arithmoquinification of a'' is
not a theorem of TNT

Let u be the uncle's own Gödel number. Now arithmoquine the uncle: replace every free a'' inside it by the numeral for u. Call the result G.

Step 4 is the pivot and deserves a slow reading. G asserts that a certain number's arithmoquinification is not a theorem. That number is u. The arithmoquinification of u is what you get by substituting the numeral for u into the uncle — which is precisely how G was built. So the sentence G describes is G. Note what G does not contain: a numeral for its own Gödel number, which is impossible, since a sentence cannot hold a numeral longer than itself. G names the uncle and the arithmoquining operation, and self-reference arrives by composition rather than by pointing.

Under the standard reading, G is an ordinary arithmetical statement — a claim that no natural number has a certain decidable property. Its self-reference is visible only from outside, to a reader who knows the coding.

Protocol. Step through the four stages for the default template and record the number produced at stage 2, then check at stage 3 that the numeral substituted into the template is that same number and that it replaces every free occurrence of the variable. Read stage 4 aloud and identify which occurrence of the number makes the sentence describe itself. Then change the template and repeat: what should change between templates is the number, while the shape of the construction stays fixed.

Limits. The lab performs the substitution and shows the resulting sentence, but it omits the two claims that make the construction legitimate: that substitution and provability are expressible inside the system as arithmetical relations. Those are asserted here and proved in the original paper. The displayed numerals are also abbreviated — written in full, the numeral for even a short template runs to an astronomical number of S symbols.

With G assembled, the argument becomes a two-branch case analysis with no third option available inside the system: either G is derivable, or its negation is, or neither is. Each of the first two branches ends in a specific defect, and naming which defect belongs to which branch is where popular accounts usually go wrong.

Branch one: suppose G is a theorem. Then there is an actual derivation of G; let m be its number and g the number of G. The proof-pair relation genuinely holds between m and g, and the arithmoquine relation genuinely holds between u and g, since G is the arithmoquinification of the uncle. Both relations are represented, so the system derives the formula stating each. From those it derives the existential claim that some pair of numbers satisfies both — which is exactly the negation of G. So the system derives both G and not-G: it is inconsistent. Read semantically, the same collapse looks like this: G says of itself that it is not derivable, so a derivable G is a derived falsehood about the numbers.

Branch two: suppose not-G is a theorem. Assume the system is consistent, so that G itself is not derivable. Then no number at all codes a derivation of G, and for each particular number 0, S0, SS0, and so on, the system derives the statement that this number is not such a code — again because the relation is represented. Meanwhile not-G asserts that some number is such a code. The system therefore claims a number with a property while denying that property of zero, of one, of two, and of every particular number in turn. That defect has a name: a system is ω-consistent when it never does this — never derives an existential claim while refuting every one of its instances. Every ω-consistent system is consistent; the reverse does not hold, so ω-consistency is the stronger assumption. In 1936 J. Barkley Rosser removed the need for it by replacing G with a cleverer sentence, one saying roughly "for any derivation of me there is a shorter derivation of my negation", for which plain consistency suffices.

The conclusion, stated exactly. For any consistent, effectively axiomatized formal system strong enough to express elementary arithmetic, G is not derivable; if the system is additionally ω-consistent — or if Rosser's sentence is used instead, merely consistent — not-G is not derivable either. Neither the sentence nor its negation can be reached, which is what incomplete means. And G is true of the natural numbers, by the shortest argument in the chapter: consistency alone implies G is not derivable, G says that no number codes a derivation of it, and that is precisely the situation. The two hypotheses do different jobs, and it is worth keeping them apart: consistency blocks G and delivers its truth; ω-consistency blocks not-G.

Protocol. Select each branch in turn and record two things: which cross edge between the two planes the branch blocks, and what the block contradicts. For the first branch, check that the contradiction is reached without appealing to truth at all. For the second, check that the contradiction is the mismatch between one existential claim and infinitely many refused instances, and note that this branch needs the stronger hypothesis. Finish on the third setting and state which of the two planes now contains something the other cannot reach.

Limits. The diagram displays the argument's shape; it does not establish the arithmetization the argument rests on, and the cross edges are drawn as given rather than constructed. The third branch is the conclusion of the reasoning, not an independent fact the picture demonstrates. Rosser's variant, which weakens the second branch's hypothesis, is not modelled.

The construction can feel like a conjuring trick until it is placed beside the argument from Day 02, which has the identical skeleton. There, a list of every bounded program was assumed, and a new function was defined to differ from the nth program at input n, so it could not appear anywhere on the list. The list here is the set of theorems, indexed by Gödel number; G is built to be the sentence that denies its own index membership in that set. In both cases the escaping object is defined by reference to its own position in the enumeration, and in both cases the enumeration's completeness is what the object contradicts.

Day 01 supplies the other half of the explanation. A level of description can be sealed off while the detail beneath is irrelevant — and the rules of TNT seal off meaning completely, which is exactly why the coding is invisible from inside. A string is manipulated as a string. That the same object is also a number, and that the number is also the subject of the string, is a relationship living on a level the machine cannot see.

That is the strange loop: not a level calling a lower level, which is ordinary, but a chain of levels that climbs away from its starting point and arrives back at it. Strings become numbers, numbers are what the strings are about, and a sentence lands on itself. The loop is not built into the system; it is built out of the system by a reader who supplies a coding the system knows nothing about.

The edge from arithmetical claims back to strings is the one the earlier diagrams left out, and it is the only new mechanism in the whole chapter. Everything else — coding, representability, substitution — exists to make that edge legitimate.

Abstractions about coding stay slippery until a number appears, so here is the whole pipeline on the shortest theorem available. Axiom 1 of TNT is ∀a:~Sa=0, and one specification step, with a becoming 0, derives the theorem ~S0=0 — zero is not the successor of anything.

Encode it with the codon table above, one codon per symbol, left to right:

symbols     ~     S     0     =     0
codons     223   123   666   111   666

Godel number of ~S0=0

    223123666111666

Decoding is the same operation reversed: chop 223123666111666 into groups of three from the left to recover 223 123 666 111 666, then read off ~, S, 0, =, 0. Different strings cannot collide, because the chopping has only one outcome.

Now name that number inside the system. The numeral for it is S written 223,123,666,111,666 times in front of 0 — a string of roughly two hundred trillion symbols. Nobody will ever write it, and nothing in the argument requires anyone to: it is finite, so it exists as a string, and that is the only property being used. Hofstadter is candid that the sentences in play are astronomically long; their length is irrelevant to their existence.

The derivation of ~S0=0 also has a number — call it m, obtained by coding its two lines and joining them. Because the derivation is genuine, the pair really does stand in the proof-pair relation, and by representability the system derives the corresponding formula:

TNT-PROOF-PAIR{SSS...S0 with m copies of S, SSS...S0 with 223123666111666 copies of S}

That is arithmetization doing real work, on a real theorem, in one concrete instance. G has the same shape with two differences: the second slot is filled by arithmoquining rather than by a number you chose, and the whole thing sits under a negation and two existential quantifiers, so that instead of confirming one derivation it denies all of them at once.

No result in mathematics is misquoted as often as this one, and most of the misquotations come from dropping one of the conditions in the statement. The theorem applies to systems that are consistent, effectively axiomatized, and strong enough to express elementary arithmetic. Remove any one of those and the conclusion goes away.

The transferable object from this chapter is the strange loop: a system, a coding that lets the system's objects stand for the system's own descriptions, and a self-application that lands one description on itself. Wherever those three ingredients appear together — self-modifying programs, self-describing grammars, a brain modelling itself — the same shape is available, and the same question can be asked of it.

The second thing to carry forward is the boundary. Any later use of "Gödel showed that..." should survive four checks: is the system consistent, is it effectively axiomatized, is it strong enough to express arithmetic, and is the claimed conclusion about that system rather than about knowledge, minds or method in general. A claim that fails any of these is not this theorem.

• [ ] Can you define "theorem" without using the word "true"?
• [ ] Can you say which two properties make a Gödel numbering work?
• [ ] Can you name the step Hofstadter sketches rather than proves, and say why it is hard?
• [ ] Can you say what arithmoquining puts in place of English quotation marks, and why G contains no numeral for its own number?
• [ ] Can you say which branch of the fork needs consistency and which needs ω-consistency?
• [ ] Can you explain why Presburger arithmetic is not a counterexample, and what happens when G is added as an axiom?
• [ ] Can you state the exact step in the Lucas–Penrose argument that is disputed?

The primary source is short and structured exactly as this chapter describes, and the secondary literature on misuse is unusually good.

• Kurt Gödel, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatshefte für Mathematik und Physik 38, 1931, pages 173–198.
• Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid, Chapter XIV, Basic Books, 1979.
• J. Barkley Rosser, "Extensions of some theorems of Gödel and Church", Journal of Symbolic Logic 1(3), 1936, pages 87–91.
• Torkel Franzén, Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, A K Peters, 2005.
• Peter Smith, An Introduction to Gödel's Theorems, Cambridge University Press, second edition 2013.
• Panu Raatikainen, "Gödel's Incompleteness Theorems", Stanford Encyclopedia of Philosophy.
• J. R. Lucas, "Minds, Machines and Gödel", Philosophy 36, 1961, pages 112–127, with Solomon Feferman's "Penrose's Gödelian Argument", Psyche 2, 1996, as the standard reply to its later form.

The chapter's result is narrow, exact, and stronger for being narrow. Every word in the statement is doing work.

• A theorem is a string the rules can derive; truth is a separate property, decided by the numbers.
• Gödel numbering needs only faithfulness and mechanical decodability to turn claims about strings into claims about arithmetic.
• Arithmetizing the proof relation is the technical heart, and Chapter XIV sketches it rather than proving it.
• Arithmoquining substitutes a formula's own number for its free variable, producing self-reference without any pointing word.
• G is derivable only if the system is inconsistent; not-G is derivable only if it is ω-inconsistent, or merely inconsistent under Rosser's variant.
• Consistency alone blocks G and makes it true of the natural numbers; ω-consistency is what closes the second branch.
• Adding G yields a consistent system with its own new undecidable sentence, and Presburger arithmetic stays complete and decidable, so the result tracks expressive strength rather than marking a universal limit.
• The step from incompleteness to any claim about minds requires knowing our own consistency, which is exactly what is in dispute.