Chapter 8: Incompleteness

Put yourself back in the schoolroom. The teacher writes on the board the rules for adding, multiplying and taking powers of positive whole numbers, eleven of them:¹

With them you can prove $(x+1{)}^2=x^2+2x+1$, and every other identity you were set as homework. A student at the back asks the obvious question. Do these rules settle every identity that is true of the positive whole numbers? If an equation between two expressions in $x$, $y$, $1$, $+$, $\cdot$ and powers holds whatever numbers are put for the letters, can it always be derived from the eleven?

The question is Tarski’s, and it waited more than a decade for an answer. The answer is no. Here is an identity, found by Wilkie, in which $A=1+x$, $B=1+x+x^2$, $C=1+x^3$ and $D=1+x^2+x^4$:

It is true for every pair of positive whole numbers $x$ and $y$. The reason is a hidden common factor: $C=A\cdot (1-x+x^2)$ and $D=B\cdot (1-x+x^2)$, so that $C^x+D^x$ is $(A^x+B^x)$ times $(1-x+x^2{)}^x$, and in the same way $C^y+D^y$ is $(A^y+B^y)$ times $(1-x+x^2{)}^y$. Both sides are then the same product, written in a different order. But the factor $1-x+x^2$ has a minus sign in it, and the eleven rules have no subtraction. The identity is true, and the rules cannot derive it.

How can anyone know that the rules cannot derive it? Not by trying and failing, since failing to find a derivation proves nothing. The way to show that something does not follow from rules is to exhibit a world in which the rules hold and the claim fails. For Wilkie’s identity the smallest such world has twelve elements, and its tables for addition, multiplication and powers obey all eleven rules. In 2026 a computer proved, with a SAT solver, that no smaller one exists.

Adding Wilkie’s identity to the board does not end the matter: no finite list of identities, however long, derives every true one. There is no last patch.

The schoolroom is a small version of a large hope. For two thousand years Euclid’s geometry was the model of knowledge: a few axioms, and every truth of the subject derived from them. In 1899 Hilbert rewrote the axioms of geometry so that every assumption was written down. He hoped for the same in arithmetic, the study of the counting numbers $0,1,2,\dots$ with addition and multiplication: axioms from which every truth about the numbers could be derived.

In the counting numbers every statement that can be written down is true or false: that is what the definition of truth in a structure says. Goldbach’s conjecture, that every even number greater than $2$ is a sum of two primes, can be written as one sentence of first-order logic. Nobody knows whether it is true or false. If there were axioms from which every true statement about the numbers could be derived, then Goldbach’s conjecture or its negation would be derivable, and settling it would be a matter of searching.

On 8 September 1930, in Königsberg, Hilbert gave an address that ended with the words Wir müssen wissen. Wir werden wissen. (We must know. We shall know.) They are on his grave. On the day before, at a round table at a conference in the same city, a young logician from Vienna, Kurt Gödel, had announced a theorem that showed the hope to be mistaken.

Two questions about theories and programs have been left open so far. They are the questions of this chapter. The first is about searching. The first-order procedure REFUTE (Theorem 7.63) certifies every entailment that holds, and runs for ever on some that do not. Is that a fault of the procedure, which a cleverer search would repair?

The second question is about describing. Even a perfect oracle for “does this follow from the theory?” tells us only what follows from the theory. What we wanted was what is true of the system it describes. The two agree only when the theory says everything about the system: can it always be chosen so? Call the two questions, about searching and about describing, the search gap and the specification gap.

This chapter shows that neither gap can be closed in general, and that one construction answers both questions: the rules by which programs run can be written down as sentences.

The plan has four steps. First, Section 8.1 makes the specification gap precise: a specification captures a structure when it proves exactly the sentences true there, and then a program can decide every question about the structure. Section 8.2 shows that every finite structure can be captured. Second, the search gap. Section 8.3 shows that no program decides whether a program halts, and writes the rules by which programs run as a theory, so that Section 8.4 can carry the result into logic: no program decides first-order validity. Third, the specification gap for the counting numbers. Section 8.5 shows that halting can be expressed in arithmetic, so no program decides arithmetic and no specification captures it, and Section 8.6, the first incompleteness theorem, names, for any sound specification, a true sentence that it does not prove. Fourth, a limit of specifications that does not depend on the structure we meant at all. Section 8.7, the second incompleteness theorem, shows that a consistent specification of arithmetic does not entail its own consistency: some sentences about a specification do not follow from it in first-order logic. The two optional sections prove in full that halting can be expressed (Section 8.8) and ask which infinite structures can be captured (Section 8.9).

8.1 Specifications

We describe a system, a structure $\mathfrak{M}$, by a theory $\mathrm{\Theta }$, and we want the sentences that follow from $\mathrm{\Theta }$ to be exactly the sentences true of $\mathfrak{M}$. To say this precisely we need a name for the set of truths of $\mathfrak{M}$, a condition that makes a theory usable, and a meaning for “exactly”. One fact then makes the question sharp: a theory that does the job lets a program decide the truths of $\mathfrak{M}$.

For every sentence $\phi$, exactly one of $\phi$ and $\mathrm{\neg }\phi$ is in $\mathrm{Th}(\mathfrak{M})$, since $\mathfrak{M}\models \mathrm{\neg }\phi$ exactly when $\mathfrak{M}⊭\phi$: a structure takes a side on every question its language can ask. That is what distinguishes a structure from a theory, which may leave a question open.

