9Incompleteness

In this chapter, we’re going to prove several versions of Gödel’s First Incompleteness Theorem. We’re also going to prove Tarski’s Theorem on the undefinability of truth, and Church’s Theorem on the undecidability of first-order logic.

9.1Preview

In Chapter 4, we studied axiomatic theories. The aim of axiomatizing an area of mathematics (or other discipline) is to put it on a firm foundation: instead of relying on a hodgepodge of intuition and imperfectly understood techniques, all results in the area should be derivable by pure logic from a set of precise and explicitly stated assumptions: the axioms.

What should we expect of an axiomatic theory? Obviously, all the axioms should be true on their intended interpretation. Ideally, they should suffice to derive all truths in the relevant area. These are semantic properties of theories, related to their intended interpretation. But they entail syntactic properties. If all axioms of a theory are true, the theory must be consistent: it won’t contain a sentence \(A\) and its negation \(\neg A\); equivalently, it won’t contain \(\bot \). If a theory contains all truths on its intended interpretation, it will be complete in the sense that for every sentence \(A\) in its language, it contains either \(A\) or \(\neg A\).

Note that this is not the sense of ‘complete’ in which the first-order calculus is complete. When we talk about completeness of a proof system, we mean that the system can prove every valid sentence. When we talk about completeness of a theory, we mean that the theory decides every sentence: it contains \(A\) or \(\neg A\), for every sentence \(A\). (This notion of completeness is sometimes called negation-completeness.)

Confusingly, ‘sound’ also has two meanings. A proof system is sound if it can only prove valid sentences. A theory is called sound if all sentences in the theory are true on their intended interpretation.

Consistency and completeness are defined syntactically, without reference to the meaning of the axioms. This makes them easier to study formally than semantic properties like soundness, which requires pinning down the intended interpretation independently of the proposed axioms, so that one can compare what the axioms say with the structure they are meant to describe.

Consistency may seem trivial: surely nobody would propose an inconsistent set of axioms? But remember that this is exactly what happened to Frege. It also happened to others, especially when trying to develop powerful systems to unify diverse areas of mathematics. Many mathematicians were therefore wary of ZFC when it was first proposed. Couldn’t it also turn out to be inconsistent?

David Hilbert saw how such fears could be put to rest. To check whether an axiomatic theory is consistent, we only need to check whether there is deduction of \(\bot \) from its axioms. Even if the theory itself, like ZFC, talks about highly infinitary matters, any deduction from its axioms is finite. We should therefore be able to establish the consistency of ZFC in a much weaker, finitary branch of mathematics that doesn’t study sets, but proofs and deductions. In the same way, Hilbert hoped that we could prove the completeness of axiomatic theories: we should be able to verify (as seemed plausible in the 1920s) that the axioms of, say, Peano Arithmetic or ZFC decide every sentence in their language.

This project for establishing the consistency and completeness of axiomatic theories is known as Hilbert’s program. It was shattered by Gödel’s incompleteness theorems. Gödel showed that sufficiently strong axiomatic theories can never be complete, unless they are inconsistent. He also showed that there is no hope of establishing the consistency of sufficiently strong theories from safe, finitary grounds. In the present chapter, we’ll focus on the first of these results. We’ll turn to the second in Chapter 10.

Gödel realized that we don’t need a separate branch of mathematics to study proofs. Since sentences and deductions are finite strings of symbols, they can be coded as numbers. We can therefore use arithmetical theories to reason indirectly about proofs. We can, for example, construct an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) so that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(\overline {n})\) is true (in the standard model of arithmetic \(\mathfrak {N}\)) iff there is a deduction of the sentence coded by \(n\) from the axioms of Peano Arithmetic.

Gödel then showed how to construct a sentence \(G\), coded by some number \(n\), such that \(G \leftrightarrow \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(\overline {n})\) is true in \(\mathfrak {N}\). Informally, \(G\) says of itself that it is not provable (in PA): it is true iff it is unprovable. It swiftly follows that PA can’t decide \(G\), assuming that PA is sound. To see this, note first that \(G\) is true: if it were false, it would be provable (because \(G\) is true iff it is unprovable), and so PA would prove a falsehood, contradicting the assumption that PA is sound. So \(G\) is true. And so \(G\) can’t be proved in PA (because \(G\) is true iff it is unprovable). Its negation \(\neg G\) can’t be proved either, as otherwise PA would prove a falsehood.

This argument assumes that PA is sound. For that reason, it is known as the “semantic” version of the First Incompleteness Theorem. Gödel’s main result is a “syntactic” version of the theorem that doesn’t require soundness. In its standard formulation, it shows that every consistent axiomatic theory that is at least as strong as Q is incomplete.

