10The Unprovability of Consistency

Gödel’s Second Incompleteness Theorem states that no sufficiently strong mathematical theory can prove its own consistency. In this chapter, we explore how this can be shown and what it implies for the foundations of mathematics and beyond.

10.1The Second Incompleteness Theorem

Let’s review some background. As in the previous chapter, we’re going to focus on axiomatizable theories in the language of arithmetic \(\mathfrak {L}_A\). A theory is simply a set of sentences that is closed under logical consequence. An axiomatizable theory is one for which there is a decidable set of axioms from which all and only the members of the theory are deducible.

By coding \(\mathfrak {L}_A\)-strings as numbers, we can use the language of arithmetic to reason about its own syntax. We use ‘\(\gln {A}\)’ to denote the code (“Gödel number”) of an \(\mathfrak {L}_A\)-string \(A\), and ‘\(\ulcorner A \urcorner \)’ to denote the \(\mathfrak {L}_A\)-numeral for \(\gln {A}\), relative to some fixed coding scheme. (The details of the scheme don’t matter, as long as it is effective.)

Given an axiomatizable theory \(T\), 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 some decidable set of axioms for \(T\). This relation is computable. In Chapter 8 we proved that all computable functions and relations are representable in any moderately strong theory of arithmetic – in particular, in any extension of Q. That is, if \(T\) is at least as strong as Q then there is an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) such that

(i)

if \(\mathrm {Prf}_T(n,m)\) holds, then \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\ulcorner n \urcorner ,\ulcorner m \urcorner )\);

(ii)

if \(\mathrm {Prf}_T(n,m)\) doesn’t hold, then \(\vdash _T \neg {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\ulcorner n \urcorner ,\ulcorner m \urcorner )\).

If \(T\) is sound, the formula \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\) also expresses \(\mathrm {Prf}_T\) in \(\mathfrak {L}_A\), so that \begin {equation*} \mathfrak {N} \Vdash {\scriptstyle \class {smallcaps}{\text {PRF}}}_T(\ulcorner n \urcorner ,\ulcorner m \urcorner ) \text { iff } \mathrm {Prf}_T(n,m). \end {equation*}

From \({\scriptstyle \class {smallcaps}{\text {PRF}}}_T(x,y)\), we can define another formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) as \(\exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_{T}(y,x)\). Informally, \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) says that the sentence with Gödel number \(x\) is provable in \(T\).

Now remember that a theory \(T\) is consistent if it doesn’t prove a contradiction. This can be spelled out in multiple ways:

(1)

There is no sentence \(A\) such that \(\vdash _T A\) and \(\vdash _T \neg A\);

(2)

\(\not \vdash _T \bot \);

(3)

There is some sentence \(A\) such that \(\not \vdash _T A\).

In classical logic, all three conditions are equivalent. Let’s focus on (2), since it is the shortest. If we have an \(\mathfrak {L}_A\)-formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) that expresses provability in \(T\), we can find another \(\mathfrak {L}_A\) formula that expresses the consistency of \(T\): \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \bot \urcorner )\).

(Officially, ‘\(\bot \)’ is not part of \(\mathfrak {L}_A\): in Chapter 1, I suggested that it abbreviates ‘\(\neg (p \to p)\)’, but we also don’t have sentence letters in \(\mathfrak {L}_A\). Let’s say that \(\bot \) is the sentence ‘\(\neg (0\!=\!0)\)’. Since \(0\!=\!0\) is provable in first-order logic, \(\bot \) is refutable in first-order logic, which is all that matters.)

Now let \(T\) be some axiomatizable extension of Q. Since the consistency of \(T\) can be expressed in \(T\)’s language, we might wonder whether \(T\) can prove it: can an arithmetical theory prove its own consistency? At the end of the 1931 paper in which he proved the First Incompleteness Theorem, Gödel gave an answer: he claimed that no sufficiently strong, axiomatizable, and consistent theory can prove its own consistency. This is Gödel’s Second Incompleteness Theorem.

Gödel also outlined a proof of this claim. It goes as follows.

Remember that in his proof of the First Incompleteness Theorem, Gödel used the (Syntactic) Diagonal Lemma to construct a “Gödel sentence” \(G\) such that \begin {equation} \tag {1} \vdash _{T} G \leftrightarrow \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner G \urcorner ). \end {equation} He then showed that if \(T\) is consistent then \(T\) can’t prove \(G\). He also showed that if \(T\) is \(\omega \)-consistent then it can’t prove \(\neg G\). But let’s focus on the first result. Its proof required no advanced mathematics. (No transfinite ordinals or the Axiom of Choice or anything like that.) It can be carried out in any moderately strong theory that can reason about recursivity, representability, and the syntax of \(T\). Suppose it can be carried out in \(T\) itself. Then the following sentence is provable in \(T\): \begin {equation} \tag {2} \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner ) \to \neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner G \urcorner ). \end {equation} This says in \(\mathfrak {L}_A\) that if \(T\) is consistent then \(T\) can’t prove \(G\).