A theory has to be one that someone can use. That asks for one thing more than a set of sentences: a program that recognises its members. Until Section 8.3 makes the word exact, a program is anything that could be written in pseudocode: it takes an input, takes steps one at a time, and may or may not stop.

The examples are the sets one would naturally write down.

• A finite set of sentences is a specification: the program compares the given sentence with each of them.

• The equality axioms of a signature that contains $=$ (Definition 6.36 of Chapter 6 defines them for any signature) are a specification. They are (Eq1), which says that everything is equal to itself, and the instances of (Eq2), which say that equals may be put for equals in a formula. There are infinitely many instances, one for each formula, but a program recognises an instance by its shape.

• In the same way, every finite set of sentences together with all the instances of finitely many schemas is a specification.

The definition asks for a program because a theory whose members nobody can recognise is no use as a specification. The point of a derivation from $\mathrm{\Theta }$ is that anyone can check it, and checking it includes checking that its open hypotheses are in $\mathrm{\Theta }$.

The set $\mathrm{Th}(\mathfrak{M})$ is a set of sentences, and so “take all the true ones” looks like the best specification of $\mathfrak{M}$ there could be. Whether it is one depends on whether a program can recognise the true sentences. For the counting numbers it cannot, as Section 8.5 shows. “All the true ones” describes a set; it does not give a checker.

The definition has two halves, of very different weight.

• Only truths: if $\mathrm{\Theta }{⊢}_{\mathrm{NK}}\phi$ then $\mathfrak{M}\models \phi$. When $\mathfrak{M}\models \mathrm{\Theta }$ this half is free, by the soundness of $\mathrm{NK}$.

• Every truth: if $\mathfrak{M}\models \phi$ then $\mathrm{\Theta }{⊢}_{\mathrm{NK}}\phi$. This is the half with content: it asks the theory to settle every question that the structure settles.

A specification that misses a truth does not show that no specification captures the structure. The identities true of the positive integers with $1$, $+$, $\cdot$ and powers can be decided by a program.⁵ So the set of all of them is itself a specification, from which every true identity follows at once. What fails at school is every finite list, the eleven identities in particular. For the counting numbers, with $+$, $\times$ and the quantifiers, no specification at all will do, finite or infinite.

Proving that no specification will do means knowing what any specification can do. It can at least produce its theorems, one after another, because a derivation is a finite string that a checker can read.

procedure LIST                     -- prints the theorems of Theta
    for each string w, shortest first, then in alphabetical order:
        if w is a derivation of NK,
           each open hypothesis of w is in Theta,
           and the conclusion of w is a sentence:
            print the conclusion of w

Proofs are easy to check and hard to find, and a program that checks every candidate finds them all, eventually. The list says nothing about a sentence that is not on it, however long one waits, and that is the whole difficulty.

procedure DECIDE(phi)              -- phi a sentence
    for each theorem psi of Theta, as LIST prints them:
        if psi is phi:                   answer yes
        if psi is the negation of phi:   answer no

A specification that captures a structure turns truth into computation. Read backwards, the theorem is a way to show that a structure cannot be captured:

The theorem has a converse, and together they say that capturing and deciding are the same thing.

What a good specification adds is economy: a short list that a person can write, read and argue about, in place of the list of every truth.

8.2 Finite Structures

Finite structures are the one kind for which the specification gap can always be closed.

On a finite structure, the definition of truth is itself an algorithm: each quantifier runs through the domain, and a sentence with $k$ nested quantifiers on $n$ elements takes about $n^k$ cases. So the truths of a finite structure, for a finite signature, can be decided. A structure whose truths can be decided is captured by the set of all its truths, by the proposition that capturing is deciding, and so every finite structure can be captured.

That specification is the list of all the truths, which is infinite and of no use to anyone. This section shows that a finite list will do, and that it is the list one would write down anyway: give each element a name, and copy out the tables.

The description is finite, since the signature and the domain are. Together with the equality axioms for ${\mathrm{\Sigma }}_{\mathfrak{M}}$, it is therefore a specification.

In words: say who is there, that they are different, that there is nobody else, and every entry of every table; then everything true has been said.

A $\mathrm{\Sigma }$-sentence is true in ${\mathfrak{M}}^{+}$ exactly when it is true in ${\mathfrak{M}}^{+}\upharpoonright \mathrm{\Sigma }=\mathfrak{M}$, so the specification proves exactly the $\mathrm{\Sigma }$-sentences true in $\mathfrak{M}$.

The closure sentence is the one sentence with no counterpart for an infinite structure, since no finite list of names covers infinitely many elements. The other sentences of ${\mathrm{\Delta }}_{\mathfrak{M}}$ describe the elements that are there. The closure sentence says that there are no others, and so tells every model of it where the structure stops. Without it, a model of the remaining sentences may have an extra element, of which the tables say nothing. A sentence true in $\mathfrak{M}$ may then fail at the extra element (Exercise 8.5).

The cost of such a specification is plain. It is as long as the tables of the structure, since it is those tables. It captures that one structure and nothing else. When the system changes, by one new element or one changed entry, the specification is wrong and has to be written again. That is why a system that changes is described not by a table, which says everything about one state alone, but by a theory, which says what must be true of every table the system can produce.

For a system with infinitely many elements no table can be written, and only a theory is left. The rest of the chapter asks whether a theory can ever say everything.