The restriction to axiomatic theories is crucial. Consider the theory \(\mathrm {Th}(\mathfrak {N})\) consisting of all \(\mathfrak {L}_A\)-sentences that are true in the standard model of arithmetic \(\mathfrak {N}\). This theory is complete: every \(\mathfrak {L}_A\)-sentence is either true or false in \(\mathfrak {N}\); if true, it is in \(\mathrm {Th}(\mathfrak {N})\); if false, its negation is in \(\mathrm {Th}(\mathfrak {N})\). By definition, \(\mathrm {Th}(\mathfrak {N})\) is also sound, and therefore consistent. But it is not an axiomatic theory: I haven’t specified \(\mathrm {Th}(\mathfrak {N})\) by giving a set of axioms, and the Incompleteness Theorem implies that I couldn’t have done so.

Officially, theories are just sets of sentences closed under first-order consequence. The same set of sentences can always be specified in many ways. Instead of speaking of axiomatic theories, we should therefore speak of axiomatizable theories. Recall that a theory is axiomatizable if there is a decidable set of axioms from which all and only the sentences in the theory can be deduced: a set of axioms for which there is a mechanical algorithm to check whether a given sentence is in it or not.

The syntactic version of Gödel’s First Incompleteness Theorem can now be stated as follows: every consistent and axiomatizable theory of arithmetic that is at least as strong as Q is incomplete.

9.2Arithmetization of syntax

As I mentioned above, Gödel’s proof draws on the insight that we can use arithmetical theories like PA to reason about their own syntax. After the work we’ve done in the previous chapter, this should not be surprising. We’ve shown in Theorem 8.5 that every computable property or relation is expressible in \(\mathfrak {L}_A\). Syntactic properties like coding an \(\mathfrak {L}_A\)-sentence or coding a deduction from the axioms of PA are clearly computable; so they are expressible in \(\mathfrak {L}_A\): there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(x,y)\) such that \({\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(\overline {n},\overline {m})\) is true (in \(\mathfrak {N}\)) iff \(n\) codes a proof of the sentence coded by \(m\) from the axioms of PA. This is all we need to run Gödel’s argument. To fix ideas, I’ll nonetheless fill in some more details.

We want to talk about sentences and deductions in the language \(\mathfrak {L}_A\), whose non-logical symbols are \(0\), \(s\), \(+\), and \(\times \). To this end, we code \(\mathfrak {L}_A\)-strings as numbers, so that we can indirectly refer to an \(\mathfrak {L}_A\)-string by the \(\mathfrak {L}_A\)-numeral of its code. We’ll use Gödel’s own coding scheme, which I introduced in Section 5.5.

We first assign a symbol code to each primitive symbol of \(\mathfrak {L}_A\), like so:

(\(a_1, a_2, \ldots \) are the “eigenvariables” of \(\mathfrak {L}_A\); see the comments at end of Section 2.4. They will play no role in what follows.)

Next, we use the prime exponent method to code sequences of symbol codes, and thereby \(\mathfrak {L}_A\)-strings. The string ‘\(0 = 0\)’, for example, determines the sequence of symbol codes \(\langle 1, 5, 1 \rangle \), which is coded as \(2^{1} \cdot 3^{5} \cdot 5^{1} = 2430\). The exponents of the primes are the symbol codes. In general, if \(p_i\) is the \(i\)th prime number then the code number of an \(\mathfrak {L}_A\)-string \(A\) composed of symbols \(s_1s_2\ldots s_n\) with symbol codes \(c_1, c_2, \ldots , c_n\) is \[ \gln {A} = p_1^{c_1} \cdot p_2^{c_2} \cdot \ldots \cdot p_n^{c_n}. \] From now on, we’ll call \(\gln {A}\) the Gödel number of \(A\). Note that individual symbols of \(\mathfrak {L}_A\) have both a Gödel number and a symbol code: ‘\(\to \)’ has symbol code 7 and Gödel number \(2^{7} = 128\). We won’t talk about symbol codes any more.

Since deductions are finite sequences of \(\mathfrak {L}_A\)-sentences, we can use the prime exponent method again to code them: the Gödel number of a deduction \(A_1, A_2, \ldots , A_n\) is \[ \gln {A_1, A_2, \ldots , A_n} = p_1^{\gln {A_1}} \cdot p_2^{\gln {A_2}} \cdot \ldots \cdot p_n^{\gln {A_n}}. \]

The Gödel number function \(\#\) converts any \(\mathfrak {L}_A\)-string \(A\) into a number \(\gln {A}\). This number \(\gln {A}\) is denoted in \(\mathfrak {L}_A\) by some numeral \(\overline {\gln {A}}\). So we can indirectly refer to any \(\mathfrak {L}_A\)-string \(A\) by the numeral \(\overline {\gln {A}}\) of its Gödel number.

We’ll abbreviate \(\overline {\gln {A}}\) as \(\ulcorner A \urcorner \). For example, since \(\gln {0\!=\!0} = 2430\), \(\ulcorner 0\!=\!0 \urcorner \) is \(\overline {2430}\), which is \(s(s(\ldots s(0)\ldots ))\) with 2430 occurrences of \(s\). In practice, you should treat the corner quotes as a special kind of quote marks: we use \(\ulcorner 0\!=\!0 \urcorner \) to denote the string ‘\(0\!=\!0\)’ via its Gödel number.

Now consider a simple syntactic property: being a variable. In our coding scheme, variables have Gödel numbers \(2^{12}, 2^{14}, 2^{16}, \ldots \). That is, a number \(n\) codes a variable iff \(n = 2^{12 + 2y}\), for some \(y\). This is a purely arithmetical property that can be expressed in \(\mathfrak {L}_A\): there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\) such that \({\scriptstyle \class {smallcaps}{\text {VAR}}}(\overline {n})\) is true (in \(\mathfrak {N}\)) iff \(n\) codes a variable. In this sense, \({\scriptstyle \class {smallcaps}{\text {VAR}}}(\overline {n})\) “says that” \(n\) codes a variable. But what it actually, explicitly says is simply that there is a number \(y\) such that \(n = 2^{12 + 2y}\).

In the terminology of the previous chapter, the formula \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\) expresses the property of coding a variable. By Theorem 8.5, every computable relation and function is expressible in \(L_A\). We can use this result to show that a wide range of syntactic notions are expressible in \(L_A\). Since our coding scheme can be implemented mechanically, it maps every computable relation or function on \(\mathfrak {L}_A\)-strings to a computable relation or function on \(\mathbb {N}\). By the Church-Turing Thesis, that relation or function is computable. By Theorem 8.5, it is expressible in \(L_A\).

