18
The Unprovability of Consistency
According to Godel’s¨ second incompleteness theorem, the sentence expressing that a theory like P is consistent is undecidable by P, supposing P is consistent. The full proof of this result is beyond the scope of a book on the level of the present one, but the overall structure of the proof and main ingredients that go into the proof will be indicated in this short chapter. In place of problems there are some historical notes at the end.
Officially we defined T to be inconsistent if every sentence is provable from T , though we know this is equivalent to various other conditions, notably that for some sentence S, both S and S are provable from T . If T is an extension of Q, then since 0 = 1 is the simplest instance of the first axiom of Q, 0 = 1 is provable from T , and if 0 = 1 is also provable from T , then T is inconsistent; while if T is inconsistent, then 0 = 1 is provable from T , since every sentence is. Thus T is consistent if and only if 0 = 1 is not provable from T . We call PrvT ( 0 = 1 
), which is to
say y PrfT ( 0 = 1 , y), the consistency sentence for T . Historically, the original paper of Godel¨ containing his original version of the first incompleteness theorem (corresponding to our Theorem 17.9) included towards the end a statement of a version of the following theorem.
18.1 Theorem* (Godel’s¨ second incompleteness theorem, concrete form). Let T be a consistent, axiomatizable extension of P. Then the consistency sentence for T is not provable in T .
We have starred this theorem because we are not going to give a full proof of it. In gross outline, Godel’s¨ idea for the proof of this theorem was as follows. The proof of Theorem 17.9 shows that if the absurdity 0 = 1 is not provable in T then the Godel¨ sentence GT is not provable in T either, so the following is true: PrvT ( 0 = 1 ) →PrvT (
GT ). Now it turns out that the theory P of inductive arithmetic, and hence any extension T thereof, is strong enough to ‘formalize’ the proof of Theorem 17.9, so we have
T PrvT ( 0 = 1 ) → PrvT ( GT ).
But GT was a Godel¨ sentence, so we have also
T GT ↔ PrvT ( GT ).
232
THE UNPROVABILITY OF CONSISTENCY |
233 |
And so we have
T PrvT ( 0 = 1 ) → GT .
So if we had T PrvT ( 0 = 1 ), then we would have T GT , which by Proposition 17.9 we do not.
Of course, the key step here, of which we have not given and are not going to be giving the proof, is the claim that a theory like P is strong enough to ‘formalize’ the proof of a result like Theorem 17.9. Godel’s¨ successors, beginning with Paul Bernays, have analyzed just what properties of PrvT are actually essential to get the second incompleteness theorem, finding that one does not really have to ‘formalize’ the whole proof of Theorem 17.9, but only certain key facts that serve as lemmas in that proof. We summarize the results of the analysis in the next two propositions.
18.2 Lemma*. Let T be a consistent, axiomatizable extension of P, and let B(x) be the formula PrvT (x). Then the following hold for all sentences:
(P1) |
If T A then T B( A ) |
(P2) |
T B( A1 → A2 ) → (B( A1 ) → B( A2 )) |
(P3) |
T B( A ) → B( B( A ) ). |
Again we have starred the lemma because we are not going to give a full proof. First we note a property not on the above list:
(P0) |
If T A1 → A2 and T A1, then T A2. |
This is a consequence of the Godel¨ completeness theorem, according to which the theorems of T are just the sentences implied by T , since if a conditional A1 → A2 and its antecedent A1 are both implied by a set of sentences, then so is its consequent A2. Whatever notion of proof one starts with, so long as it is sound and complete, (P0) will hold. One might therefore just as well build it into one’s notion of proof, adding some appropriate version of it to the rules of one’s proof procedure. Of course, once it is thus built in, the proof of (P0) no longer requires the completeness theorem, but becomes comparatively easy. [For the particular proof procedure we used in Chapter 14, we discussed the possibility of doing this in section 14.3, where the version of (P0) appropriate to our particular proof procedure was called rule (R10).]
(P1) holds for any extension of Q, since if T A, then PrvT (
A 
) is correct, and being an -rudimentary sentence, it is therefore provable in Q. (P2) is essentially the assertion that the proof of (P0) (which we have just said can be made comparatively easy) can be ‘formalized’ in P. (P3) is essentially the assertion that the (by no means so easy) proof of (P1) can also be ‘formalized’ in P. The proofs of the assertions (P2) and (P3) of ‘formalizability’ are omitted from virtually all books on the level of this one, not because they involve any terribly difficult new ideas, but because the innumerable routine verifications they—and especially the latter of them—require would take up too much time and patience. What we can and do include is the proof that the starred lemma implies the starred theorem. More generally, we have the following:
234 |
THE UNPROVABILITY OF CONSISTENCY |
18.3 Theorem (Godel’s¨ second incompleteness theorem, abstract form). Let T be a consistent, axiomatizable extension of P, and let B(x) be a formula having properties
(P1)–(P3) above. Then not T B( 0 = 1 ).
The proof will occupy the remainder of this chapter. Throughout, let T be an extension (not necessarily consistent) of Q. A formula B(x) with properties (P1)– (P3) of Lemma 18.2 we call a provability predicate for T . We begin with a few words about this notion. The formula PrvT (x) considered so far we call the traditional provability predicate for T , though, as we have indicated, we are not going to give the proof of Lemma 18.2, and so are not going to be giving the proof that the ‘traditional provability predicate’ is a ‘provability predicate’ in the sense of our official definition of the latter term.
If T is ω-consistent, taking the traditional PrvT (x) for B(x), we have also the following property, the converse of (P1):
(P4) |
If T B( A ) then T A. |
[For if we had T PrvT (
A ), or in other words T y PrfT ( A , y), but did not haveT A, then for each b, PrfT ( A , b) would be correct and hence provable in Q and hence in T , and we would have an ω-inconsistency in T .] We do not, however, include ω-consistency in our assumptions on T , or (P4) in our definition of the technical term ‘provability predicate’. Without the assumption of (P4), which is not part of our official definition, a ‘provability predicate’ need not have much to do with provability. In fact, the formula x = x is easily seen to be a ‘provability predicate’ in the sense of our definition.
On the other hand, a formula may arithmetically define the set of Godel¨ numbers of theorems of T without being a provability predicate for T . If T is consistent and PrvT (x) is the traditional provability predicate for T , then not only does PrvT (x) arithmetically define the set of Godel¨ numbers of theorems of T , but so does the formula Prv*T (x), which is the conjunction of PrvT (x) with PrvT ( 0 = 1 
), since the second conjunct is true. But notice that, in contrast to Theorem 18.1, Prv*T (
0 = 1 ) is provable in T . For it is simply
(PrvT ( 0 = 1 ) & PrvT ( 0 = 1 ))
which is a valid sentence and hence a theorem of any theory. The formula Prv*T (x), however, lacks property (P1) in the definition of provability predicate. That is, it is not the case that if T A then T Prv*T ( A ). Indeed, it is never the case that
T Prv*T (
A ), since it is not the case that T PrvT ( 0 = 1 
), by Theorem 18.1. The traditional provability predicate PrvT (x) has the further important, if nonmathematical, property beyond (P0)–(P4), that intuitively speaking Prv(x) can plausibly be regarded as meaning or saying (on the standard interpretation) that x is the Godel¨ number of a sentence that is provable in T . This is conspicuously not the case for Prv*T (x), which means or says that x the Godel¨ number of a sentence that is provable in T and T is consistent.
The thought that whatever is provable had better be true might make it surprising that a further condition was not included in the definition of provability predicate,
THE UNPROVABILITY OF CONSISTENCY |
235 |
namely, that for every sentence A we have
(P5) T B( A ) → A.
But in fact, as we also show below, no provability predicate fulfills condition (P5) unless T is inconsistent.
Our next theorem will provide answers to three questions. First, just as the diagonal lemma provides a sentence, the Godel¨ sentence, that ‘says of itself’ that it is unprovable, so also it provides a sentence, the Henkin sentence, that ‘says of itself’ that it is provable. In other words, given a provability predicate B(x), there is a sentence
HT such that T HT ↔ B( HT ). Godel’s¨ theorem was that, if T is consistent, then the Godel¨ sentence is indeed unprovable. Henkin’s question was whether the Henkin sentence is indeed provable. This is the first question our next theorem will answer. Second, call a formula Tr(x) a truth predicate for T if and only if for every sentence A of the language of T we have T A ↔ Tr (
A 
). Another question is whether, if T is consistent, there can exist a truth predicate for T . (The answer to this question is going to be negative. Indeed, the negative answer can actually be obtained directly from the diagonal lemma of the preceding chapter.) Third, if B(x) is a provability predicate, call B(
0 = 1 ) the consistency sentence for T [relative to B(x)]. Yet another question is whether, if T is consistent, the consistency sentence for T can be provable in T . (We have already indicated in Theorem 18.3 that the answer to this last question is going to be negative.)
The proof of the next theorem, though elementary, is somewhat convoluted, and as warm-up we invite the reader to ponder the following paradoxical argument, by which we seem to be able to prove from pure logic, with no special assumptions, the existence of Santa Claus. (The argument would work equally well for Zeus.) Consider the sentence ‘if this sentence is true, then Santa Claus exists’; or to put the matter another way, let S be the sentence ‘if S is true, then Santa Claus exists’.
Assuming |
|
(1) |
S is true |
by the logic of identity it follows that |
|
(2) |
‘If S is true, then Santa Claus exists’ is true. |
From (2) we obtain |
|
(3) |
If S is true, then Santa Claus exists. |
From (1) and (3) we obtain |
|
(4) |
Santa Claus exists. |
Having derived (4) from the assumption (1) we infer that without the assumption (1), indeed without any special assumption, that we at least have the conditional conclusion that if (1), then (4), or in other words
(5) |
If S is true, then Santa Claus exists. |
236 THE UNPROVABILITY OF CONSISTENCY
From (5) we obtain
(6) |
‘If S is true, then Santa Claus exists’ is true. |
By the logic of identity again it follows that |
|
(7) |
S is true. |
And from (5) and (7) we infer, without any special assumptions, the conclusion that
(8) |
Santa Claus exists. |
18.4 Theorem (Lob’s¨ |
theorem). If B(x) is a provability predicate for T , then for any |
sentence A, if T B( A ) → A, then T A. |
|
Proof: Suppose that B is a provability predicate for T and that |
|
(1) |
T B( A ) → A. |
Let D(y) be the formula (B(y) → A), and apply the diagonal lemma to obtain a |
|
sentence C such that |
|
(2) |
T C ↔ (B( C ) → A). |
So |
|
(3) |
T C → (B( C ) → A). |
By virtue of property (P1) of a provability predicate, |
|
(4) |
T B( C → (B( C ) → A)). |
By virture of (P2), |
|
(5)T B( C → (B( C ) → A) ) → (B( C ) → B( B( C ) → A )).
From (4) and (5) it follows that
(6) |
T B( C ) → B( B( C ) → A ). |
By virtue of (P2) again, |
|
(7) |
T B( B( C ) → A ) → (B( B( C ) ) → B( A )). |
From (6) and (7) it follows that |
|
(8) |
T B( C ) → (B( B( C ) ) → B( A )). |
By virtue of (P3),
(9)
From (8) and (9) it follows that (10)
From (1) and (10) it follows that (11)