2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Noah, this implication $$ Pr(A)\wedge Pr(\neg A)\rightarrow Pr(0=1), $$ how is it derived? $\endgroup$ – Sergei Akbarov Nov 22 '19 at 6:32
  • 1
    $\begingroup$ @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). $\endgroup$ – Noah Schweber Nov 22 '19 at 14:42
  • $\begingroup$ Noah, thank you! $\endgroup$ – Sergei Akbarov Nov 22 '19 at 16:13
  • 1
    $\begingroup$ @SergeiAkbarov Happy to help! $\endgroup$ – Noah Schweber Nov 22 '19 at 16:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.