For example, there is a mechanical procedure for checking whether a given string is a well-formed sentence of \(\mathfrak {L}_A\). So there is also a mechanical procedure for checking whether a given number is the Gödel number of an \(\mathfrak {L}_A\)-sentence. So the property (call it \(\mathrm {Sent}\)) of coding an \(\mathfrak {L}_A\)-sentence is computable. By Theorem 8.5, it follows that there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {SENT}}}(x)\) such that \({\scriptstyle \class {smallcaps}{\text {SENT}}}(\overline {n})\) is true (in \(\mathfrak {N}\)) iff \(n\) is the Gödel number of an \(\mathfrak {L}_A\)-sentence.

Similarly, if a theory \(T\) is axiomatized by a decidable set of axioms then there is a mechanical procedure for checking whether a given sequence of \(\mathfrak {L}_A\)-sentences is a deduction of a given target sentence from these axioms: we only need to check whether the last sentence in the sequence is the target sentence, and whether each sentence in the sequence is either an axiom of \(T\), an instance of the logical axioms A1–A7, or follows from previous sentences by MP or Gen. All these checks can be performed mechanically. Let \(\mathrm {Prf}_T\) be the relation that holds between numbers \(n\) and \(m\) iff \(n\) codes a deduction (informally, a “proof”) of the sentence coded by \(m\) from a set of axioms that generates \(T\). If \(T\) is computably axiomatizable, \(\mathrm {Prf}_T\) is computable. By Theorem 8.5, it is expressible in \(L_A\): there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) such that \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\overline {n},\overline {m})\) is true (in \(\mathfrak {N}\)) iff \(n\) codes a proof of the sentence coded by \(m\) from the axioms of \(T\).

For a final example, let’s look at a function on \(\mathfrak {L}_A\)-strings. Consider the concatenation function that takes two \(\mathfrak {L}_A\)-strings and returns the string consisting of the first followed by the second. This is clearly computable. So there is a recursive function \(*\) that maps the Gödel numbers of any two \(\mathfrak {L}_A\)-strings to the Gödel number of the concatenation of these strings. By Theorem 8.5, it follows that there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {CONCAT}}}(x,y,z)\) that defines \(*\) in \(L_A\), so that \({\scriptstyle \class {smallcaps}{\text {CONCAT}}}(\overline {n},\overline {m},\overline {k})\) is true (in \(\mathfrak {N}\)) iff \(k\) codes the concatenation of the strings coded by \(n\) and \(m\). (I’ll write this as \(k = n * m\), rather than \(k = *(n,m)\)).

In these examples, I’ve used the Church-Turing Thesis to argue that \(\mathrm {Sent}\), \(\mathrm {Prf}_T\) and \(*\) are computable in the technical sense, given that they are obviously computable in an informal sense. These appeals to the Church-Turing Thesis are avoidable. We could show directly that \(\mathrm {Sent}\), \(\mathrm {Prf}_T\) and \(*\) can be constructed from zero, successor, and projection by composition, primitive recursion, and regular minimization. In fact, we don’t need minimization: \(\mathrm {Sent}\), \(\mathrm {Prf}_T\) and \(*\) are primitive recursive. I won’t go through the details for each case. But let me illustrate what’s involved with the concatenation function \(*\) (which will play an important role in the next section).