Now suppose that \(T\) can prove its own consistency: it can prove \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner )\). By Modus Ponens and (2), \(T\) can infer \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner G \urcorner )\). By (1), it can then infer \(G\). But we’ve assumed that \(T\) is an axiomatizable extension of Q. And we know from Gödel’s First Incompleteness Theorem that no axiomatizable and consistent extension of Q can prove \(G\). So \(T\) must be inconsistent.

In sum, if \(T\) is a consistent and axiomatizable extension of Q, and (2) is provable in \(T\), then \(T\) can’t prove its own consistency.

It turns out that (2) isn’t provable in Q. But it is provable in the standard axiomatization of arithmetic, Peano Arithmetic (PA). The Second Incompleteness Theorem therefore implies that PA can’t prove its own consistency (assuming it is consistent).

Before we investigate why (2) is provable in PA, let’s think about the significance of the result. Why should we care whether PA can prove its own consistency?

Note that any inconsistent theory can trivially prove its own consistency (as long as this is expressible in its language): an inconsistent theory can prove everything. Even if a consistent theory could prove its own consistency, this would therefore provide no reason to think that the theory really is consistent.

The significance of the Second Incompleteness Theorem comes from what it implies about the powers of theories to prove the consistency of other theories. Take a theory like ZFC in which most of mathematics can be formalized. Hilbert had hoped that one could prove the consistency of such theories in a much weaker, “finitary” theory that studies deductions as finite syntactic objects. Gödel’s Second Incompleteness Theorem implies that this can’t be done. ZFC is certainly strong enough to prove (2). By Gödel’s Theorem, it follows that ZFC can’t prove its own consistency. But then no weaker theory can prove the consistency of ZFC either: if something isn’t even provable in ZFC, it can’t be provable in, say, PA or Q – for anything that’s provable in PA or Q is also provable (under a suitable translation, see Section 4.3) in ZFC.

To complete the proof of the Second Incompleteness Theorem, we’d need to show that sufficiently powerful theories like PA prove (2). Fortunately, this doesn’t require formalizing the entire proof of the First Incompleteness Theorem. It is enough to show that the formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(x)\) satisfies some basic conditions. These conditions are known as the Hilbert-Bernays-Löb provability conditions, because they were first formulated explicitly in a 1939 textbook by Hilbert and Bernays and later streamlined by Martin Löb. They are as follows.

We’ll see below how (2) can be derived from P1–P3. First, let’s examine what it takes to show that, say, \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) satisfies the three conditions.

P1 is easy. Assume that \(A\) is provable in PA. Then there is number \(n\) that codes a deduction of \(A\) from the axioms of PA. Since \({\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(x,y)\) represents \(\mathrm {Prf}_{\mathrm {PA}}\) in PA, we have \(\vdash _{\mathrm {PA}} {\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(\overline {n},\ulcorner A \urcorner )\). So we also have \(\vdash _{\mathrm {PA}} \exists y \, {\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(y, \ulcorner A \urcorner )\) and therefore \(\vdash _{\mathrm {PA}} {\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(\ulcorner A \urcorner )\). So \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) satisfies P1.

The argument for P2 isn’t much harder. Suppose we have a proof of \(A \to B\) and a proof of \(A\). From these, we can construct a proof of \(B\) by concatenating the two proofs and adding \(B\) as a final line (applying Modus Ponens). All this can be formalized in PA, showing that if there are numbers \(m\) and \(n\) that code proofs of \(A\) and \(A \to B\), then there is a number \(k\) that codes a proof of \(B\). Which is what P2 says.

The argument for P3 is more involved. It essentially requires formalizing within PA the proof that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}\) satisfies P1. This takes about a dozen pages of tedious tinkering. I’ll spare us the details. (You can find them, for example, in George Boolos, The Logic of Provability, 1993, ch. 2.) Let’s just accept that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {PA}}(x)\) satisfies P1–P3.

We can now finish the proof of the Second Incompleteness Theorem, by deriving (2) from P1–P3. To remove clutter, I’ll abbreviate \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner A \urcorner )\) as \(\Box A\). This is a little misleading because it suggests that the sentence \(A\) occurs in \(\Box A\), while in fact only its Gödel numeral does. But it will make the proof more readable.

With this convention, P1–P3 can be written as follows:

Why is this an incompleteness theorem? Because it shows that a certain sentence, \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner )\), is unprovable in any sufficiently strong and consistent theory \(T\), even though it is true.

