Gödel's Second Incompleteness Theorem

Godel's Second Incompleteness Theorem Let r be a recursively axiomatized theory that includes Q. The proof of Godel's first incompleteness theorem proceeded by constructing a sentence o such that (1) (0 Bewr([ro I])) is a theorem. Having this, it was straightforward to prove the following: If (2) r is consistent, then o isn't provable in r . We can formulate this result withing the language of arithmetic. Using "Con(r)" to abbreviate "-Bewr([r- 0 - 0 I])," we formalize (2) as: (3) (Con(r) -- Bewr([r I])). (1) and (3) together give us: (Con(r) (4) Provided that o). r includes PA, we can formalize the derivation of (4) within r.Hence we have: (5) Bewr([ r(Con(r) Because the set of theorems of (6) - ~)l]). r is closed under modus ponens, (5) gives us: {Bewr([rCon(r)l] - Bewr([rol])) (3) and (6) together tautologically imply: (7) (Con(r) -- Bewr([rCon(r)l])). Thus we have: Second Incompleteness Theorem. No consistent, recursively axiomatized theory that includes PA can prove its own consistency. Proof: I don't really want give a proof of ( 9 , which would be unbearably long and boring. I'll be content with a sketch. The proof depends on three principles, which were first singled out by M. H. Lob: Second Incompleteness Theorem, p. 2 If I? 1 4 , then I? tBewr([r@]). (L1) (L2) t ( ~ e w r ( [ ~ @+l )Bewr([Bewr([ r@l)'l)). (L3) t ( ~ e w r ('(4 [ - $)'I) (Bewr([ '@I) - Bewr([ W'l))). (Ll) we proved earlier, when we showed that "Bewr(x)" weakly represents { r@ : 4 is a ) , so, since I? consequence of I?) in Q. This tells us that, if I? 1 4 , then Q t ~ e w ~ ( [ r @ ]and includes Q, I? t ~ e w ~ ( [ ~ @ ] ) . (L2) is the formalized statement of (Ll). To prove it, we formalize our proof that every true x sentence is provable in I?. First we show, by induction on the complexity of terms, that, for each term T(x1,...,%), I? t(vzl)...(vG)w%+l)(~(zl,...,4 = G+l Bewr([T(xl,...%) - %+I/ / [ Z l 1 ~ ~ ~ ~ [%+ill)). ~~%1 = %+,I 1 Next show, by induction on the complexity of bounded formulas, that for each bounded formula $(~1,...,%), t(v~l)...(v~)($(zl,... ,GI Next, prove the same thing for $ a - ~ e w r (r[ $ ( ~ ~ ~ ~ ~ ~ ~ ~ x l ~ [ Z l l ~ ~ ~ x " ~ x formula, by induction on the length of the initial existential quantifier prefix. The key fact we need is that our rules of proof include Existential Generalization. Because Bewr(x1) is a formula, a special case of this principle will be: - (vzl)(~ewr(zl) Bewr([ ~ewr(xl)'X1/[zllI)). We get (L2) by instantiating with [r@]. A detailed proof would be quite laborious. To prove (L3), simply note that, if we have proofs of ( 4 - $) and 4 , we get a proof of $ by taking the two proofs together, then adding $ at the end by the rule Modus Ponens. All we need to know is that the arithmetical concatenation operation works properly. Second Incompleteness Theorem, p. 3 Now that we have (L1)-(L3), we want to see how to utilize them to get the Second Incompleteness Theorem. The Self-Referential Lemma gives us a sentence o such that (a) 1 - - Bewr([r~l])). I? ( 0 We have, (b) 1 - - Bewr([r~l]))). I? ( 0 (Ll) lets us derive: (c) - I? t ~ e w ~ ( [ r ( o- Bewr([r~1]))1]). Applying (L3), we get: (dl - I? t ( ~ e w ~ ( [ r ~ lBewr([r]) Bewr(['ol])l])). (L2) gives us this: (el - -- t ( ~ e w r ( [ ~ o l l )Bewr([Bewr([ roll)ll)) (- Bewr([r~l]) (Bewr([r~l]) 0 = 0)) is a tautology, hence a theorem of I?, so that by (Ll) we have: (f) I? t ~ e w ~ ( [ r Bewr([rW]) (- + (Bewr([rW]) -- 0 = O))7]). Two applications of (L3) give us: (g) I? t ( ~ e w ~ ( [ r - ~ e w ~ ( [ r ~ ] () B 7 ]e)~ ~ ( [ B e w ~ ( [ ~ 0 ~ ] ) 7 ] ) + Bewr([r- 0 = 011))). (d), (e), and (g) yield, by truth-functional logic: - (h) I? t ( ~ e w ~ ( [ r ~ lBewr([r]) 0 = 011)). (9 I? t(Con(I?) -- Bewr([ roll)), using the definition of "Con." This and (a) give us: (i - I? t(~on(I?) o). + Second Incompleteness Theorem, p. 4 We want to show that, if is consistent, Con(r) isn't provable in r.Equivalently, we want to show that, if Con(r) is provable in I?, then I? is inconsistent. Toward this end, suppose that 0 r 1con(r). (j) and (k) yield: (1) r 10. By (Ll), we get: (m) t~ew~([r~l]). (a) and (m) give us: (n) r 1- O. (1) and (n) show us that I? is inconsistent, as requiredB The First Incompleteness Theorem was a little disappointing. Sure, it did what it was advertised as doing, giving us a true, unprovable sentence. But the sentence it gave us was an out-of-the-way statement that, apart from its appearance in the First Incompleteness Theorem, no one would ever have been interested in. The theorem left open the possibility that there aren't any interesting statements that aren't provable in PA. With the Second Incompleteness Theorem, our disappointment dissipates, for we certainly are interested in knowing whether our theories are consistent. Thus Con(PA) is an important truth that isn't provable in PA. We've proved the Second Incompleteness Theorem for the language of arithmetic, but the same proof will work for any language into which we can translate the language of arithmetic. In particular, we can prove that, if axiomatic set theory is consistent, then it cannot prove its own consistency. This discovery stopped Hilbert's program dead in its tracks. Hilbert Second Incompleteness Theorem, p. 5 hoped to prove the consistency of the axioms of set theory in a system much weaker than axiomatic set theory. It turns out that (assuming axiomatic set theory is consistent) proving its consistency will require a theory stronger than axiomatic set theory. So if you're worried about the consistency of set theory, you won't get a consistency proof that helps. By using interpretations, we can extend the proof of the Second Incompleteness Theorem to theories like the Zermelo-Fraenkel axioms for set theory, theories that are substantially richer than PA. We can use the same technique to extend the proof to theories that are substantially weaker than PA, like Q. We cannot prove the Second Incompleteness Theorem for Q directly, by proving analogues to (L1)-(L3), with "BewQ" in place of Bew,,." To prove (L2), we need induction, and in Q we don't have induction. To obtain the Second Incompleteness Theorem for Q, and for other theories that include Q, one has to be more devious. We first produce a theory I? that, although weaker that PA - it's obtained from PA by restricting the induction axiom schema - is nonetheless strong enough to prove Second Incompleteness Theorem. Next, we interpret I? into Q by giving a translation that leaves the nonlogical terms alone but suitably restricts the quantifiers. If we had a proof of CON(Q) in Q, we could get a proof of CON(I?) in r.The details of the proof, which is mainly due to Alex Wilkie, are delicate, and all I can do here is give you the URL for Sam Buss's web site, where you can find the proof written out; it's http://www.math.ucsd.edu/-sbussResearchWeb/handbooldI/index.html. Refocusing our attention on PA, if we think a sentence 0 is true, we'll think it's consistent; that is, we would expect to have the following: (Y 'Con({y 1)- Second Incompleteness Theorem, p. 6 All instances of this schema are, in fact, provable in PA. The proof isn't easy, and I won't attempt it here. It follows that, if the theory I? is finitely axiomatized, it proves its own consistency. Consequently, by the Second Incompleteness Theorem, if I? is finitely axiomatized and it includes PA, then I? is inconsistent. Thus we have the following: Theorem (Ryll-Nardzewski). No consistent theory in the language of arithmetic that includes PA can be finitely axiomatized. This theorem is not as resilient as most of the results we have been studying, which generalize from the language of arithmetic to other languages into which you can translate the language of arithmetic. Ryll-Nardzewski's theorem, and the schema (y - Con({y))) that backs it up, are brittle. They hold for the language of arithmetic, but they don't necessarily hold for other languages that include the language of arithmetic. Let us say - this is a little vague, but bear with me- that we consciously accept an arithmetical theory I? if, upon reflection, we are willing to agree that all the members of I ' are true. (Keep in mind what we learned from Tarski, that, whereas the general notion of truth is philosophically suspicious, truth in the language of arithmetic is unexceptionable.) If we think that all the members of I? are true, then we must surely think that I? is consistent, since we know the Soundness Theorem, which tells us that the members of an inconsistent set of sentences can't all be true. Thus if I? is a recursively axiomatized set of sentences that includes PA, then if we consciously accept I?, we'll accept Con(I?). Let I? be the set of arithmetical sentences that we are, upon careful reflection, willing to accept. Assuming, pace Lucas and Penrose, that we I? is effectively enumerable, that if we consciously accept I?, then we'll accept Con(I?), which means, by the Second Incompleteness Second Incompleteness Theorem, p. 7 Theorem, that I? is inconsistent. This puts a limitation on our capacity for self-knowledge. Assuming the set of arithmetical sentences we accept is consistent, we can't consciously accept the set of arithmetical sentences we accept. Perhaps we consciously accept each finite subset of the set of arithmetical sentences we accept, but we won't consciously accept the whole thing. There are a couple of ways this could happen. The most likely scenario is that we aren't sufficiently aware of our own mental state to be able to identifl the set of arithmetical sentences we accept. This is, it seems to me, the normal human condition. We can, however, imagine science-fiction cases in which a futuristic brain scan reveals to us exactly which sentences we accept by, as it were, discovering our brain's wiring diagram. Arranging it that, at a particular time, we know a Godel code1 of the set of arithmetical sentences we are willing to accept at that time is not entirely straightforward, even if the have the full medical resources of the starship Enterprise at our disposal. The trouble is that our arithmetical beliefs aren't entire the product of apriori cogitation. Some of our arithmetical beliefs we have because of sensory experiences we've had, for example, hearing a lecture or reading a book, and we may expect that our beliefs will change in the future on the basis of new sensory experiences. In particular, if a computer analysis of a brain snapshot taken at time t, tells me that the set of my arithmetical sentences I accept has Godel code k, I might respond to this knowledge by accepting that the set of sentences with Godel code k is consistent. But this won't mean that I believe a set of sentences that implies its own consistency. Instead, the set of my arithmetical beliefs at a later time t,, after I've seen the computer printout, includes the statement that the set of sentence I 1 We may that the Godel code of a recursively enumerable set to be the Godel number of a E formula that has the set as its extension. Second Incompleteness Theorem, p. 8 believed at an earlier time tois consistent. To arrange things so that, at a particular time, we have a code of the set of arithmetical sentences we are willing to accept at that time, we have to be more devious. A complete circuit analysis of your brain ought to tell you, not only what sentences you accept, but what sentences you would accept in response to various sensory inputs you might have in the future, in the same way that a complete circuit analysis of an adding machine would tell you how the machine would respond to various possible combinations of keystrokes. It will provide you with a detailed description of a h c t i o n f, such that, for any possible sensory input i, f(i) is a Godel code of the set of arithmetical sentences you will accept after experiencing i. Call this h c t i o n f your transition f ~ n c t i o n . ~ There's no telling how new sensory inputs will affect your mental states. Perhaps the song of a mockingbird will awaken an erstwhile dozing corner of your brain an enable you to enjoy a mathematical insight that would otherwise have been unavailable. We are trying to show that, if the clockwork model of the mind is correct, it is theoretically possible, with enough effort, resourcefulness, and technical firepower, for you to put yourself in a position in which you know a Godel code for the set of arithmetical sentences you are willing to accept. To that end, let's try to minimize the effects of random disturbances like mockingbird calls, and focus our attention on the question how to accommodate the fact that, typically, learning your mental state is going to change your mental state. So suppose that you are put into a sensory deprivation chamber, where the only sensory stimulation you are in a position to enjoy is an Arabic numeral, 2 To keep things tolerably simple, I am supposing that your brain is deterministic. In real life, the jury is still out on this, or so I understand. Second Incompleteness Theorem, p. 9 which will appear on a LED display. Using the number k as a code for the state in which the numeral for k appears on the LED display, we can treat your transition function as having numerical inputs. As you enter the sensory deprivation chamber, a snapshot of your brain is taken and fed into a computer, which determines the Godel code of your transition function. The Arabic numeral for this code is then flashed on the LED display. Let's say the number is k. Then, after you see the display, you'll know the Godel number of the set of arithmetical sentences you are willing to accept. It's the output of the function with Godel code k - call it "f' - on input k. You'll know your own Godel number. Now that you know that you are willing to accept all the members of the set coded by f(k), should you also be willing to accept that all the members of the set are true? For each sentence in the set, you have good enough reason to accept the sentence, so you have good enough reason to accept that the sentence is true. But this doesn't show that you have reason to accept that all the sentences in the set are true, since we sometimes find ourselves in a position to accept each instance of a generalization without being in a position to accept the generalization. If you are in a position to accept the thesis that all the members of f(k) are true, the evidence that leads you to accept it will be psychological, not mathematical. Observing the LED didn't give you any new mathematical insights. What it told you, assuming you trust the instruments, is something about your psychological states. The question is, now that you know the psychological fact that you are willing to accept all the outputs of f(k), does this give you good reason to accept that all the outputs of f(k) are true? I can imagine you reasoning like this, "I know that I am careful, methodical, and clever, and that I don't accept things without good reason. I'm not the sort of person who makes Second Incompleteness Theorem, p. 10 mathematical mistakes. So I can be confident that the things I am willing to accept are true." I hope you don't reason this way, because to me it sounds terribly arrogant. And, indeed, such arrogance is promptly punished. If you accept that a the things you are willing to accept are true, you'll be willing to accept that the things you are willing to accept are consistent, and this means, by the Second Incompleteness Theorem, that the things you are willing to accept are inconsistent. You might try to overcome the accusation of arrogance by adopting higher standards of acceptance, taking advantage of the fact that "willing to accept" is a vague term. "Most of the time," you will admit, "I am as error prone as the next fellow. But right now, when I talk about 'accepting' an arithmetical statement, I mean that I am willing to embrace the statement under the very highest standards of meticulous mathematical rigor. That's how I'm using the word 'accept' here, and I have programmed the transition-function-recognition program to reflect this high standard of rigor. Surely, if I have such elevated epistemic criteria, I can be confident that the things I am willing to accept are true." The trouble is that, while adopting these very high standards does indeed make it more reasonable to believe that they things you are willing to accept are true, this belief in your own veracity, while reasonable, isn't secure enough to pass your very high standards. Raising standards makes it harder for your beliefs to count as "accepted," including your belief that the things you accept are true. In the end, I think the moral to be drawn fiom the Lucas-Penrose argument is a lesson in humility. We human beings are highly fallible, and we can't be sure, even when we're reasoning carehlly, that the things we accept are true, or even consistent. Second Incompleteness Theorem, p. 11 Let us return our attention to the case in which our theory I? is something like Peano arithmetic, that we consciously accept. That means that we not only suppose that the members of I? are consistent; we believe that they're true. Of course, the statement that the members of I? are true, unlike the statement that I? is consistent, isn't something that we are able to express within the language of arithmetic. But our belief that I? is true will have repercussions for what purely arithmetical sentences we are willing to accept. For a given arithmetical sentence 4 , we might or might not know whether 4 is true, but we will know, because we regard all the members of I? as true and we recognize that all the consequences of a true theory are true, that, if 4 is a consequence of I?, 4 is true. That is, we are willing to accept all of the so-called Reflection Axioms: (Bewr([ r@l) - 4)- The Reflection Axioms are called that because we get them, not directly from I?, but by reflecting on the fact that I? is a theory that we are willing to acknowledge as true. The Reflection Axioms are statements we are willing to accept in virtue of our conscious willingness to accept I?. Which of them are actually consequences of I?? Well, of course, if 4 is a consequence of I?, then the conditional (Bewr([r@]) - 4 ) is a consequence of I?, since you can prove a conditional by proving its consequent. It turns out that these are the only Reflection Axioms that are provable in I?: Lob's Theorem. If is a recursive set of sentences that includes PA, the Reflection Axiom (Bewr([r@]) 4 is a consequence of I?. - 4 ) is a consequence of I? only if Second Incompleteness Theorem, p. 12 We can derive the Second Incompleteness Theorem as a special case of Lob's Theorem - by setting 4 equal to " 0 = 0." Conversely, we can derive Lob's Theorem from the Second Incompleteness Theorem. That wasn't the way Lob proved the theorem initially; it's a later proof, due to Saul Kripke. Proof (Kripke): The key fact we use is that, for any Jr and 8 , Bewr([qJr - 8)1]) is provably equivalent to B e ~ ~ ~ { ~ , ( [ This @ l ]is) .easy to see. If we have a derivation of (Jr - 8 ) from I?, we can get a derivation of 8 from I? u {Jr) by adding Jr as a line by Premise Introduction, then adding 8 by Modus Ponens. If, conversely, we have a proof of 8 from I? u {Jr), we get a derivation of (Jr - 8 ) from I' by Conditional Proof. We prove Lob's theorem by proving its contrapositive, that is, by assuming that 4 isn't a consequence of I? and deriving that consequence that (Bewr([r@]) I?. Since 4 isn't a consequence of I?, I? u - 4 ) isn't a consequence of {- 4 ) is consistent. It follows from the Second Incompleteness theorem that I' u {- 4 ) doesn't prove its own consistency, so that we have: r u 1- 4 ) $con(r u 1- $1). I? u {- 4 ) $- ~ewr,,{-~,([~ - 0 = 0'1). I? u {- 4 ) $- Bewr([r(- 4 -- 0 = 0)ll). 41 $ - ~ e w r ( [ '@I) (because (- 4 - 0 = 0) and 4 are provably equivalent). I' u {- - I?$(- 4 + -Be~r([~@l))- $ ( ~ e w r ( ['@I) - $)-m The way Lob's Theorem came about was this: Godel constructed a sentence that asserted its own unprovability in PA, and he showed that that sentence was true but unprovable in PA. Second Incompleteness Theorem, p. 13 Leon Henkin was curious what would happen if, instead, you constructed a sentence that asserted its own provability in PA. Would such a sentence be provable? Would it be true? Lob answered Henkin's question by showing that, if 4 is a sentence that asserts its own provability in PA, so that PA Be~r([~@l)), then 4 is provable in PA (and so true). Lob sent his paper to the Journal of Symbolic Logic, which sent it to Henkin to referee. Henkin noticed that Lob's proof only used the right-to-left direction of the hypothesis. Thus Lob's Theorem, as we have it today, was born. Here is Lob's proof: Proof (Lob): Given 4 , use the Self-Referential Lemma to construct a sentence 6 such that: (9 I' t ( 6 - (Bewrt[ r 6 a - 4)). (i) yields this, by sentential calculus: (ii) I' I@ + (Bewrtr r611) + 4))- (Ll) gives us this: (iii) I' t ~ e w r (r(6 [ + (Bewr([ r6'1) + 4)YI). Two applications of (L3) give us this: (iv) I' t(~ewr([~6'1) + (~ewr([~ewr([~6'lY + lBewr(['@l))). ) (L2) yields this: (v) I' t(~ewr([~6'1) + Be~r([Bewr([~6'lYl)). By a truth-functional inference of the form Second Incompleteness Theorem, p. 14 - :. - (a (P (a P) (a Y)) y) we derive: (vi) I' t ( ~ e w r ('&I) [ - ~ e w r ('@'I))[ Assume, as the hypothesis of Lob's Theorem: (vii) I' t(Bewr(['@'l) - 0). (vi) and (vii) give us this: (viii) I' t(Bewr(['6'1) (i) and (viii) give us: 0x1 r 1s. Using (Ll), we derive: (XI r Isewr([ r611). (viii) and (x) give us: (xi) as required. I? 10, + 9)