Recall that \(*\) maps two Gödel numbers \(\gln {A}\) and \(\gln {B}\) to the Gödel number \(\gln {AB}\) of the concatenation of \(A\) and \(B\). If \(B\) is a single symbol, it is easy to define this operation arithmetically: \[ \gln {A} * \gln {s} = \gln {A} \cdot \mathrm {pri}(\mathrm {len}(\gln {A}))^{\gln {s}}, \] where \(\mathrm {pri}(i)\) is the \(i\)th prime number and \(\mathrm {len}(n)\) is the length of the string coded by \(n\). In Section 7.2, I showed that \(\mathrm {pri}\) and \(\mathrm {len}\) are primitive recursive. So the function \[ \mathrm {append}(x,y) = x \cdot \mathrm {pri}(\mathrm {len}(x))^{y} \] is also primitive recursive.

Next, we need the function \(\mathrm {entry}\) that takes two numbers \(n\) and \(i\) and returns the exponent of the \(i\)th prime in the prime factorization of \(n\). I showed in Section 7.2 that this function, too, is primitive recursive. Using \(\mathrm {append}\) and \(\mathrm {entry}\), we define (by primitive recursion) a function \(\mathrm {conc}\) that takes three numbers \(n\), \(m\), and \(i\) and returns the code of the string consisting of the string coded by \(n\) followed by the first \(i\) symbols of the string coded by \(m\): \begin {align*} \mathrm {conc}(x, y, 0) & = x \\[0.5em] \mathrm {conc}(x, y, s(i)) & = \mathrm {append}(\mathrm {conc}(x, y, i), \mathrm {entry}(y, s(i))). \end {align*}

From this, we can define \(x*y\) as \(\mathrm {conc}(x,y,\mathrm {len}(y))\).

9.3The First Incompleteness Theorem

I’ll now explain how Gödel managed to construct a sentence that is true iff it is unprovable. The construction is so perplexing that it may help to first give a version for English. I’ll show how to construct an English sentence that is true iff it is unprovable. (Let’s pretend we’ve specified what it means for an English sentence to be “provable”. You’ll see that nothing hangs on this.)

In English, we can use quote marks to denote expressions of English. For example,

‘is English’

is a noun that denotes an English predicate. We can combine nouns like this with predicates to form sentences:

(1)

‘is English’ is English.

(2)

‘is made of stone’ is made of stone.

(3)

‘is made of stone’ is English.

In (1) and (2), a predicate is applied to itself, using quote marks. Let’s call a sentence that results by applying a predicate to itself in this manner the diagonalization of that predicate. So (1) is the diagonalization of ‘is English’.

Now consider the predicate ‘has a diagonalization that is not provable’. If we diagonalize this predicate, we get

(4)

‘has a diagonalization that is not provable’ has a diagonalization that is not provable.

This is a sentence. What does it say? Well, it says that the predicate it quotes has an unprovable diagonalization. Every predicate has a unique diagonalization. So (4) says that the diagonalization of the quoted predicate (‘has a diagonalization that is not provable’) is not provable. But (4) is the diagonalization of that predicate. So (4) says of itself that it is not provable.

This trick obviously generalizes. We can replace ‘is not provable’ by any predicate \(A\). The argument shows that for any English predicate \(A\), there is a sentence \(G\) that says of itself that it is \(A\). To construct \(G\), we first construct another predicate \(F\): ‘has a diagonalization that is \(A\)’. \(G\) is then the diagonalization of \(F\). It is true iff it is \(A\).

We’ll now run this argument for \(\mathfrak {L}_A\). We use open formulas \(A(x)\) as predicates, and Gödel numerals \(\ulcorner A(x) \urcorner \) to refer to these predicates. For example, if \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\) expresses the property of coding a variable, then \({\scriptstyle \class {smallcaps}{\text {VAR}}}(\gn {{\scriptstyle \class {smallcaps}{\text {VAR}}}(x)})\) is a sentence saying (falsely) that the code of \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\) codes a variable – equivalently: that \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\) is a variable. We might call \({\scriptstyle \class {smallcaps}{\text {VAR}}}(\gn {{\scriptstyle \class {smallcaps}{\text {VAR}}}(x)})\) the diagonalization of \({\scriptstyle \class {smallcaps}{\text {VAR}}}(x)\). However, it proves convenient to use a slightly more roundabout definition.

For any \(\mathfrak {L}_A\)-formula \(A\), we define the diagonalization of \(A\) as the formula \[ \exists x(x\!=\ulcorner A \urcorner \land A). \]

If \(x\) is free in \(A\), which is the only case we care about, this is logically equivalent to \(A(\ulcorner A(x) \urcorner )\).

With this definition, constructing the diagonalization of a formula is a trivial mechanical task. Let \(\mathrm {diag}\) be the function that takes the Gödel number of a formula as input and returns the Gödel number of the formula’s diagonalization. This function is computable. In fact, it is primitive recursive, and easily expressible with the concatenation function \(*\): \[ \mathrm {diag}(y) = \gln {\exists x(x\!=\overline {y} \land } * y * \gln {)}. \]