In a way, this form of incompleteness is more striking than the one established by Gödel’s First Theorem. Here is how Gödel put it in a 1951 lecture:

[The second theorem] makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct, and moreover I believe that they contain all of mathematics. If someone makes such a statement he contradicts himself. For if he perceives the axioms under consideration to be correct, he also perceives (with the same certainty) that they are consistent. Hence he has a mathematical insight not derivable from his axioms.

Take the standard axiomatization of set theory, ZFC. Suppose we “perceive” that ZFC is sound, and therefore consistent. If this “perception” is correct, it goes beyond what ZFC can prove, although the consistency part can be expressed in the language of ZFC: we perceive the truth of \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {ZFC}}(\ulcorner \bot \urcorner )\). We might propose a strengthened version of ZFC, with \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {ZFC}}(\ulcorner \bot \urcorner )\) as a new axiom. Call this theory ZFC\(^+\). The Second Incompleteness Theorem still applies: ZFC\(^+\) can’t prove its own consistency (if it is consistent). But if ZFC is sound, then so is ZFC\(^+\). Our “perception” of the soundness of ZFC therefore allows us to strengthen ZFC\(^+\) by adding another consistency statement, \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_{\mathrm {ZFC}^+}(\ulcorner \bot \urcorner )\). Call this theory ZFC\(^{++}\). The Second Incompleteness Theorem still applies …. In this way, our perception of the soundness of ZFC allows us to construct an infinite sequence of ever stronger theories, each of which must be sound. We might even propose a theory ZFC\(^{\omega }\) that combines all these theories: the union of ZFC, ZFC\(^+\), ZFC\(^{++}\), etc. This theory is still axiomatizable, so the Second Incompleteness Theorem still applies: it can’t prove its own consistency (if it is consistent). So we can keep adding consistency statements, creating ZFC\(^{\omega +1}\), ZFC\(^{\omega +2}\), …, ZFC\(^{\omega +\omega }\), and so on, up through the ordinals until we reach a point (the “Church-Kleene ordinal” \(\omega _1^{\mathrm {CK}}\)) where the union of the previous theories can no longer be captured in the language of ZFC.

10.2Löb’s Theorem

For a suitable theory \(T\), the Diagonal Lemma allows us to construct a Gödel sentence \(G\) that says of itself that it is unprovable in \(T\). We can also construct a sentence \(H\) that says of itself that it is provable. More formally, if we apply the (Syntactic) Diagonal Lemma to the formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\), we get a sentence \(H\) such that \begin {equation} \tag {D} \vdash _T H \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner H \urcorner ). \end {equation} \(H\) is called the Henkin sentence for \(T\). It’s easy to show that no consistent theory can prove its Gödel sentence. For the Henkin sentence, the situation is less clear. Is \(H\) provable in \(T\)? This question was raised by Leon Henkin in 1952, and answered by Martin Löb in 1955. Löb showed that if \(T\) is consistent, axiomatizable, and sufficiently strong, and it proves \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner ) \to A\) for some sentence \(A\), then it also proves that sentence \(A\). This is known as Löb’s Theorem. Since (D) gives us \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner H \urcorner ) \to H\), the Theorem entails \(\vdash _T H\). The Henkin sentence \(H\) is indeed provable in \(T\).

The proof of Löb’s Theorem resembles the following proof that Santa Claus exists.

Let \(S\) be the sentence ‘if \(S\) is true then Santa Claus exists’. This being a conditional, we can try to prove it by deriving the consequent from the antecedent. So assume the antecedent: \(S\) is true. So if \(S\) is true then Santa Claus exists (for this is what \(S\) says). Still assuming that \(S\) is true, we can infer (by Modus Ponens) that Santa Claus exists. Now we have derived the consequent of \(S\) from its antecedent. So we’ve proved \(S\): we’ve proved that if \(S\) is true then Santa Claus exists. And since we’ve proved \(S\), we can infer by Modus Ponens that Santa Claus exists.

This line of reasoning is known as Curry’s Paradox. It clearly works for any consequent \(A\) in place of ‘Santa Claus exists’. In the following proof of Löb’s Theorem, we replace ‘is true’ (which is not expressible in \(\mathfrak {L}_A\)) by ‘is provable’. The assumption \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner ) \to A\) of Löb’s Theorem gives us one direction of the Tarski biconditional for \(A\). In the presence of P1–P3, that’s enough to run a Curry-style argument and show that \(\vdash _T A\).

