Gödel, Turing and the limits of proof

The last chapter ended with a question that sounds almost like heresy. The Scottish Book still has unsolved problems, and usually that means the right idea hasn’t been found yet. But is there a statement about natural numbers that’s true yet can’t be proved in principle, whatever geniuses take it on? Before answering, let’s play a game. It was invented by Douglas Hofstadter for his book Gödel, Escher, Bach (1979), and it contains the whole plot of the chapter in miniature.

There are strings of the letters M, I and U. We start with the string MI. Four moves are allowed, and nothing else:

1. if a string ends in I, you may append U: $x\mathrm{I} \to x\mathrm{IU}$;
2. everything after M may be doubled: $\mathrm{M}x \to \mathrm{M}xx$ (MIU gives MIUIU);
3. any three I’s in a row may be replaced by a single U: $\mathrm{III} \to \mathrm{U}$;
4. any two U’s in a row may be erased: $\mathrm{UU} \to$ nothing.

The task: produce the string MU. Try it before reading on.

A game by the rules

Most likely your strings grew fast. Doubling speeds them up, triples of I turn into U, pairs of U vanish, and it seems that any moment now a single U will be left. But MU doesn’t come out. A search doesn’t help either: in at most seven moves MI gives 1730 different strings, and MU isn’t among them. But not finding something doesn’t mean there’s nothing to find: what if MU appears on the thousandth move?

This kind of game has a general name.

The key word here is “mechanically”. To check a derivation you needn’t understand anything: it’s enough to compare each string with the rules. A schoolchild can do it, and so can a computer. But to answer the question “is MU derivable”, the rules alone aren’t enough, and that’s the whole intrigue.

We must know

By the start of the twentieth century mathematicians had discovered that intuition fails even in the foundations. Naive set theory led to Russell’s paradox (chapter 51), and many began to doubt what the edifice of mathematics stood on at all. In the 1920s David Hilbert proposed a rescue programme. Write the whole of mathematics as a formal system, with axioms and mechanical rules of inference, as in the MIU game. Then prove that the system is good, and prove it rigorously, by the simplest “finitary” means, which nobody could doubt. “Good” meant two things.

An inconsistent system is useless: everything is derivable in it, since anything follows from a falsehood (chapter 51). A complete system answers every question. In 1928 Hilbert and Wilhelm Ackermann added a third requirement: there must be an algorithm that decides, for any statement, whether it’s derivable. This is the Entscheidungsproblem, the “decision problem”.

For arithmetic the candidate for such a system was the axiomatisation published by Giuseppe Peano in 1889 (a year earlier Richard Dedekind had described a similar system). Its language is sparse: zero $0$, the “next number” function $S$ (so $S0$ is one and $SS0$ is two), addition, multiplication, equality, logical connectives and quantifiers over the natural numbers. Here it’s more convenient to start the natural numbers at zero, although in the course we usually start at one.

Together with the rules of logic these axioms are called Peano arithmetic. Induction is the one from the chapter on sequences, only now it’s not a proof technique but an axiom, one for each formula $\varphi$. All the familiar properties of numbers follow from these axioms, from $2 + 2 = 4$ to the infinitude of the primes. It seemed that little remained: to prove that the system is consistent and complete.

From 5 to 7 September 1930 a conference on the foundations of mathematics was held in Königsberg. On the last day, in the closing discussion, the 24-year-old Kurt Gödel from Vienna briefly remarked that the formal system of arithmetic contains statements that are true but unprovable in it. Almost nobody understood the remark; apparently only John von Neumann grasped it immediately. The next day, 8 September, in the same Königsberg, Hilbert gave a speech that was broadcast on the radio. It ended with the words “Wir müssen wissen. Wir werden wissen”, “We must know. We will know”. These words are carved on his grave in Göttingen. Gödel’s paper came out in 1931, and Hilbert’s programme as conceived proved impossible to carry out. We’ll see how Gödel proved it, but first let’s solve the puzzle.

A step outside the system