By Theorem 8.5, all computable functions are expressible in \(\mathfrak {L}_A\). So there is a formula \({\scriptstyle \class {smallcaps}{\text {DIAG}}}(x,y)\) such that \({\scriptstyle \class {smallcaps}{\text {DIAG}}}(\overline {n},\overline {m})\) is true (in \(\mathfrak {N}\)) iff \(m\) codes the diagonalization of the formula coded by \(n\). We use this formula to construct, for any formula \(A(x)\) a sentence that “says of itself” that it has the property expressed by \(A(x)\).

Now we’re ready to prove the semantic version of Gödel’s First Incompleteness Theorem. Let \(T\) be some axiomatizable theory in \(\mathfrak {L}_A\), so that there is a decidable set of axioms \(\Gamma \) from which all and only the members of \(T\) can be deduced. I’ll say that a sentence is provable in \(T\) if it is deducible from some such set \(\Gamma \). As above, let \(\mathrm {Prf}_T\) be the relation that holds between numbers \(n\) and \(m\) iff \(n\) codes a deduction of the sentence coded by \(m\) from \(\Gamma \). As explained in the previous section, \(\mathrm {Prf}_T\) is computable; so there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) such that \(\mathfrak {N} \Vdash {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\overline {n},\overline {m})\) iff \(n\) codes a deduction from \(\Gamma \) of the sentence coded by \(m\). Let \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) abbreviate \(\exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(y,x)\). By construction, \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner )\) is true (in \(\mathfrak {N}\)) iff \(A\) is provable in \(T\). So \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner )\) is true iff \(A\) is unprovable in \(T\). By diagonalising \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\), we get a sentence \(G\) that is true (in \(\mathfrak {N}\)) iff it is unprovable (in \(T\)).

This is a beautiful argument, although the conclusion isn’t news to us: we’ve already derived it from the unsolvability of the Halting Problem in Section 5.5 (which, of course, wasn’t known when Gödel published his result).

As I mentioned in Section 9.1, Gödel also proved a syntactic version of the Incompleteness Theorem that doesn’t require the relevant theory to be sound (true in \(\mathfrak {N}\)), but merely imposes some syntactic conditions on it.

The idea is to run through the proof of Theorem 9.1 inside the theory \(T\). Instead of relying on the equivalence of \(G\) and \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner )\) in \(\mathfrak {N}\), we’ll use the fact that \(T\) can prove their equivalence: \(\vdash _T G \leftrightarrow \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner )\). This requires a different version of the Diagonal Lemma, turning on the representability of \(\mathrm {diag}\) in \(T\), rather than on its expressibility. Recall that a (one-place) function \(f\) is representable in a theory \(T\) iff there is a formula \(A(x,y)\) such that for all \(n\),

(i)

\(\vdash _T A(\overline {n},\overline {f(n)})\), and

(ii)

\(\vdash _T \forall y (A(\overline {n},y) \rightarrow y = \overline {f(n)})\).

Equivalently: \(\vdash _T \forall y (A(\overline {n},y) \leftrightarrow y = \overline {f(n)})\).

Now assume that \(T\) is an axiomatizable theory in which both \(\mathrm {diag}\) and \(\mathrm {Prf}_T\) are representable. As before, define \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) as \(\exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(y,x)\). The Syntactic Diagonal Lemma gives us a sentence \(G\) (called the Gödel sentence for \(T\)) such that \begin {equation} \tag {D} \vdash _T G \leftrightarrow \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner ). \end {equation} Let’s go through the reasoning in the proof of Theorem 9.1 to show that \(T\) can’t decide \(G\).

One of the two directions goes through smoothly: we can show that \(G\) isn’t provable in \(T\), unless \(T\) is inconsistent. For suppose \(T\) can prove \(G\). This means that there is a deduction of \(G\) from a suitable set of axioms for \(T\). Since \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) represents \(\mathrm {Prf}_T\) in \(T\), it follows that there is a number \(n\) (the code of the deduction) such that \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\overline {n},\ulcorner G \urcorner )\). Since \(T\) is closed under first-order consequence, it follows that \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner )\). By (D), we have \(\vdash _T \neg G\), So \(T\) proves both \(G\) and \(\neg G\).

The other direction is trickier. Suppose \(T\) can prove \(\neg G\). By (D), \(T\) can then prove \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner )\), which is short for \(\exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(y,\ulcorner G \urcorner )\). If \(T\) is consistent, there is no deduction of \(G\) from \(T\)’s axioms. So \(\mathrm {Prf}_T(n,\ulcorner G \urcorner )\) is false for every number \(n\). Since \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) represents \(\mathrm {Prf}_T\) in \(T\), it follows that \(\vdash _T \neg {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\overline {n},\ulcorner G \urcorner )\) for every number \(n\).