In line 1 of this proof, the Diagonal Lemma is used to construct the sentence \(S\) that “says that” (is provably equivalent to) ‘if \(S\) is provable then \(A\)’. As in Curry’s Paradox, \(T\) can derive that if \(S\) is provable then \(A\) (line 9). From this, \(T\) infers that \(S\) is true (line 10), and thereby that \(S\) provable (line 11), from which it infers \(A\) by Modus Ponens (line 12).

From Löb’s Theorem, it is a short step to the Second Incompleteness Theorem. Assume \(T\) can prove \(\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner )\). By propositional logic, this entails \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner ) \to \bot \). By Löb’s Theorem, it follows that \(T\) can prove \(\bot \). So if \(T\) can prove its own consistency, then \(T\) is inconsistent.

Löb’s Theorem also entails a version of Tarski’s Theorem on the undefinability of truth. Recall that a predicate \(W(x)\) is a truth predicate for a theory \(T\) if \(T\) can prove all the Tarski biconditionals \[ W(\ulcorner A \urcorner ) \leftrightarrow A. \] Suppose that \(W(x)\) is a truth predicate for \(T\). Then \(W(x)\) is also a provability predicate for \(T\). Assume that \(T\) is an axiomatizable theory in which \(\mathrm {diag}\) is representable. Since \(\vdash _T W(\ulcorner A \urcorner ) \to A\) for all \(A\), it follows by Löb’s Theorem that \(\vdash _T A\) for all \(A\). So \(T\) is inconsistent.

Löb’s Theorem highlights the difference between the formal concept of provability and the concept of truth. One might have expected that a sufficiently powerful theory would “know that” whatever it can prove is the case. That is, one might have expected that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T\) should satisfy the Reflection principle from exercise 10.4:

(A truth predicate would satisfy both Ref and its converse.) Löb’s Theorem shows that if \(T\) is sufficiently strong and consistent then \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T\) satisfies only those instances of Ref for which \(A\) is already provable in \(T\), in which case \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner ) \to A\) follows by propositional logic.

10.3The logic of provability

If you are familiar with modal logic, the provability conditions P1–P3 will look familiar, especially when written with the box operator \(\Box \). If you aren’t familiar with modal logic, let me introduce some background.

The language \(\mathfrak {L}_M\) of propositional modal logic is obtained from the language \(\mathfrak {L}_0\) of propositional logic by adding the unary sentence operator ‘\(\Box \)’: whenever \(A\) is an \(\mathfrak {L}_M\)-sentence, then so is \(\Box A\). The intended meaning of the box varies from application to application; often it is used to express some kind of necessity.

Hilbert-style proof systems for propositional modal logic extend the propositional calculus by axioms and inference rules that govern the behaviour of the box. A well-known proof system adds one axiom schema and one rule of inference:

This system is known as K. (So ‘K’ names both a proof system and an axiom schema. The letter stands for Saul Kripke.) Stronger systems can be obtained by adding further axioms. For example, the system K4 adds an axiom schema known (for obscure historical reasons) as ‘4’; the system S4 adds both 4 and Ref (more commonly known as ‘T’):

Any system that can be obtained by adding axiom schemas to K is called a normal modal logic.

Above I used the box notation to simplify sentences of \(\mathfrak {L}_A\). Sentences in the box notation look just like sentences of \(\mathfrak {L}_M\). To make this more explicit, let \(t\) be a function that maps each sentence letter \(p\) of \(\mathfrak {L}_M\) to an \(\mathfrak {L}_A\)-sentence \(t(p)\). We can extend any such \(t\) to a mapping from \(\mathfrak {L}_M\)-sentences to \(\mathfrak {L}_A\)-formulas, as follows: \begin {align*} \transt {p} &= t(p) \\[0.5em] \transt {\neg A} & = \neg \transt {A} \\[0.5em] \transt {A \to B} & = \transt {A} \to \transt {B} \\[0.5em] \transt {\Box A} & = {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \transt {A} \urcorner ) \end {align*}

Here I use ‘\(\transt {A}\)’ to denote the output of the mapping for input \(A\). For example, assume that \(t(p)\) is ‘\(0\!=\!0\)’. Then \(\transt {p}\) is ‘\(0\!=\!0\)’, \(\transt {\neg p}\) is ‘\(\neg (0\!=\!0)\)’, and \(\transt {\Box p}\) is ‘\({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner 0\!=\!0 \urcorner )\)’.

Now assume that \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) satisfies P1–P3. In “box notation”, P1, P2, and P3 are Nec, K, and 4, respectively. We might therefore expect that whenever an \(\mathfrak {L}_M\)-sentence \(A\) is provable in the modal system K4, then \(\transt {A}\) is provable in \(T\). We’ll confirm this below.

The full modal logic of provability isn’t K4, however. It has another axiom schema, known as GL (for Gödel and Löb):