Inside the MIU game all you can do is make moves. To prove that MU will never come out, you have to look at the game from outside and find a quantity that no move changes, an invariant, as in graph problems or in the fifteen puzzle. Hofstadter called this “jumping out of the system”.

The idea: follow not the whole string but only the remainder of the number of I’s on division by $3$. The rules move this remainder around three circles, and no arrow leads into circle $0$.

The axiom MI has one letter I, remainder $1$. We’ll prove by induction on the length of a derivation that every derivable string has remainder $1$ or $2$. Rule 1 appends U, rule 4 erases two U’s. The number of I’s doesn’t change, nor does the remainder. Rule 3 replaces three I’s by one U: the number of I’s decreases by exactly $3$, and the remainder on division by $3$ doesn’t change. Rule 2 doubles everything after M, and the number of I’s doubles. Remainder $1$ becomes $2$, remainder $2$ becomes $4$, that is, $1$ again. From remainder $0$ doubling would lead only to $0$, but we’re never there. Each rule takes a string with remainder $1$ or $2$ to a string with remainder $1$ or $2$, and at the start the remainder is $1$. By induction the number of I’s in every theorem of MIU isn’t divisible by $3$. MU has zero I’s, and zero is divisible by $3$, so MU isn’t a theorem.

Notice where this proof lived. Not inside MIU: the game itself has no numbers, remainders or induction. We reasoned about the system in a richer language, the language of arithmetic. The invariant gives more than a refusal: it describes all the theorems of MIU completely.

Is the string MUIIU derivable in the MIU system? Answer “yes” or “no”.

Yes. It has two letters I, and $2$ isn’t divisible by $3$, so by the theorem the string is derivable. One derivation: $\mathrm{MI} \to \mathrm{MII} \to \mathrm{MIIII} \to \mathrm{MIIIIIIII}$ (eight I’s) $\to \mathrm{MUIIIII} \to \mathrm{MUIIU}$: first rule 2 three times, then rule 3 twice, to the first three I’s and to the last three.

For arithmetic Hilbert hoped for the same: everything that can be known about numbers should be derivable inside the system. Gödel noticed two things. First, the language of arithmetic is rich enough to talk about formal systems, including arithmetic itself, just as we’ve just talked about MIU in the language of remainders. Second, a trap follows from this.

Formulas become numbers

For arithmetic to reason about formulas, formulas have to be turned into numbers. Give each symbol a code, for example $0 \mapsto 1$, $S \mapsto 2$, $+ \mapsto 3$, $= \mapsto 5$, and encode a string of symbols as a product of powers of primes.

The primes in order: the first place in the string is two, the second three, the third five, and so on. $p_k$ is the $k$th prime. The codes of the symbols: $a_i$ is the code of the symbol in the $i$th place. The exponent says which symbol, the base in which place. Example: the formula $0 = 0$ is the symbols with codes $1, 5, 1$, and its number is $2^1 \cdot 3^5 \cdot 5^1 = 2 \cdot 243 \cdot 5 = 2430$. The formula $S0 = S0$ gets the number $2^2 \cdot 3^1 \cdot 5^5 \cdot 7^2 \cdot 11^1 = 20{,}212{,}500$.

Uniqueness is guaranteed by the fundamental theorem of arithmetic (chapter 3): factorisation into primes is unique, so the exponents, and hence the symbols, can be read off the number without ambiguity. Not every number is a Gödel number: $10 = 2 \cdot 5$ skips the three, and in $2^{20}$ the exponent $20$ isn’t the code of any symbol. Check it on the encoder.

The numbers grow fast: the formula $\forall x\,\neg(Sx = 0)$ of nine symbols already has a 55-digit number. But size doesn’t matter; what matters is mechanicalness. A proof is a sequence of formulas, and it too can be encoded as a number, for example $2^{\ulcorner\varphi_1\urcorner} \cdot 3^{\ulcorner\varphi_2\urcorner} \cdots$. And here’s Gödel’s key observation. Checking “is the number $x$ the number of a proof of the formula with number $y$” is a mechanical procedure: factorise $x$, read off the formulas, compare each with the axioms and rules. And any such procedure can be written as a formula of arithmetic. We get a formula $\mathrm{Prf}(x, y)$, “$x$ is the number of a proof of the formula with number $y$”, and a formula $\mathrm{Prov}(y) = \exists x\,\mathrm{Prf}(x, y)$, “the formula with number $y$ is provable”.