We now have the following situation: \(T\) proves \(\exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(y,\ulcorner G \urcorner )\), but also \(\neg {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\overline {n},\ulcorner G \urcorner )\) for every number \(n\). The theory says that there is a number of a certain kind, but also denies that any particular number 0,1,2,…is of that kind. This isn’t inconsistency, but it is almost as bad. Gödel called it “\(\omega \)-inconsistency”: a theory is \(\omega \)-inconsistent if there is a formula \(A(x)\) such that

(i)

\(\vdash _T \exists x \, A(x)\), but

(ii)

for every number \(n\), \(\vdash _T \neg A(\overline {n})\).

A theory is \(\omega \)-consistent if it is not \(\omega \)-inconsistent.

Clearly, no sound theory can be \(\omega \)-inconsistent. So \(\omega \)-consistency is another purely syntactic condition (besides consistency) that is entailed by soundness.

We’ve established the main result of Gödel’s 1931 paper:

I won’t go through the details of the proof again, as we’re going to prove a strictly stronger result in the next section, showing that mere consistency (as opposed to \(\omega \)-consistency) is enough. We will derive this from another important result, Tarski’s Theorem. But I want to mention that there is also a way to establish it directly, following Gödel’s line of reasoning. The trick, due to J. Barkley Rosser, is to make a slight change to the sentence \(G\). Instead of using a sentence that says of itself that it is unprovable, Rosser uses a sentence saying that for every proof of it, there is a shorter proof of its negation. More formally, Rosser’s version of the argument uses the diagonalization \(R\) of the following formula in place of \(G\): \[ \forall y({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(y,x) \,\to \, \exists z(z \!< \!y \,\land \, \forall v({\scriptstyle \class {smallcaps}{\text {CONCAT}}}(\ulcorner \neg \urcorner ,x,v) \to {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(z,v))). \] One can show that if \(\mathrm {Prf}_T\) and \(\mathrm {diag}\) are representable in \(T\), \(T\) is consistent, and \(T\) knows a few facts about arithmetic, then it can prove neither \(R\) nor \(\neg R\).

9.4Tarski’s Theorem

Recall that a formula \(A(x)\) represents a property \(P\) in a theory \(T\) iff for every \(\mathfrak {L}_A\)-sentence \(B\),

(i)

if \(P(B)\), then \(\vdash _T A(\ulcorner B \urcorner )\), and

(ii)

if \(\neg P(B)\), then \(\vdash _T \neg A(\ulcorner B \urcorner )\).

In exercise 9.9, you showed that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) does not represent provability in PA. Officially, PA is just the set of all sentences that are provable in PA. You therefore showed that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) does not represent membership in PA.

This result can be strengthened. The following theorem, due to Alfred Tarski (1933), shows that no \(\mathfrak {L}_A\)-formula represents membership in PA. Indeed, no formula represents membership in any consistent theory in which \(\mathrm {diag}\) is representable.

Note that Tarski’s Theorem isn’t restricted to axiomatizable theories. It even holds for \(\mathrm {Th}(\mathfrak {N})\). Since representability in \(\mathrm {Th}(\mathfrak {N})\) implies expressibility in \(\mathfrak {L}_A\), it follows that no \(\mathfrak {L}_A\)-formula expresses membership in \(\mathrm {Th}(\mathfrak {N})\):

Tarski’s Theorem shows that while \(\mathfrak {L}_A\) can formalize its own syntax (we can express \(\mathfrak {L}_A\)-properties like being a variable or being a sentence), it can’t express the most basic concept of its own semantics. This isn’t just true for \(\mathfrak {L}_A\). Loosely speaking, no sufficiently powerful language that can express its own syntax can express its own semantics.

We can bring this out a little more clearly by considering the concept of a truth predicate. As Tarski pointed out, the central feature of the predicate ‘is true’ in English is that when it is applied to a sentence, the result is equivalent to that sentence:

(1)

‘Snow is white’ is true iff snow is white.

(2)

‘2+2=4’ is true iff 2+2=4.

Sentences like (1) and (2) are called Tarski biconditionals. A theory that can reason about truth should be able to prove all Tarski biconditionals for its language. Thus a formula \(W(x)\) is called a truth predicate for a theory \(T\) iff \(\vdash _T W(\ulcorner A \urcorner ) \leftrightarrow A\) for every sentence \(A\) in \(T\)’s language. An argument similar to the one used in Theorem 9.3 shows that no sufficiently powerful theory can have a truth predicate, unless it is inconsistent. This result is also called “Tarski’s Theorem”.

While Gödel’s sentence \(G\) says of itself that it is unprovable, the sentence \(L\) that figures in this proof says of itself that it is not true. It is a formal analogue of the Liar sentence ‘This sentence is false’. The existence of such a sentence leads to paradox: if \(L\) is true then \(L\) is false, and if \(L\) is false then \(L\) is true. Theorem 9.5 concludes that \(L\) can’t exist. By the Diagonal Lemma, it would exist if there were a truth predicate for \(T\). So there can be no truth predicate for \(T\). By contrast, it is not an option to deny the existence of \(G\). By the Diagonal Lemma, \(G\) can be constructed from \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\). The existence of \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) is guaranteed by the fact that (for suitable choices of \(T\)) \(\mathrm {Prf}_T\) is computable.

