# Takeuti's proof of the Second Incompleteness theorem

I am reading Gödel's second incompleteness theorem in Takeuti's "Proof theory" (page 85), and I don't understand how he derives the sequent $$\operatorname{Con},\operatorname{Pr}(\ulcorner A_G\urcorner)\vdash \neg\operatorname{Pr}(\ulcorner\neg A_G\urcorner)$$ (in his notations: $$\operatorname{Consis}_S,\vdash A_G \rightarrow \neg\vdash \neg A_G$$), where $$A_G$$ is the Gödel sentence. He writes that this follows from Lemma 10.5, but I do not see the connection.

I would be grateful if anybody could cast some light on this.

P.S. Actually, if there is a more or less simple way to derive the sequent $$\operatorname{Con}\vdash A_G,$$ I hope, somebody will give a hint. Takeuti's reasoning seems too long (and too vague) to me.

In the interests of readability, I will use "$$Pr$$" for the S-provability predicate and reserve "$$\vdash$$" for the metatheoretic provability relation. I think this is the major readability issue.

I will also rudely conflate formulas with their Godel numbers. Less rudely and more superficially, I will write "$$Con$$" for Takeuti's "$$\overline{Consis_{\bf S}}$$" and "$$G$$" for Takeuti's "$$A_G$$."

I think that Lemma 10.5 itself, which is the metatheoretic statement that S is consistent iff it does not prove the specific sentence $$\perp$$, is not really relevant; rather, we want the internal version, namely that for each sentence $$A$$ (in particular, for $$A=G$$) we have

$$(*)\quad {\bf S}\vdash Con\rightarrow \neg (Pr(A)\wedge Pr(\neg A)).$$

This internalization was not, as far as I can tell, something Takeuti stated explicitly, but it's easy enough to prove on its own (specifically, prove in S that $$Pr(A)\wedge Pr(\neg A)\rightarrow Pr(0=1)$$ and then look at the contrapositive).

To see why $$(*)$$ is relevant, note that taking $$A=G$$ and applying some basic logical manipulations it yields $${\bf S}\vdash Con\wedge Pr(G)\rightarrow\neg Pr(\neg G).$$ Since $${\bf S}\vdash \neg G\leftrightarrow Pr(G)$$ this in turn yields $$\color{green}{{\bf S}\vdash Con\wedge Pr(G)\rightarrow \neg Pr(Pr(G))}.$$

So what? Well, we also have that S proves that it proves the things it proves - that is, for every sentence $$A$$ we have $${\bf S}\vdash Pr(A)\rightarrow Pr(Pr(A)).$$ Again taking $$A=G$$ (and adding $$Con$$ as a dummy hypothesis) yields $$\color{blue}{{\bf S}\vdash Con\wedge Pr(G)\rightarrow Pr(Pr(G)).}$$

Now combining the green and blue deductions above and applying more basic logical manipulations yields $${\bf S}\vdash Con\rightarrow \neg Pr(G)$$. Since $${\bf S}\vdash G\leftrightarrow\neg Pr(G)$$, this yields the desired deduction $$\color{red}{{\bf S}\vdash Con\rightarrow G.}$$

• Noah, this implication $$Pr(A)\wedge Pr(\neg A)\rightarrow Pr(0=1),$$ how is it derived? – Sergei Akbarov Nov 22 '19 at 6:32
• @SergeiAkbarov S can prove basic facts about the provability predicate. For example, for any $A$ and $B$ it can prove $$Pr(A)\wedge Pr(\neg A)\rightarrow Pr(A\wedge\neg A)$$ and $$Pr(A\wedge\neg A)\rightarrow Pr(B).$$ This is basically immediate from the definition of "$Pr$" (both of those correspond to basic proof rules). – Noah Schweber Nov 22 '19 at 14:42
• Noah, thank you! – Sergei Akbarov Nov 22 '19 at 16:13
• @SergeiAkbarov Happy to help! – Noah Schweber Nov 22 '19 at 16:14