Hofstadter shows the same on MIU. Replace M by $3$, I by $1$, U by $0$: the string MIIU becomes the number $3110$. Then rule 1, “append U to a string ending in I”, becomes “append a zero on the right to a number ending in one”, that is, multiply by $10$. The other rules also become operations on decimal digits, and the sentence “MU is a theorem of MIU” turns into a statement about numbers: “$30$ is obtained from $31$ by these operations”. A question about symbols has become a question of arithmetic.

With our table of codes ($0 \mapsto 1$, $S \mapsto 2$), which string of symbols does the number $180$ encode?

$180 = 2^2 \cdot 3^2 \cdot 5^1$. The exponents in order: $2, 2, 1$, that is, the symbols $S, S, 0$. It’s the string $SS0$, the numeral for two.

A sentence that talks about itself

The ancient liar paradox: “This statement is false.” If it’s true, it’s false, and if it’s false, it’s true. The word “this” cheats here: arithmetic has no demonstrative pronouns, and a formula can’t point a finger at itself. But self-reference can be built honestly, by substitution. Here’s a sentence devised by the philosopher Willard Quine:

“yields falsehood when preceded by its quotation” yields falsehood when preceded by its quotation.

Do what it says: take the phrase in quotation marks and put its own quotation in front of it. You get this whole sentence. So the sentence says of itself that it’s false: a liar without the word “this”. The mathematical version of the trick is called the diagonal lemma. The role of “preceded by its quotation” is played by the function $\mathrm{diag}$: given the number $n$ of a formula $\varphi_n(x)$ with one free variable, it outputs the number of the formula $\varphi_n(\bar n)$, in which the number $n$ is substituted for $x$ (the bar means the numeral for the number in the language: $\bar 2 = SS0$). The function $\mathrm{diag}$ is computable, and by the representability lemma arithmetic can talk about it.

The idea is the same table as in Cantor’s diagonal proof (chapter 52). The rows are the formulas $\varphi_0(x), \varphi_1(x), \dots$ with one variable, listed in order of their numbers; the columns are numbers; cell $(n, k)$ holds the statement $\varphi_n(\bar k)$. We’re interested in the diagonal.

On the diagonal stand the statements $\varphi_n(\bar n)$: each formula applied to its own number in the list. Their numbers are computed by the function $\mathrm{diag}(n) = \ulcorner\varphi_n(\bar n)\urcorner$. Form the formula $\psi(x) = \varphi(\mathrm{diag}(x))$: “the number of the diagonal statement for $x$ has the property $\varphi$”. This is a legitimate formula with one variable, because $\mathrm{diag}$ is representable. So it’s in the list: $\psi = \varphi_m$ for some number $m$. Look at the cell $(m, m)$, where the row of $\psi$ meets the diagonal. It holds the statement $G = \psi(\bar m) = \varphi(\mathrm{diag}(\bar m))$. But $\mathrm{diag}(m)$ is by definition the number of the statement $\varphi_m(\bar m) = \psi(\bar m) = G$. Arithmetic proves the equation $\mathrm{diag}(\bar m) = \ulcorner G\urcorner$ (the representability lemma), so $G = \varphi(\mathrm{diag}(\bar m))$ is provably equivalent to $\varphi(\ulcorner G\urcorner)$. The cell talks about itself.

Now take as $\varphi(y)$ the property “the formula with number $y$ is unprovable”, that is, $\neg\mathrm{Prov}(y)$. The diagonal lemma produces a statement $G$ that’s provably equivalent to $\neg\mathrm{Prov}(\ulcorner G\urcorner)$: “I am unprovable”. This is no longer a paradox but a trap. The liar has no good truth value; $G$ has one.