The system of modal logic obtained by adding GL to K4 is also called GL. (It turns out that the 4 schema is redundant: it can be derived from GL.)

GL is the modal translation of a formalized version of Löb’s Theorem. Löb’s Theorem states that

If \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner ) \to A\) then \(\vdash _T A\).

The formalized version of Löb’s Theorem lifts this into \(T\):

\(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\gn {{\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner ) \to A}) \to {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner A \urcorner )\).

It is easily derivable from Löb’s Theorem itself:

The following theorem confirms that if \({\scriptstyle \class {smallcaps}{\text {PROV}}}_T(x)\) satisfies P1–P3, and an \(\mathfrak {L}_M\)-sentence \(A\) is provable in the modal logic GL, then \(\transt {A}\) is provable in \(T\).

The converse of Theorem 10.3 also holds: whenever \(\vdash _{T} \transt {A}\), then \(\vdash _{\mathrm {GL}} A\). This arithmetical completeness theorem was proved by Robert Solovay in 1976. The proof is too hard to get into here.

Theorem 10.3 shows that we can use propositional modal logic to establish results about provability in theories like PA. Solovay’s theorem shows that all general facts about provability in such theories can be established in this way.

For a simple illustration of how this works, here is a GL-proof of a formalized version of the Second Incompleteness Theorem, showing that if \(T\) meets the conditions for the Theorem, then \(T\) can prove that if it can prove its own consistency, then it is inconsistent. \begin {flalign*} \quad 1.\quad & \vdash _{GL} \neg \Box \bot \to (\Box \bot \to \bot ) && \text {(propositional logic)}& \\[0.5em] \quad 2.\quad & \vdash _{GL} \Box (\neg \Box \bot \to (\Box \bot \to \bot )) && \text {(from 1 by Nec)}& \\[0.5em] \quad 3. \quad & \vdash _{GL} \Box \neg \Box \bot \to \Box (\Box \bot \to \bot ) && \text {(from 2 by K)}& \\[0.5em] \quad 4.\quad & \vdash _{GL} \Box (\Box \bot \to \bot ) \to \Box \bot && \text {(GL)}& \\[0.5em] \quad 5.\quad & \vdash _{GL} \Box \neg \Box \bot \to \Box \bot && \text {(from 3 and 4)}& \end {flalign*}

By Theorem 10.3, it follows that \(\vdash _T {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\gn {\neg {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner )}) \to {\scriptstyle \class {smallcaps}{\text {PROV}}}_T(\ulcorner \bot \urcorner )\).

For another illustration, one can show that (for any sentence \(A\)) \begin {equation*} \vdash _{GL} \Box (A \leftrightarrow \Box \neg A) \to \Box (A \leftrightarrow \Box \bot ). \end {equation*} Among other things, this tells us what theories like PA will make of a sentence \(N\) that “says of itself” that its negation is provable. We get such a sentence by applying the Diagonal Lemma to the formula \({\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \neg \urcorner * x)\): \begin {equation*} \vdash _{T} N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \neg N \urcorner ). \end {equation*} By P1, this entails \[ \vdash _{T} {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\gn {N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \neg N \urcorner )}). \] The above result from GL gives us \[ \vdash _{T} {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\gn {N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \neg N \urcorner )}) \to {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\gn {N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \bot \urcorner )}). \] So by Modus Ponens, \[ \vdash _{T} {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\gn {N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \bot \urcorner )}). \] If \(T\) is sound, this entails \[ \vdash _{T} N \leftrightarrow {\scriptstyle \class {smallcaps}{\text {PROV}}}_{T}(\ulcorner \bot \urcorner ). \] So the sentence \(N\) that says that its negation is provable in PA is equivalent in PA to the statement that PA is inconsistent. Since PA can neither prove nor disprove its own consistency (assuming it is consistent), it can neither prove nor disprove \(N\).

10.4Chaitin’s Incompleteness Theorem

In 1974, Gregory Chaitin proved a version of the First Incompleteness Theorem that connects it to issues of computability. We’ll see that it also opens a new route to the Second Incompleteness Theorem.

Recall that a Turing machine takes as input a pattern of strokes and blanks on its tape. Its output, if it halts, is also a pattern of strokes and blanks. If we ignore the blank cells to the left of the first stroke and to the right of the last stroke, all these patterns are finite. Every finite pattern can be produced by a Turing machine. In fact, for every finite pattern of strokes and blanks, there are infinitely many Turing machines that produce it. We might be interested in the most efficient way to generate a given pattern: what is the shortest Turing machine program that produces it (starting on blank tape)?

The program of a Turing machine is a string that lists all its instructions – all quintuples like \(\langle q_0, B, 1, R, q_1 \rangle \) that specify what machine does if it scans a certain symbol in a certain state. We’ve seen in Section 6.3 that these instructions can themselves be coded as patterns of strokes and blanks and fed to a universal Turing machine, which will execute the program.

