In the last exercise of the last chapter Computability and Logic of Boolos et al we are asked to use $GL$'s arithmetical soundness theorem to find a weaker assumption than the $\omega$-consistency of $PA$ to show that the Gödel Sentence of PA, $G$, is not disprovable in $PA$.

Since $PA\vdash G\leftrightarrow \neg Prv(\ulcorner G\urcorner)$, we have $PA\vdash \neg G \leftrightarrow Prv(\ulcorner G\urcorner)$, whose corresponding modal sentence is $q\leftrightarrow\square\neg q$. I worked out the fixed point of this, and it results in $q\leftrightarrow \square \bot$, so by Arithmetical Soundness we have that $PA\vdash \neg G \leftrightarrow Prv(\ulcorner 0=1\urcorner)$.

So the disprovability of $G$ is equivalent to the affirmation of the existence a proof of inconsistency,... that is, is equivalent to the $\omega$-inconsistency of the existential predicate $Prv(\ulcorner 0=1\urcorner)$, given the consistency of $PA$.

Is there a way I am missing to strengthen this somewhat dissapointing result?

  • 1
    $\begingroup$ Are you sure about $q↔□¬q$ ?. $\endgroup$ – Mauro ALLEGRANZA Mar 6 '16 at 14:10
  • 2
    $\begingroup$ Page 337 (middle): 27.13 Example: "When $α(x)$ is $\lnot Prv(x)$, then $π_α$ is the Godel sentence, $A(p)$ is $\lnot □ p$, and $H$ is (according to Table 27-1) $\lnot □⊥$, so $η$ is the consistency sentence $\lnot Prv(0=1)$, and since $P \vdash π_α ↔ \lnot Prv(0 = 1)$, we get the result that ... *the Godel sentence is provably equivalent in P to the consistency sentence". $\endgroup$ – Mauro ALLEGRANZA Mar 6 '16 at 14:16
  • $\begingroup$ @MauroALLEGRANZA I am taking the realization $q^\phi = \neg G$, thought I am not enterely convinced that the relettering is legal. I can extend the argument if you think is important. $\endgroup$ – Jsevillamol Mar 6 '16 at 14:32
  • $\begingroup$ @MauroALLEGRANZA That part is consistent with my result, and precisely the cause I asked. It seemed to me like I should be able to infer another equivalence using fixed-point reasoning, since the equivalence pointed in the book is not that different from $\omega$-consistency (as I tried to convey in my question). I guess I was expecting something like $PA\vdash \neg G \leftrightarrow \neg Prov(\ulcorner 0=1 \urcorner)$. $\endgroup$ – Jsevillamol Mar 6 '16 at 14:38

Your Answer

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

Browse other questions tagged or ask your own question.