8.3 Programs as Theories

The search gap asks about every procedure, not just about REFUTE. To answer it we need to say exactly what a procedure is, and Chapter 1 has already given an answer: a procedure is a combinator. A term built from $\mathsf{K}$ and $\mathsf{S}$ computes by being rewritten, and the theorem on Turing completeness (Theorem 1.18) says that combinators compute everything that any machine computes.⁷

The plan is short to state. Chapter 1’s four rules for a step, and its lemma on the shape of a normal form, can be written as a handful of first-order sentences, the same handful for every program. Then “the program halts” becomes “a certain sentence follows”. So whatever cannot be decided about programs cannot be decided about sentences either. Whether a program halts, as we show first, is one such thing. That no program decides it is the source of both of the chapter’s answers: Section 8.4 carries it into logic, and Section 8.5 into arithmetic.

The section takes seven things from Chapter 1, and needs nothing else from there.

• Steps. A combinator steps by four rules: ($\mathsf{K}$), which takes $\mathsf{K}PQ$ to $P$; ($\mathsf{S}$), which takes $\mathsf{S}PQR$ to $PR(QR)$; and (${\mathrm{app}}_1$) and (${\mathrm{app}}_2$), which make a step in the function, or in the argument, a step of the whole application. The formula $M⇝N$ says that $M$ steps to $N$. A run is a chain of steps, $M{⇝}^{\ast }N$ says that $M$ runs to $N$, and a combinator that cannot step is in normal form.

• The shape of a normal form (Lemma 1.7). A combinator is in normal form exactly when it is $\mathsf{K}$, $\mathsf{K}N$, $\mathsf{S}$, $\mathsf{S}N$ or $\mathsf{S}N{N}^{\prime }$, where $N$ and $N^{\prime }$ are combinators in normal form.

• One result at most (Corollary 1.8). A term runs to at most one normal form.

• No step is a wrong turn (Corollary 1.9). If $M$ runs to a normal form $N$, then every term that $M$ runs to also runs to $N$.

• The Monster. With $\mathsf{I}:=\mathsf{S}\mathsf{K}\mathsf{K}$ and $\omega :=\mathsf{S}\mathsf{I}\mathsf{I}$, which applies its argument to itself, the Monster is $\mathrm{\Omega }:=\omega \omega$, that is, $\mathsf{S}\mathsf{I}\mathsf{I}(\mathsf{S}\mathsf{I}\mathsf{I})$. It has no normal form: every run of it goes on for ever.

• The numerals. With $\mathsf{B}:=\mathsf{S}(\mathsf{K}\mathsf{S})\mathsf{K}$, the numeral of a number is given by $\underset{―}{0}:=\mathsf{K}\mathsf{I}$ and $\underset{―}{n+1}:=\mathsf{S}\mathsf{B}\underset{―}{n}$. The numeral of $n$ applies its first argument $n$ times to its second: $\underset{―}{n}fx$ runs to $f(f(\cdots (fx)\cdots ))$, with $n$ copies of $f$.

• Turing completeness (Theorem 1.18). The functions on numerals that combinators compute are exactly those that a Turing machine computes.

The booleans are recalled where they are used.

Programs

A program’s input is a combinator too, and the input for a number is its numeral. Chapter 1 wrote the numerals with a bar over the number. This chapter keeps the bar for the numerals of arithmetic, which are terms of first-order logic, and writes the numerals of the combinators with a bar beneath.

A program, in this chapter, is a combinator: a term built from $\mathsf{K}$ and $\mathsf{S}$ by application alone.

In words: a program halts on $n$ when, given the numeral of $n$, it has a result. By the corollary of Chapter 1 that a term has at most one result (Corollary 1.8), the result is then unique.

Halting asks that some run ends, not that every run does. The combinator $\mathsf{K}\mathsf{K}\mathrm{\Omega }$, with $\mathrm{\Omega }$ the Monster, halts: its $\mathsf{K}$ step gives $\mathsf{K}$ at once. But a run that keeps stepping inside $\mathrm{\Omega }$ never ends.⁸

Codes

We want a program to take another program as its input. Inputs are numbers, so we number the programs. A combinator is a finite string, and the string we number is the one with every application bracketed, as in the definition of terms in Chapter 1.

For instance, $\mathrm{str}(\mathsf{K}\mathsf{K})$ is $\mathtt{(}\mathtt{KK}\mathtt{)}$, and $\mathrm{str}(\mathsf{S}\mathsf{K}\mathsf{K})$ is $\mathtt{(}\mathtt{(}\mathtt{SK}\mathtt{)}\mathtt{K}\mathtt{)}$.

For instance, $⌜\mathsf{K}⌝=1$ and $⌜\mathsf{K}\mathsf{K}⌝=3\cdot 5^3+1\cdot 5^2+1\cdot 5+4=409$. Different combinators have different strings, and so different codes. A program can compute the code of a combinator, and the combinator of a code. Base five is a choice: any numbering that a program can compute and undo would serve, and this one is the shortest to describe.

A program given a number as its input may want to ask what the program with that number does. Not every number is a code, so we let the others name a program too, one that never halts.

The second line is a convention, and any program that halts on no input would do as well. So $\mathrm{prog}(⌜M⌝)=M$ for every combinator $M$. The second line gives a program that halts on no input: $\mathsf{K}\mathrm{\Omega }\underset{―}{n}$ steps to the Monster $\mathrm{\Omega }$, which has no normal form, so by the corollary of Chapter 1 that no step is a wrong turn (Corollary 1.9) it has none either.