Let’s define the complexity of a pattern as the length of the shortest program that produces it. (This is somewhat imprecise, but the imprecision will do us no harm. The more precise concept is called Kolmogorov complexity.)

Some patterns can be produced by very short programs, others require very long programs. As a rule, short and regular patterns can be produced by short programs, while long and disorderly patterns tend to require long programs: they have high complexity.

It’s easy to see that there is no limit to how complex a pattern can be. For any number \(n\), only finitely many patterns can be produced by programs of length up to \(n\); all other patterns require longer programs: they have greater complexity.

You’d think that for any number \(n\), we can easily find examples of patterns whose complexity is demonstrably greater than \(n\). Chaitin’s Incompleteness Theorem shows that this is not so. In essence, it says that for any axiomatized and consistent theory that knows some basic facts about Turing machines, there is a particular number \(L\) such that the theory can’t prove of any pattern that its complexity is greater than \(L\).

To state this more precisely, consider the relation \(H\) that holds between a Turing machine program \(M\), a pattern of strokes and blanks \(S\), and a number \(t\) if \(M\) halts with output \(S\) after \(t\) steps. This relation is decidable. So it is representable in any sufficiently strong arithmetical theory – e.g., in any extension of Q – by some formula \({\scriptstyle \class {smallcaps}{\text {H}}}(x,y,z)\). Let \({\scriptstyle \class {smallcaps}{\text {LEN}}}(x,y)\) represent the (obviously computable) function that maps each program to its length. We can now express “the complexity of pattern \(S\) exceeds \(n\)” in \(\mathfrak {L}_A\) as the claim that there is no program \(x\) of length \(\leq n\) that produces \(S\) after some number of steps \(t\): \(\forall x \forall y \forall t \, (({\scriptstyle \class {smallcaps}{\text {LEN}}}(x,y) \land y \leq \overline {n}) \,\to \, \neg {\scriptstyle \class {smallcaps}{\text {H}}}(x, \ulcorner S \urcorner , t))\). Abbreviate this as \({\scriptstyle \class {smallcaps}{\text {COMPEXC}}}(S, n)\). Chaitin’s Theorem says that beyond some limit \(L\), no such statement is provable.

A nice aspect of this proof is that it works for any reasonable definition of complexity. (That’s why we didn’t need to be very precise about this.) It also works for programs in ordinary programming languages like Python or JavaScript, rather than Turing machine programs, and for data structures that aren’t just patterns of strokes and blanks. Among other things, it shows that there is a number \(L\) such that we can’t prove (in, say, ZFC) of any specific string of bits that it requires a Python program longer than \(L\) to be produced.

We can estimate the value of \(L\). One would certainly need a lot of instructions to program the machine \(M_T\) (in the proof of Theorem 10.4) that takes a number \(k\) as input and then searches through all proofs in \(T\) until it finds a proof of some statement of the form ‘the complexity of \(S\) is greater than \(k\)’. But one wouldn’t need an astronomical number of instructions. 10,000 should be enough. If the doubling machine needs 10 instructions, \(M_n\) needs around \(10 n + 10,000\) instructions, each of which has a fixed length. If the average length of these instructions is, say, 10 (never mind how this is measured), \(d \cdot k + c\) will be around \(100,000 + 100k\). The smallest \(k\) with \(100,000 + 100k < 2^k\) is \(k = 17\). This puts \(L\) at \(2^{17} = 131,072\). For less cumbersome kinds of programs, \(L\) is even smaller. For Python and bit strings, it is well under 10,000.

That’s an astonishingly small number. Imagine a 3D movie of the entire observable universe for its first billion years, at atomic resolution. Could you write a Python program that generates this movie, in under 10 KB, without using external resources? Surely not! Chaitin’s Incompleteness Theorem implies that while this may be true, it can’t be proved.

Like Gödel’s First Incompleteness Theorem, Chaitin’s Incompleteness Theorem shows that certain arithmetical truths are unprovable in PA or ZFC. In 2010, Shira Kritchman and Ran Raz pointed out that there is also a route from Chaitin’s Theorem to the Second Incompleteness Theorem.

We begin with an apparent paradox. There is a finite number of programs of length \(\leq L\). Let \(N\) be that number plus 1. Each number \(n\) between \(1\) and \(N\) can be coded as a pattern of \(n+1\) strokes. Since there are more such numbers than programs of length \(\leq L\), at least one of them must require a program longer than \(L\) to be printed. How many, exactly, require a program longer than \(L\)?

