About the disprovability of the Gödel Sentence

70 Views Asked by At

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?