The trick is that a proof of $G$ would itself be a refutation of $G$. The representability lemma is applied to $\mathrm{Prf}$ for the system $T$: checking proofs in $T$ is mechanical, because its axioms can be recognised mechanically.

Suppose $T$ proves $G$. Then $G$ has a proof with some number $p$, and the statement $\mathrm{Prf}(\bar p, \ulcorner G\urcorner)$ is true. It’s a concrete check of concrete numbers, and by the representability lemma $T$ proves it, and with it $\exists x\,\mathrm{Prf}(x, \ulcorner G\urcorner)$, that is, $\mathrm{Prov}(\ulcorner G\urcorner)$. On the other hand, $T$ proves $G$ and the equivalence $G \leftrightarrow \neg\mathrm{Prov}(\ulcorner G\urcorner)$, so it also proves $\neg\mathrm{Prov}(\ulcorner G\urcorner)$. The system has proved a statement and its negation, yet it’s consistent. So $G$ isn’t provable in $T$. Since there’s no proof, the formula $\mathrm{Prov}(\ulcorner G\urcorner)$, “there’s a number of a proof of $G$”, is false in the natural numbers, and $\neg\mathrm{Prov}(\ulcorner G\urcorner)$ is true. If the theorems of $T$ are true, then the proved equivalence is true, and so $G$ is true. Then $\neg G$ is false, and a system that proves only true things won’t prove it. Neither $G$ nor $\neg G$ is derivable in $T$: $T$ is incomplete, and $G$ is a statement that’s true but unprovable in $T$.

The condition “all theorems are true” can be weakened. Gödel himself managed with a weaker technical condition, so-called ω-consistency, and in 1936 J. Barkley Rosser built a different statement, a little craftier than $G$, for which consistency alone suffices.

The key word in the theorem is “any”. Add $G$ to the axioms: you get a new system $T'$, still consistent and mechanical, and the diagonal lemma will build its own $G'$ for it. No finite or mechanically listable set of axioms exhausts arithmetical truth. Unprovability is always relative: $G$ is unprovable in $T$, but trivially provable in $T'$.

What does Gödel’s first theorem state?

That arithmetic is inconsistent That every consistent, mechanically specified system containing arithmetic has a statement it neither proves nor refutes That there are statements that can’t be proved in any system of axioms That truth in mathematics depends on one’s point of view

Incompleteness is a property of each particular system: it has its own $G$. Adding $G$ to the axioms gives a system in which $G$ is provable, but it will have its own unprovable statement.

A system can’t vouch for itself

Gödel dealt Hilbert’s programme a second blow in the same paper. The statement “$T$ is consistent” can also be written as a formula of arithmetic: “there’s no proof of the statement $0 = S0$”, that is, $\mathrm{Con}(T) = \neg\mathrm{Prov}(\ulcorner 0 = S0\urcorner)$.

By some accounts, in November 1930 von Neumann derived the second theorem from the first on his own and wrote to Gödel, but Gödel had already found it. The meaning is harsh: the consistency of arithmetic can’t be proved by means weaker than arithmetic itself. Hilbert’s programme in its original form collapsed. That doesn’t mean the consistency of arithmetic is in doubt: in 1936 Gerhard Gentzen proved it, but by relying on transfinite induction, a principle that isn’t in Peano arithmetic. Confidence in the foundations remained, but it rests not on a finitary check but on conviction in stronger principles.

What an algorithm is

Hilbert’s third question remained, the decision problem: is there an algorithm that tells, for any statement, whether it’s derivable? To answer “no”, you first have to say precisely what an algorithm is. In 1936 this was done independently by Alonzo Church in Princeton and the 23-year-old Alan Turing in Cambridge. Turing’s definition is an imaginary computer that performs the simplest actions imaginable.

It seems that such a thing can at most add one. But Turing showed that any computation that can be described as a mechanical procedure can be expressed with such tables. Moreover, there’s a universal machine: it reads from the tape a description of any other machine and its input, and does what that machine would do. This is the idea of a stored program, more than ten years before the first such computers. The claim “everything computable by a mechanical procedure is computable by a Turing machine” is called the Church–Turing thesis. It isn’t a theorem: “mechanical procedure” is an informal notion. But in ninety years no computation has been found that doesn’t fit into a Turing machine, and all the models proposed, Church’s λ-calculus, recursive functions, any programming language, have turned out to be equivalent to it.