Suppose there is exactly one number \(x\) between \(1\) and \(N\) that requires a program longer than \(L\) to be printed. In that case, we can find that number. We can run all Turing machines whose program has length \(\leq L\). By assumption, at some point, all the \(N\!-\!1\) numbers that can be printed by such machines have been printed. We know that there is at least one number between \(1\) and \(N\) that requires a longer program. So we know that the remaining number must be the one that requires a longer program. We have a proof that the complexity of that remaining number is greater than \(L\). But by Chaitin’s Incompleteness Theorem, we can’t prove this!

This argument seems to show that there can’t be a single number between \(1\) and \(N\) that requires a program longer than \(L\) to be printed. Well, suppose there are exactly two. In that case, we can find them. We run through all Turing machines with programs of length \(\leq L\) until all the \(N-2\) numbers that can be printed by such machines have been printed. We’ve just shown that there must be at least two numbers between \(1\) and \(N\) that require a program longer than \(L\) to be printed. So we can identify these two numbers as the ones that haven’t been printed yet. We have therefore proved that the complexity of these two numbers is greater than \(L\). By Chaitin’s Incompleteness Theorem, this is impossible.

So there can’t be exactly two numbers between \(1\) and \(N\) that require a program longer than \(L\) to be printed. Well, suppose there are exactly three.…

Continuing this line of thought up to \(N\), we can seemingly show that every number between \(1\) and \(N\) is too complex to be printed with a program of length \(\leq L\). But this is evidently false. We can easily show that, say, the number 1 can be printed with a program much shorter than \(L\).

Kritchman and Raz show where the paradoxical argument fails if it is spelled out formally. This requires a theory in which one can formalize the proof of Chaitin’s Theorem. Q is too weak for this, but PA is strong enough. More specifically, PA can prove that there is a number \(L\) such that PA can’t prove of any number \(x\) that the complexity of \(x\) is greater than \(L\) – unless PA is inconsistent, in which case, of course, it proves everything. PA can also prove that there is at least one number between \(1\) and \(N\) whose complexity is greater than \(L\). And it can prove that if there is exactly one such number then PA can find it, by showing that all the other numbers \(y < N\) have complexity at most \(L\), and inferring that the remaining number has complexity greater than \(L\). So PA can prove that if there is exactly one number between \(1\) and \(N\) then PA can prove that the complexity of that number is greater than \(L\).

In the argument above, I said that this contradicts Chaitin’s Incompleteness Theorem. But Chaitin’s Theorem for PA doesn’t quite say that PA can’t prove that the complexity of \(x\) is greater than \(L\). It says that PA can’t prove this if PA is consistent.

If PA could prove its own consistency, it could use Chaitin’s Theorem to conclude that there can’t be exactly one number between \(1\) and \(N\) with complexity greater than \(L\). It could similarly show that there can’t be exactly two such numbers, and so on. It would reach the conclusion that every number between \(1\) and \(N\) has complexity greater than \(L\), which it can also refute, as it can prove that 1 has complexity less than \(L\). Thus, if PA could prove its own consistency, it would be inconsistent.

10.5Philosophy of mind

Gödel’s Incompleteness Theorems, and their corollaries, have profound implications for the foundations of mathematics. They derailed Hilbert’s program. They draw a wedge between truth and provability, showing that there is no way to capture all mathematical truths in an axiomatic system. Some have argued that Gödel’s theorems also have profound implications for our understanding of the human mind: they show that our mathematical capacity goes beyond what any mechanical system (any computer) can achieve.

In its basic form, this argument goes as follows.

Let \(S\) be the set of mathematical sentences that I accept as true. \(S\) includes the axioms of PA. Let \(S^+\) be the set of sentences entailed by \(S\). If my mind is equivalent to a Turing machine, \(S\) is computably enumerable, and \(S^+\) is a computably axiomatizable extension of PA. I can then go through the proof of Gödel’s First Incompleteness Theorem to construct a sentence \(G\) that is true, but not in \(S^+\). This is impossible: since I realize that \(G\) is true, \(G\) is part of my mathematical knowledge: it must be in \(S^+\)! Hence my mind is not equivalent to a Turing machine.

An initial problem with this argument is that the inference to the truth of \(G\) requires the assumption that \(S^+\) is consistent. Gödel’s proof shows that if \(S^+\) is axiomatizable and consistent, then \(G\) is not in \(S^+\). To reach the conclusion that \(G\) is true, the argument therefore assumes that the set \(S^+\) includes the statement that \(S^+\) is consistent. Obviously, \(S^+\) is consistent iff \(S\) is consistent. So the argument assumes that the set \(S\) of my mathematical beliefs includes the statement that this very set is consistent. It’s not enough to believe that “my mathematical beliefs are consistent”; I would also have to be aware of the fact that my mathematical beliefs comprise precisely the set \(S\). Thus one way to escape the argument is to hold that we cannot be fully aware of our mathematical beliefs.