We’ll now use Tarski’s Theorem to derive both the undecidability of first-order logic and strengthened versions of Gödel’s First Incompleteness Theorem. Both derivations are easy, and follow a similar pattern.

Let \(\hat {Q}\) be the conjunction of the seven axioms of Q. If there were an algorithm to decide whether a first-order sentence is valid, we could use it to decide whether a sentence \(A\) is in Q, by checking whether \(\hat {Q} \to A\) is valid. So membership in Q would be computable, and hence representable in Q. This contradicts Tarski’s Theorem. So there can be no algorithm to decide whether a first-order sentence is valid.

As for Gödel’s Theorem, let \(T\) be a consistent, axiomatizable extension of Q. If \(T\) were complete, we could decide whether a sentence \(A\) is in \(T\) by simultaneously searching for a proof of \(A\) and a proof of \(\neg A\): one or the other must exist. So membership in \(T\) would be computable, and hence representable in \(T\). This contradicts Tarski’s Theorem. So every consistent and axiomatizable extension of Q is incomplete.

To fill in some more details, I’ll begin with a small lemma.

Church’s Theorem shows that Hilbert’s Entscheidungsproblem has no solution: there is no mechanical procedure that decides whether an arbitrary first-order sentence is valid.

Turning to the syntactic Incompleteness Theorem, I’ll first give a more rigorous proof of Proposition 5.5, according to which every axiomatizable and complete first-order theory is decidable. I couldn’t give a rigorous proof in Chapter 5 because we didn’t yet have a rigorous concept of computability. The following proof shows that if a theory is axiomatizable and complete, then membership in the theory is recursive.

Since all computable functions are representable in every extension of Q (Theorem 8.3), Theorem 9.7 implies that every consistent, axiomatizable extension of Q is incomplete. We can prove an even stronger result by strengthening Lemma 9.3.

9.5The arithmetical hierarchy

Let’s take stock. Since all computable functions are representable in PA, Gödel’s Theorem shows that PA is incomplete (unless it is inconsistent). The incompleteness can’t be fixed by simply adding more axioms: as long as the resulting theory is consistent and axiomatizable, it will remain incomplete.

The result carries over to more powerful theories like ZFC, in virtue of the fact that PA is interpretable in these theories (see Section 4.3). More generally, Gödel’s Theorem applies whenever a theory’s language is rich enough to express central aspects of its own syntax. This isn’t always the case. For example, consider a fragment of \(\mathfrak {L}_A\) whose only non-logical symbols are \(0\), \(s\), and \(+\), without \(\times \). In the previous chapter, we needed multiplication to express the recursive functions and relations. Without multiplication, \(\mathrm {Prf}_T\) and \(*\) are no longer expressible. As a consequence, the Incompleteness Theorems don’t apply. Indeed, if you restrict the axioms of PA to this weaker language, and remove the two axioms for multiplication, you get a complete theory. (This theory is called Presburger Arithmetic.)

Return to PA. We know that there are (infinitely many) true sentences that PA can’t prove. But what do they look like? This is important to assess the practical significance of Gödel’s result. If PA can’t prove 2+2=4, that’s a serious problem. If the only arithmetical truths that PA can’t prove take a trillion years to state, incompleteness may be harmless in practice.

Gödel’s original proof (unlike the proof via Tarski’s Theorem) gives us an example of an unprovable sentence: the “Gödel sentence” \(G\). As I’ll explain below, this sentence states (in a very roundabout way) that a certain complicated equation between polynomials has no solution in the natural numbers. If it weren’t for Gödel’s Theorem, no one would ever have considered this equation. Until the 1960s, the only sentences known to be unprovable in PA were of this kind. Since then, more natural examples have been found. The simplest is probably Goodstein’s Theorem. (See Section 7.3.) Goodstein’s Theorem states an interesting fact about the natural numbers, but its proof involves transfinite ordinals: it is provable in ZFC, but not in PA. For ZFC itself, we already know of a “natural” statement that it can’t decide: the Continuum Hypothesis. There are many other examples.

To get a sense of which \(\mathfrak {L}_A\)-sentences are provable and which might be unprovable in PA, it is useful to classify the \(\mathfrak {L}_A\)-sentences by their construction from atomic formulas. Since the only predicate letter in \(\mathfrak {L}_A\) is the identity predicate ‘=’, all atomic formulas of \(\mathfrak {L}_A\) are identity statements: they have the form \(t_1 = t_2\). From these, complex formulas are constructed using truth-functional connectives and quantifiers. We’ll divide them into stages.