What a program cannot decide

We borrow one fact about programs from Chapter 1.

The proof of the fact builds $P$ from the pseudocode by a fixed method, instruction by instruction, and we call this $P$ the translation of the pseudocode. Conversely, pseudocode can run a combinator step by step and read off its result; a combinator $M$ answers a yes-or-no question about $m$ and $n$ when $M\underset{―}{m}\underset{―}{n}$ runs to $\mathsf{K}$ (yes) or $\mathsf{K}\mathsf{I}$ (no), Chapter 1’s booleans. So a program may be given in either form. Pseudocode may also take a string as its input, such as a sentence or a derivation: a string over a finite list of symbols is read as a number in a large enough base, just as the string of a combinator is read as its code.

The first thing no program can do is the one that Chapter 1 left open: tell in advance whether a program halts.

procedure P(e)                     -- e a number
    if h says that prog(e) halts on e:
        loop for ever
    else: halt

Figure 8.1 draws the proof as a table. Row $e$ records, for each input $n$, whether $\mathrm{prog}(e)$ halts on $n$ (marked $✓$) or runs for ever (marked $\mathrm{\infty }$); the entries shown are made up, but every program has a row. The program $P$ runs down the diagonal and does the opposite of each entry it finds there. So its row differs from row $e$ in column $e$, for every $e$, and it is no row of the table. Yet $P$ has a code $p$, and its row is row $p$. At the entry in row $p$ and column $p$, the two would have to differ from each other, which is the contradiction of the proof.

Computation as a theory

The halting theorem is about combinators. To carry it into logic, we write Chapter 1’s rules for a step as sentences. The sentences talk about combinators, so their signature has the constants $\mathsf{K}$ and $\mathsf{S}$ and a two-place function symbol for application. We write that symbol as application is written, by putting its two arguments side by side and grouping to the left, so that a combinator is also a closed term of the signature. A relation symbol $\mathsf{Step}(x,y)$ will say that $x$ steps to $y$, a relation symbol $\mathsf{Nf}(x)$ that $x$ is in normal form, and a relation symbol $\mathsf{Halts}(x)$ that $x$ halts. Call this signature ${\mathrm{\Sigma }}_{\mathrm{KS}}$: the constants $\mathsf{K}$ and $\mathsf{S}$, the function symbol for application, the two-place relation symbol $\mathsf{Step}$, and the one-place relation symbols $\mathsf{Nf}$ and $\mathsf{Halts}$.

In words: the first group is Chapter 1’s four rules for a step, each bar read as an implication, so that a rule with nothing above the bar is a sentence on its own. The second group is the lemma on the shape of a normal form (Lemma 1.7), for combinators, read from right to left: a term of one of the shapes it lists, with its parts in normal form, is in normal form. The third says that a term halts if it is in normal form already, or if it steps to a term that halts.

For a combinator $M$, write ${\eta }_M$ for the sentence $\mathsf{Halts}(M)$, which says that $M$ halts.

The sentences for normal forms name five shapes. The obvious shortcut, $(\mathsf{Nf}(x)\wedge \mathsf{Nf}(y))\to \mathsf{Nf}(xy)$, is left out, and for a good reason: it would make $\mathsf{K}\mathsf{K}\mathsf{K}$ normal, since $\mathsf{K}\mathsf{K}$ and $\mathsf{K}$ are, and $\mathsf{K}\mathsf{K}\mathsf{K}$ steps to $\mathsf{K}$. Two normal parts make a normal whole only when the whole is not a redex, and the three shapes that are applications, $\mathsf{K}x$, $\mathsf{S}x$ and $\mathsf{S}xy$, are exactly the ways of avoiding one.

Two features of the definition are deliberate. The theory has no symbol for “runs to”: halting is passed back along a run one step at a time, which keeps every sentence short. And the theory is the same for every program. Only ${\eta }_M$ mentions $M$, because every combinator runs by the same four rules: the program is the term, not a list of instructions.

Example 8.22 (the theory at work). The program $\mathsf{I}\mathsf{K}$, that is, $\mathsf{S}\mathsf{K}\mathsf{K}\mathsf{K}$, halts in two steps:

$$\mathsf{S}\mathsf{K}\mathsf{K}\mathsf{K}⇝\mathsf{K}\mathsf{K}(\mathsf{K}\mathsf{K})⇝\mathsf{K}.$$

In any model of ${\mathrm{\Theta }}_{\mathrm{KS}}$, its sentences force these lines, one by one:

$$\begin{array}{rlrl}& \mathsf{Step}(\mathsf{S}\mathsf{K}\mathsf{K}\mathsf{K},\mathsf{K}\mathsf{K}(\mathsf{K}\mathsf{K}))& & \text{the }\mathsf{S}\text{ sentence, at }\mathsf{K}\text{, }\mathsf{K}\text{, }\mathsf{K}\\ & \mathsf{Step}(\mathsf{K}\mathsf{K}(\mathsf{K}\mathsf{K}),\mathsf{K})& & \text{the }\mathsf{K}\text{ sentence, at }\mathsf{K}\text{, }\mathsf{K}\mathsf{K}\\ & \mathsf{Nf}(\mathsf{K})& & \text{normal forms, the first sentence}\\ & \mathsf{Halts}(\mathsf{K})& & \text{halting, the first sentence}\\ & \mathsf{Halts}(\mathsf{K}\mathsf{K}(\mathsf{K}\mathsf{K}))& & \text{halting, the second, with lines 2 and 4}\\ & \mathsf{Halts}(\mathsf{S}\mathsf{K}\mathsf{K}\mathsf{K})& & \text{halting, the second, with lines 1 and 5.}\end{array}$$