There are other problems with the argument. The concepts of mathematical knowledge and belief are surprisingly difficult to model consistently, especially if we want to allow for beliefs about one’s own beliefs.

Suppose we extend the language of arithmetic by a predicate \(B\) for belief. On its intended interpretation, \(B(\ulcorner A \urcorner )\) is meant to express that I accept the sentence \(A\). (We could use special quote marks to refer to sentences, rather than Gödel numbers. This would make no difference.) We could also add a predicate \(K\) for knowledge.

We might now want to lay down some axioms for \(B\) and \(K\). For example, since knowledge is factive (what is known is true), a minimal theory of mathematical knowledge and belief should include the schema Ref\(_K\):

Suppose such a theory also includes the axioms of Q. In fact, let’s simply consider the theory \(T\) that adds Ref\(_K\) to Q. By the Diagonal Lemma, there is a sentence \(G\) such that \begin {equation} \tag {D} \vdash _{T} G \leftrightarrow \neg K(\ulcorner G \urcorner ). \end {equation} By Ref\(_K\), \(\vdash _{T} K(\ulcorner G \urcorner ) \to G\). Combining this with (D), we get \(\vdash _{T} K(\ulcorner G \urcorner ) \to \neg K(\ulcorner G \urcorner )\), which entails \(\vdash _{T} \neg K(\ulcorner G \urcorner )\). By (D) again, we get \(\vdash _{T} G\).

This shows that the sentence \(G\) that figures in (D) is derivable from the axioms of Q and an instance of Ref\(_K\). One would think that I could know the axioms of Q and the relevant instance of Ref\(_K\). Going through the above reasoning, I could thereby come to know \(G\). But this is incompatible with \(T\), for we’ve just seen that \(\vdash _T \neg K(\ulcorner G \urcorner )\)!

This puzzle is known as the Knower Paradox. If we hold fixed classical logic and the factivity of knowledge (as expressed by Ref\(_K\)), the only way to avoid contradiction is to deny that I can come to know \(G\) by competently going through its proof. Notice that the above argument against the equivalence between my mind and a Turing machine involved a very similar assumption: that I could come to know the Gödel sentence \(G\) of \(S^+\) by going through the proof of Gödel’s Theorem.

The situation for belief is arguably even worse. If we add \(B\) to \(\mathfrak {L}_A\), we can construct a formula \({\scriptstyle \class {smallcaps}{\text {BC}}}(x,y)\) saying that there is a code \(c\) of a sequence of sentences \(A_1, \ldots , A_n\) such that \(B({\scriptstyle \class {smallcaps}{\text {ENTRY}}}(c,i))\) for each \(1 \leq i \leq n\), and \(\exists y {\scriptstyle \class {smallcaps}{\text {PRF}}}_{\mathrm {PA}}(y, \ulcorner A_1 \land \ldots \land A_n \to A \urcorner )\). That is, \({\scriptstyle \class {smallcaps}{\text {BC}}}(\ulcorner A \urcorner )\) is true iff \(A\) is provable in PA from premises that I believe.

Now assume that the set of sentences that I believe is decidable and consistent with PA. (This is surely possible.) Let \(B^*\) be the set of sentences that are provable in PA from premises that I believe. \(B^*\) is a consistent, axiomatizable extension of PA. Without further assumptions about \(B\), one can show that \({\scriptstyle \class {smallcaps}{\text {BC}}}(x)\) satisfies P1–P3. So Löb’s Theorem applies: whenever \(B^*\) contains \({\scriptstyle \class {smallcaps}{\text {BC}}}(\ulcorner A \urcorner ) \to A\), it also contains \({\scriptstyle \class {smallcaps}{\text {BC}}}(\ulcorner A \urcorner )\).

This is highly counterintuitive. For example, one might think that I could believe that \(1\!+\!1\! =\! 3\) does not follow in PA from my mathematical beliefs. (It certainly seems to me as if I believe this!) But if \(\neg {\scriptstyle \class {smallcaps}{\text {BC}}}(\ulcorner 1\!+\!1\!=\!3 \urcorner )\) is in \(B^*\) then so is its tautological consequence \({\scriptstyle \class {smallcaps}{\text {BC}}}(\ulcorner 1\!+\!1\!=\!3 \urcorner ) \to 1\!+\!1\!=\!3\). By Löb’s Theorem, it follows that ‘\(1\!+\!1\!=\!3\)’ is in \(B^*\). That is, I can only believe that ‘\(1\!+\!1\!=\!3\)’ does not follow from my mathematical beliefs if it actually follows from my mathematical beliefs!