The halting problem

Every machine on a blank tape either halts at some point or runs for ever. You can watch it, but what do you do if the machine has been running for a million steps? Maybe it’ll halt on step one million and one. We’d like a judge program.

The trick is the diagonal again. If a judge existed, a program could be built from it that defies the judge on itself.

Suppose the program $H$ solves the halting problem: on input $(P, x)$ it always halts and answers “halts” or “loops”, and is always right. Programs are finite texts and can be listed in order of their numbers: $P_0, P_1, P_2, \dots$ (the set of programs is countable, chapter 52). Let the inputs be numbers. Make a table: cell $(i, j)$ says whether $P_i$ halts on input $j$. $H$ can fill in all its cells. Look at the diagonal: does $P_n$ halt when given its own number $n$ as input? Write a program $D$. On input $n$ it runs $H$ on the pair $(P_n, n)$. If $H$ answered “halts”, $D$ goes into an endless loop; if “loops”, $D$ halts. This is a legitimate program: $H$ exists by assumption, and the rest is a branch and a loop. The row of the program $D$ is the flipped diagonal: on input $n$ it behaves opposite to $P_n$ on input $n$. $D$ is a program, so it’s somewhere in the list: $D = P_k$ for some $k$. Compare row $k$ with the row of $D$ at cell $(k, k)$. If $P_k$ halts on input $k$, then $H$ will say so, and $D$ on input $k$ will loop; if $P_k$ loops, $D$ will halt. Either way $D$ and $P_k$ behave differently on input $k$, yet they’re the same program. A contradiction. The row of $D$ differs from every row of the table, though $D$ is a program and has to be in it. So the assumption is false, and the program $H$ doesn’t exist.

Test the argument on live “judges”. Below, the machine $D$ is assembled from whichever predictor you choose, including yourself.

With this Turing answered Hilbert as well. If there were an algorithm deciding whether a statement is derivable, it could be used to solve the halting problem too: the statement “the machine $P$ halts on input $x$” can be written in arithmetic in the language of numbers, like provability in Gödel’s work. So the decision problem is undecidable. The term “halting problem” itself appeared later, among Turing’s followers, but the diagonal argument is his.

Does the theorem imply that you can’t find out whether the program “while true: do nothing” halts?

Yes, nothing at all can be found out about programs No: for individual programs it can often be proved whether they halt; what’s impossible is one algorithm that answers for all of them Yes, but only on weak computers

The theorem forbids a universal judge. For many particular programs the answer is easily found, and for some it’s very hard; there are even programs whose halting can be neither proved nor refuted in a chosen system of axioms, as we’ll see below.

The halting problem gives a second proof of incompleteness that needs no technical representability lemma except the simplest one: the statement “$P$ doesn’t halt on input $x$” can be written as a formula of arithmetic. A computation is a finite sequence of tape states, it can be encoded as a number, and “$P$ halts” means “there’s a number encoding a halted computation”.

Undecidability next door

You might think undecidability lives only in artificial questions about programs that ask about themselves. In the second half of the twentieth century it turned out to be hiding in perfectly ordinary mathematics.

Hilbert’s tenth problem. In 1900 Hilbert asked for a method that, given any equation with integer coefficients, like $x^3 + y^3 + z^3 = 42$, finds out whether it has a solution in integers. For this equation a solution was found only in 2019, and its numbers have seventeen digits. In 1970 Yuri Matiyasevich, completing the work of Martin Davis, Hilary Putnam and Julia Robinson, proved that no such method exists. Moreover, for any program one can write down a polynomial that has integer roots if and only if the program halts. The halting problem dresses up as an equation.

The word problem. A group can be given by generators and relations, as in the chapter on groups, and one can ask whether a given product of generators equals the identity. In 1955 Pyotr Novikov built a finitely presented group for which this question is undecidable; William Boone did so independently.