The last line is ${\eta }_{\mathsf{I}\mathsf{K}}$, so ${\mathrm{\Theta }}_{\mathrm{KS}}\models {\eta }_{\mathsf{I}\mathsf{K}}$. The first two lines are the run, the third recognises its result as a normal form, and the last three pass that result back to its start:

The main lemma of this section says that the sentences describe running in just the sense needed: a program $M$ halts exactly when ${\eta }_M$ follows from ${\mathrm{\Theta }}_{\mathrm{KS}}$.

In words: a program halts exactly when the sentence “it halts” follows from the sentences that describe computation.

Since ${\mathrm{\Theta }}_{\mathrm{KS}}$ is a set of sentences, the soundness and completeness of $\mathrm{NK}$ let us read the lemma with ${\mathrm{\Theta }}_{\mathrm{KS}}{⊢}_{\mathrm{NK}}{\eta }_M$ in place of ${\mathrm{\Theta }}_{\mathrm{KS}}\models {\eta }_M$: a program halts exactly when a derivation exists.

We call the structure $\mathfrak{T}$ of the second half the term structure. Its domain is the set of closed terms of ${\mathrm{\Sigma }}_{\mathrm{KS}}$ and each of them means itself, as in the term structure of Chapter 6 (Definition 6.64), but its relations are chosen by what the combinators do, not by a set of sentences. It is a Herbrand structure, in the sense of Chapter 7, and it satisfies ${\mathrm{\Theta }}_{\mathrm{KS}}$.

The first half of the proof shows that every model of ${\mathrm{\Theta }}_{\mathrm{KS}}$ makes $\mathsf{Halts}$ true of each combinator that halts. It shows nothing about the other combinators, and such a structure may well be more generous: Exercise 8.8 has one in which every combinator halts. The term structure is the least generous, since it makes $\mathsf{Halts}$ true of the combinators that halt and of nothing else. That is why the second half uses it.

When $M$ halts, the facts that establish ${\eta }_M$ follow its run step by step, and each of them is forced: it is the one literal left in an instance of a sentence of ${\mathrm{\Theta }}_{\mathrm{KS}}$ once the others are established (Example 8.22 lists them for $\mathsf{I}\mathsf{K}$). So a procedure that sets forced literals, as DPLL does, can find them by itself. The sentences of ${\mathrm{\Theta }}_{\mathrm{KS}}$, and the negation of ${\eta }_M$, each have a clause form of one clause: drop the quantifiers and write each implication as a disjunction. Every one of these clauses has at most one positive literal: they are Horn clauses, the kind a logic program is made of (Remark 8.25). Give ${\mathrm{\Theta }}_{\mathrm{KS}}\cup \{\mathrm{\neg }{\eta }_M\}$ to the first-order procedure REFUTE (Theorem 7.63): by that theorem and the lemma that a program is a theory, it returns UNSAT exactly when $M$ halts, and on the Monster it runs for ever.

step(app(app(k,X),Y), X).
step(app(app(app(s,X),Y),Z), app(app(X,Z),app(Y,Z))).
step(app(X,Y), app(X1,Y)) :- step(X,X1).
step(app(X,Y), app(X,Y1)) :- step(Y,Y1).
nf(k).  nf(s).  nf(app(k,X)) :- nf(X).  nf(app(s,X)) :- nf(X).
nf(app(app(s,X),Y)) :- nf(X), nf(Y).
halts(X) :- nf(X).
halts(X) :- step(X,Y), halts(Y).

8.4 Undecidability of First-Order Logic

The lemma that a program is a theory turns a question about a program into a question about a sentence, by a map that a program can compute. That is all it takes to move the undecidability of halting from programs to logic, and so to settle the first of the chapter’s two questions, the search gap.

In words: no algorithm decides first-order logic, not even for the sentences that say something as plain as “this program stops”. The signature is small, and a larger one does not help: a program for a larger signature would decide, in particular, the sentences of ${\mathrm{\Sigma }}_{\mathrm{KS}}$, whose validity does not depend on symbols they do not mention.

The proof has a shape that fits any question about programs. To show that no program answers some question, show how a program could turn every question “does $\mathrm{prog}(e)$ halt on $n$?” into a question of the new kind with the same answer. A program for the new question would then answer every halting question, and no program does. Such a map is called a reduction: the one here sent $(e,n)$ to ${\theta }_{\mathrm{KS}}\to {\eta }_{M\underset{―}{n}}$, where $M=\mathrm{prog}(e)$. The hard part of each such proof is always the same, checking that the answers agree, and here it was the lemma that a program is a theory.

The same reduction gives the other forms of the question at once.

In (i) the set $\mathrm{\Gamma }$ never changes: the proof uses the same ${\mathrm{\Theta }}_{\mathrm{KS}}$ for every program. So there is one finite set of sentences whose consequences no program decides.

