= Strict Gödel-to-Rosser implication
{c}
{title2=$T\vdash G\to R,\quad T\nvdash R\to G$}
For the standard <Gödel sentence> and <Rosser sentence>, the formalized Rosser unprovability theorem and $G\leftrightarrow\operatorname{Con}(T)$ yield $T\vdash G\to R$. If $T+\operatorname{Con}(T)$ is consistent, the converse is unprovable under the usual formalized incompleteness hypotheses. A proof of $R\to G$ would give $\Box\neg G\to\Box\neg R$. Formalized negative unprovability identifies $\neg\Box\neg R$ with $\operatorname{Con}(T)$ and $\neg\Box\neg G$ with $\operatorname{Con}(T+\operatorname{Con}(T))$. The strengthened theory would then prove its own consistency, contradicting the <Gödel second incompleteness theorem>. The consistency assumption belongs to this strictness conclusion.
Back to article page