At the first stage, we have all identity statements \(t_1 = t_2\), all inequalities of the form \(t_1 < t_2\), and all formulas that can be constructed from these by truth-functional connectives and bounded quantification, where a bounded quantification of a formula \(A\) is a formula of the form \(\forall x(x < t \;\to \; A)\) or \(\exists x(x < t \;\land \; A)\), with \(x\) not occurring in \(t\). (Officially, of course, \(t_1 < t_2\) is short for \(\exists z(t_1 + s(z) = t_2)\).) The formulas in this class are called \(\Delta _{0}\)-formulas. Intuitively, a \(\Delta _{0}\)-formula is any \(\mathfrak {L}_A\)-formula that doesn’t involve unbounded quantification.

At the next stage, we consider all sentences that can be formed from \(\Delta _{0}\)-formulas by prefixing unbounded universal quantifiers or unbounded existential quantifiers. A \(\Delta _{0}\)-formula with a string of universal quantifiers in front is called a \(\Pi _{1}\)-formula; a \(\Delta _{0}\)-formula with a string of existential quantifiers in front is called a \(\Sigma _{1}\)-formula. For example, \(\forall x \forall y (x + y = y + x)\) is a \(\Pi _{1}\)-formula, while \(\exists x \exists y (x + y = y + x)\) is a \(\Sigma _{1}\)-formula.

Prefixing universal quantifiers to a \(\Sigma _{1}\)-formula yields a \(\Pi _{2}\)-formula; prefixing existential quantifiers to a \(\Pi _{1}\)-formula yields a \(\Sigma _{2}\)-formula. Thus \(\forall x \exists y (x + y = y + x)\) is \(\Pi _{2}\), and \(\exists x \forall y (x + y = y + x)\) is \(\Sigma _{2}\). And so on.

This somewhat complicated classification is motivated by the computational properties of the relations expressed by the relevant formulas. The relations expressed by \(\Delta _{0}\)-formulas are all primitive recursive. Since \(\Delta _{0}\)-formulas don’t involve unbounded quantification, one can check whether they hold of some numbers by simple checks, without unbounded loops. By contrast, to check whether a \(\Sigma _{1}\)-formula \(\exists x \, A(x)\) holds of some number, one may need to search through all numbers until one finds a witness for \(A(x)\). Many \(\Sigma _{1}\)-formulas therefore express relations that are not primitive recursive. Some of them are merely recursive. In fact, every recursive (=computable) relation is expressible by a \(\Sigma _{1}\)-formula. But not every relation expressed by a \(\Sigma _{1}\)-formula is computable. Some are just computably enumerable. Recall from Section 5.4 that a relation \(R\) on \(\mathbb {N}\) is computably enumerable iff there is a computable relation \(S\) such that \(R(x_1,\ldots ,x_n)\) holds iff \(\exists y \, S(x_1,\ldots ,x_n,y)\).

We can use Theorem 9.9 to get an idea of what the unprovable Gödel sentence \(G\) for PA might look like. Recall that \(G\) is equivalent in PA to \(\neg \mathrm {Prov}_{\mathrm {PA}}(\ulcorner G \urcorner )\). Since \(\mathrm {Prov}_{\mathrm {PA}}\) is defined by existential quantification from the computable relation \(\mathrm {Prf}_{\mathrm {PA}}\), it is computably enumerable. By Theorem 9.9, it is expressible by a \(\Sigma _{1}\)-formula. So the Gödel sentence \(G\) is equivalent in PA to the negation of a \(\Sigma _{1}\)-sentence. This makes it equivalent to a \(\Pi _{1}\)-sentence. Gödel’s result therefore shows that there are undecidable \(\Pi _{1}\)-sentences.

Theorem 9.9 can be strengthened:

Since every \(\mathfrak {L}_A\)-term expresses a polynomial, the MRDP Theorem shows that every computably enumerable relation is expressed by a formula stating that a certain equation between polynomials has a solution in the natural numbers. That’s why I said that the Gödel sentence is equivalent to the statement that some equation between polynomials has no solution in the natural numbers. The proof of the MRDP theorem is too difficult to be even sketched here.

Let’s return once more to Tarski and Gödel. By Theorem 9.4, arithmetical truth is not expressible in \(\mathfrak {L}_A\). With our new understanding of the arithmetical hierarchy, we can now strengthen the semantic Incompleteness Theorem. As stated in Theorem 9.1, the semantic Theorem says that every sound and axiomatizable \(\mathfrak {L}_A\)-theory is incomplete. It is easy to see that a theory is axiomatizable iff the set of Gödel numbers of its members is computably enumerable. Theorem 9.1 therefore applies to all theories whose members are expressed by a \(\Sigma _{1}\)-formula. We can extend the result to non-axiomatizable theories that are only expressible by \(\Pi _{2}\)-formulas or \(\Sigma _{12}\)-formulas.

Let’s say that a theory \(T\) is expressible in \(\mathfrak {L}_A\) if there is an \(\mathfrak {L}_A\)-formula \(W(x)\) such that for all sentences \(B\), \(\mathfrak {N} \Vdash W(\ulcorner B \urcorner )\) iff \(B \in T\).