This settles the search gap. The first-order procedure certifies every entailment that holds, and may never answer for one that fails; the search gap asked whether a cleverer search could always stop, and part (iii) of the corollary says that none can.

The procedure REFUTE stops on every unsatisfiable clause set (Theorem 7.63), and so does REFUTE-U, which chooses its instances by unification (Proposition 7.98, from the optional Section 7.8; only its statement is used here). A procedure that also stopped on every satisfiable set would decide satisfiability, and there is no such procedure. Whatever a cleverer search gains, and unification gains a great deal, it cannot gain the other half of the answer. When the procedure runs for ever on a satisfiable set, that is not a defect of the procedure: no procedure could do better.

The valid sentences therefore form a set of a particular kind: one that has a semi-decision procedure (Definition 7.64), and so can be listed, but cannot be decided.¹² They can be listed: negate every sentence, put each negation in clause form and run REFUTE on all of them at once, interleaving the runs; then print each sentence whose run closes. Every valid sentence is printed sooner or later. But they cannot be decided, by the theorem that validity is undecidable. The listing shows where the difficulty lies: a sentence that is not valid is never printed, and no amount of waiting tells it apart from one that has not been printed yet. Membership can be confirmed, and non-membership in general cannot.

8.5 Arithmetic as a Theory

The structure that the founders of modern logic most wanted to capture is the oldest one in mathematics: the counting numbers. We want to know whether some specification captures them. By the theorem that capturing makes truth decidable, it is enough to show that no program decides their truths, and the reduction that worked for validity works again, once halting can be expressed as a sentence about numbers. So what is left is to fix the language, and to express halting in it. The language is that of the counting numbers in Chapter 6, with equality added, since without it the language could not even say $x+y=y+x$.

The language has no symbol for $1$, or for $7$. It does not need one, since it can count.

So $\bar{3}$ is $s(s(s(0)))$, and in general $\bar{n}$ has $n$ copies of $s$. Its value in $\mathfrak{N}$ is $n$, by induction on $n$.

The structure cannot be written out as a table, since its domain is infinite: it can only be described by a theory.

The language is small, but it says a great deal. Write $x\mid y$ for $\mathrm{\exists }z(x\times z=y)$, “$x$ divides $y$”, and

With these abbreviations, the sentence $\mathrm{\forall }x\mathrm{\exists }p(x<p\wedge \mathit{Prime}(p))$ says that there are infinitely many primes, which is true. The sentence

is Goldbach’s conjecture. A specification that captured $\mathfrak{N}$ would derive it or its negation, and the same holds for most open problems of number theory, which can be written in this language too.

The obvious candidate

Every course on arithmetic starts from the axioms of Peano arithmetic.

The first group describes the successor, the second and third say how $+$ and $\times$ compute, and the fourth defines the order. The fifth is proof by induction, with one axiom for each property it might be applied to.

A program recognises an induction axiom by its shape, so $\mathrm{PA}$ is a specification, and $\mathfrak{N}\models \mathrm{PA}$. It proves a great deal: very nearly every theorem of elementary number theory that has ever been proved can be derived in it. The question is whether it, or anything like it, proves every true sentence.

Saying things about programs

To express halting we need to say what it is for a formula to express a relation between numbers. The notion is the plainest one there is.

The even numbers are definable, by $\mathit{Even}(x)$, and so are the primes and the pairs $(x,y)$ with $x\mid y$.

Definability is a matter of truth in $\mathfrak{N}$, and says nothing about proofs. A formula that defines a set is true of its members. Whether any specification can prove it true of them is a different question, about the specification. The notion that asks for proofs has a name of its own, representability, and the main line of this chapter never uses it. Section 8.7 needs two facts about what $\mathrm{PA}$ proves, and states them.

From now on a program is referred to by its code, and its input is a number. In this form halting is undecidable, by the theorem of Section 8.3: no program decides, given the numbers $e$ and $n$, whether $\mathrm{prog}(e)$ halts on $n$.

The idea of the proof

The proof is in the optional Section 8.8, and here is how it goes. A halting run is finite: a list of combinators $M_0⇝M_1⇝\cdots ⇝M_N$, where $M_0$ is the program applied to the numeral of its input and $M_N$ is in normal form. Each combinator is a string of the four symbols $\mathtt{K}$, $\mathtt{S}$, $\mathtt{(}$ and $\mathtt{)}$, and so, read as in its code, a list of the digits $1$ to $4$. So a halting run is a finite table of numbers, one row for each combinator.

The one idea of the proof is that a finite table of numbers can be packed into two numbers $a$ and $b$, with the entry at position $i$, counting from $0$, the remainder of $a$ on division by $1+(i+1)b$. (A run needs a few such pairs, for the lengths of the rows as well as their digits; the sketch speaks of one.) A remainder is expressed by $+$ and $\times$: “$r$ is the remainder of $a$ on division by $m$” is $\mathrm{\exists }q(a=q\times m+r\wedge r<m)$.

So $H(x,y)$ can say: there are numbers $N$, $a$ and $b$ whose table has, in its first row, the string of the program with code $x$ applied to the numeral of $y$; in each later row, the string of a combinator one step from the row before; and, in its last row, a normal form. One step replaces a stretch of the form $\mathtt{(}\mathtt{(}\mathtt{K}P\mathtt{)}Q\mathtt{)}$ by $P$, or one of the form $\mathtt{(}\mathtt{(}\mathtt{(}\mathtt{S}P\mathtt{)}Q\mathtt{)}R\mathtt{)}$ by $\mathtt{(}\mathtt{(}PR\mathtt{)}\mathtt{(}QR\mathtt{)}\mathtt{)}$, and a normal form has no such stretch. Each of those conditions talks only about digits at positions in the table, that is, about remainders, that is, about $+$ and $\times$.