Wang tiles. Take a set of square tiles with coloured edges; they can’t be rotated, and adjacent edges must match in colour. Can the whole plane be tiled with them? In 1961 Hao Wang asked whether there’s an algorithm answering this question for any set. In 1966 Robert Berger proved there isn’t. Along the way he built a set of 20,426 tiles that can tile the plane, but only non-periodically; today such a set of just 11 tiles is known.

The busy beaver

Back to machines on a blank tape. Take all the machines with $n$ states and the symbols $0$ and $1$; there are finitely many of them. Some run for ever, the rest halt. Among those that halt, find the one that ran longest.

The function was invented by Tibor Radó in 1962. Its values:

The five-state champion was found by Heiner Marxen and Jürgen Buntrock back in 1989, and it leaves 4098 ones on the tape. The difficulty wasn’t finding it but proving that none of the other five-state machines that halt runs longer. For that, every machine that doesn’t halt had to be dealt with, and for each one it had to be proved that it never halts. Dozens of participants in the open bbchallenge project around the world did this from 2022 to 2024, and the final proof was checked by a computer in the formal proof system Coq.

A two-state beaver: in state $A$ on $0$ it writes $1$, moves right and goes to $B$; on $1$ it writes $1$, moves left and goes to $B$. In state $B$ on $0$ it writes $1$, moves left and goes to $A$; on $1$ it writes $1$, moves right and halts. How many steps does it make on a blank tape, counting the last one?

Follow the tape; brackets mark the head. $A$: $[0] \to 1[0]$, $B$: $\to [1]1$, $A$: $\to [0]11$, $B$: $\to [0]111$, $A$: $\to 1[1]11$, $B$: writes $1$, moves right, halts. $6$ steps in all, with $4$ ones on the tape. Check it in the simulator above.

In the same way one proves that $BB(n)$ eventually overtakes every computable function: if $BB(n) \le f(n)$ for a computable $f$, we’d solve the halting problem by running machines for $f(n)$ steps. And the beaver is linked to incompleteness quite vividly. There are known machines with a few hundred states that halt if and only if a contradiction turns up in the set theory ZFC. If ZFC is consistent, such a machine runs for ever, but by Gödel’s second theorem this can’t be proved in ZFC, and so the corresponding value of $BB$ can’t be computed in it either. Five states turned out to be at the limit of human strength; for a few hundred, the limit is set by a theorem.

The answer to the seventh question

Yes. For any consistent system of axioms that can be written out mechanically and contains arithmetic, there’s a statement about natural numbers that’s true but unprovable in that system (Gödel, 1931). Such statements can even be quite “everyday”: for example, that a certain Turing machine never halts. Unprovability is always relative to a system of axioms; the theorem doesn’t assert any absolute “truth without proof”.

The theorem is often misreported, so let’s note what isn’t in it. It doesn’t say that mathematics is inconsistent or that truth is subjective: it says the exact opposite, $G$ is unambiguously true. It doesn’t say that particular open problems are unprovable: Goldbach’s conjecture or the Riemann hypothesis may well be proved tomorrow. It doesn’t claim that humans are stronger than machines: philosophers argue about that, and the arguments go beyond mathematics. And it doesn’t abolish proof: almost everything mathematicians do is proved in ZFC without any trouble.

And the MIU game now looks prophetic. Inside it you could neither get MU nor understand that it was impossible; the answer came from looking from outside. With arithmetic it’s the same, but with a twist: jumping out of a system into a stronger one, we find ourselves inside a system again, with its own unprovable truths. The ladder never ends.

Where next

Rigour has been pushed to the limit: a proof has become a chain of symbols checked by a machine, and we’ve seen where this road runs into a wall. Now we can allow ourselves the opposite: a geometry in which lengths and angles don’t matter and shapes can be kneaded like modelling clay. A topologist, as the well-known joke goes, can’t tell a coffee mug from a doughnut. Why are a mug and a doughnut “the same”, but a ball and a doughnut not? And what does “the same” even mean if the shapes have different sizes and angles? That’s the chapter on topology.