Takeuti's proof of the Second Incompleteness theorem

Question

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.

Answer 1

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.}$$