Since halting is definable, the undecidability of halting moves from programs to the counting numbers by a reduction, as it moved to validity.

So $\mathrm{Th}(\mathfrak{N})$, the set of all true sentences of arithmetic, is not a specification: “take all the true ones” gives no checker. And $\mathrm{PA}$, in particular, misses some truth.

The contrast with school algebra is now exact. The identities true of the positive integers, with $1$, $+$, $\cdot$ and powers, can be decided, so they form a specification. Only the finite lists of them fail. For arithmetic, no list a program can read will do, and that is a theorem.

8.6 First Incompleteness Theorem

The corollary says that a specification of arithmetic misses a truth, and gives no idea which. We want to name one. The specification is assumed to tell the truth, and the sentence will come from a program that watches the specification at work.

Here the word names a property of a specification. It should not be confused with the soundness of $\mathrm{NK}$, a property of the proof system: whatever $\mathrm{NK}$ derives from true premisses is true. The two are connected: by the soundness of $\mathrm{NK}$, a specification $\mathrm{\Theta }$ is sound exactly when $\mathfrak{N}\models \mathrm{\Theta }$. In particular, $\mathrm{PA}$ is sound, and so is every specification obtained from it by adding true sentences.

The program waits for the specification to say that some program does not halt on its own code.

procedure D(e)                     -- e a number
    for each theorem phi of Theta, as LIST prints them:
        if phi is  not H(e, e),  e written as a numeral:  halt

In words: on the input $e$, the program waits for $\mathrm{\Theta }$ to prove that $\mathrm{prog}(e)$ does not halt on $e$, and halts if that ever happens. The interesting input is the program’s own code.

The proof used three things: that $\mathrm{\Theta }$ is sound, that its theorems can be listed, and that halting is definable. It used no particular axioms of arithmetic, and no fact about what any specification proves, beyond what $\mathrm{\Theta }$’s own soundness gives.

Figure 8.2 draws the theorem. Among the sentences of ${\mathrm{\Sigma }}_{\mathrm{A}}$, the theorems of a sound $\mathrm{\Theta }$ lie inside the truths. The sentence $\mathrm{\neg }H(\bar{d},\bar{d})$ lies in the gap between them, and its negation is false, so $\mathrm{\Theta }$ proves neither. Adding the sentence to $\mathrm{\Theta }$ widens the theorems to take it in, but the wider specification is again sound and has its own diagonal program, whose sentence lies in the new gap. There is no last patch.

The theorem has two hypotheses on $\mathrm{\Theta }$, that it is a specification and that it is sound. Both are needed, and an example shows each.

• A specification. The set $\mathrm{Th}(\mathfrak{N})$ proves exactly the truths, so it leaves no truth unproved. No program lists it, since a listing would decide truth in $\mathfrak{N}$ by waiting for $\phi$ or $\mathrm{\neg }\phi$, and no program decides truth in $\mathfrak{N}$. So it is not a specification, and its diagonal program cannot be written.

• Sound. A specification that contains a sentence and its negation proves every sentence, by ($\to$E) and ($\mathrm{\perp }$E), and so it proves $\mathrm{\neg }H(\bar{d},\bar{d})$. It is a specification, and not sound.

8.7 Second Incompleteness Theorem

The first incompleteness theorem measured a specification against the structure we meant: some truth about $\mathfrak{N}$ does not follow from it. This section finds a limit of another kind, which does not mention $\mathfrak{N}$ at all. Hilbert’s programme, the plan to secure mathematics by formal axioms, asked that the axioms should never contradict themselves, a property of derivations and not of truth, and that arithmetic should prove this about itself. We want to know whether a specification can. It cannot: a consistent specification that contains $\mathrm{PA}$ does not prove the sentence that says it is consistent, and so, by the completeness of $\mathrm{NK}$, that sentence does not follow from it.

The route has two steps. The first theorem assumed that $\mathrm{\Theta }$ is sound, a strong assumption: to know that a theory proves nothing false about the counting numbers, one has to know which sentences about them are true, and that is what no specification can tell us. So we first replace soundness by consistency, at the cost of one fact about what $\mathrm{PA}$ proves. Then we carry the proof of the first theorem out inside $\mathrm{PA}$, which is one more fact.

Consistency is the property of Definition 6.53: a set of sentences $\mathrm{\Theta }$ is consistent if $\mathrm{\Theta }{⊬}_{\mathrm{NK}}\mathrm{\perp }$. In words: the theory never leads to a contradiction. Equivalently, there is no sentence $\phi$ with both $\mathrm{\Theta }{⊢}_{\mathrm{NK}}\phi$ and $\mathrm{\Theta }{⊢}_{\mathrm{NK}}\mathrm{\neg }\phi$, since ($\to$E) turns such a pair into $\mathrm{\perp }$ and ($\mathrm{\perp }$E) turns $\mathrm{\perp }$ into anything. The definition mentions derivations alone, and no structure.

A sound specification is consistent, since $\mathfrak{N}⊭\mathrm{\perp }$. The converse fails (Remark 8.51).

