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