To trade soundness for consistency, we need one fact about what $\mathrm{PA}$ can prove: that it can check a finished calculation.

The reason is that a halting run is a finite calculation. If the program halts, there are particular numbers $N$, $a$ and $b$ that pack its run, and $H(\bar{e},\bar{n})$ follows by ($\mathrm{\exists }$I) from the claim that these numbers do so. That claim comes down to a check of each of finitely many rows, and each check to facts about particular numbers, such as $\overline{80}=\overline{26}\times \bar{3}+\bar{2}$. A check is finite because every “for all” in $H$ can be written to range only over the numbers below a given one. The specification $\mathrm{PA}$ proves each such fact by calculating with its equations, as a pupil checks a long division. We take the details on loan.¹⁵

In words: for a specification that contains $\mathrm{PA}$, consistency is enough in place of soundness.

The proof shows the price of the weaker assumption. A consistent specification that is not sound might prove the false sentence $H(\bar{d},\bar{d})$, and nothing in the argument forbids it. So the theorem cannot say that $\mathrm{\Theta }$ leaves the question open either way.

Consistency as a sentence

Whether $\mathrm{\Theta }$ is consistent is a question about a program: the one that waits for $\mathrm{\perp }$.

procedure C(e)                     -- the input is ignored
    for each theorem phi of Theta, as LIST prints them:
        if phi is bottom:  halt

The specification $\mathrm{\Theta }$ is consistent exactly when $C_{\mathrm{\Theta }}$ never halts, whatever its input, and so, by the definability lemma, exactly when $\mathfrak{N}\models {\mathrm{Con}}_{\mathrm{\Theta }}$. In words, ${\mathrm{Con}}_{\mathrm{\Theta }}$ says “$\mathrm{\Theta }$ is consistent” in the language of arithmetic. The programme hoped for a derivation of such a sentence from axioms everyone accepts.

The definition asks for the translation of $C_{\mathrm{\Theta }}$, and not for any combinator that halts on the same inputs. When $\mathrm{\Theta }$ is consistent, $C_{\mathrm{\Theta }}$ halts on no input, like every combinator that never halts. For some of those, such as the translation of “loop for ever”, $\mathrm{PA}$ proves that they never halt, and with such a code in place of $c$ the sentence would be provable. The sentence must speak of the program that actually searches the theorems of $\mathrm{\Theta }$.

The second incompleteness theorem needs one more fact on loan, and of the facts the chapter borrows it is the longest to check. The proof of the first incompleteness theorem from consistency is an argument about numbers and programs. In particular it shows that if $\mathrm{\Theta }$ is consistent, then the diagonal program of $\mathrm{\Theta }$ does not halt on its own code $d$. That argument can be carried out inside $\mathrm{PA}$.

Written with ${\mathrm{Con}}_{\mathrm{\Theta }}$ in place of “$\mathrm{\Theta }$ is consistent”, the argument uses only the definitions of the programs $D_{\mathrm{\Theta }}$ and $C_{\mathrm{\Theta }}$, the fact that true halting is provable, and the step from a sentence and its negation to $\mathrm{\perp }$. What has to be checked is that $\mathrm{PA}$ can prove each of these about the formula $H$. That check is long and is omitted by most textbooks.¹⁷

In words: a consistent specification of arithmetic cannot prove its own consistency.

By the completeness of $\mathrm{NK}$, it follows that $\mathrm{\Theta }⊭{\mathrm{Con}}_{\mathrm{\Theta }}$: some model of $\mathrm{\Theta }$ makes ${\mathrm{Con}}_{\mathrm{\Theta }}$ false. So this is a limit on what a specification entails, and not only on how well it fits $\mathfrak{N}$.

8.8 Defining Halting (optional)

This section is optional. It proves the lemma that halting is definable in $\mathfrak{N}$, which the main line used with only a sketch of its proof, and it shows that the formula can be written with every universal quantifier bounded, the form the fact that true halting is provable needs. The main line uses these results, not their proofs.

The proof has two parts. The first is a fact about numbers: a finite sequence of numbers can be packed into two numbers, from which each entry is recovered as a remainder. The second lays the run out as a table of strings, one for each combinator of the run, and uses the packing to write a formula that says “there is a halting run”.

Each part comes down to one picture. The first: the list $2,0,3$ is stored in the single number $80$, as its remainders on division by $3$, $5$ and $7$ ($80=26\times 3+2=16\times 5+0=11\times 7+3$), and any finite list can be stored in this way. The second: a step of a run copies most of one row of the table into the next, and changes one stretch of it (Figure 8.3). A reader who wants only the idea of the proof can stop here; the rest of the section checks that both pictures can be written as formulas of arithmetic.

Packing a sequence

Write $\mathrm{rem}(a,m)$ for the remainder of $a$ on division by $m$, for $m\ge 1$. The packing uses the function

called Gödel’s $\beta$-function. One fact from elementary number theory is needed, and we prove it.

In words: when the divisors share no factor, the remainders can be chosen independently of one another, and some number has all of them. (With the divisors $2$ and $4$ they cannot: no number leaves remainder $0$ on division by $2$ and $1$ on division by $4$.)

In words: any finite list of numbers, however long, can be stored in two numbers, and read back one entry at a time by taking remainders.

The formula

The function $\beta$ is definable: $\beta (a,b,i)=v$ exactly when $\mathfrak{N}$ makes true