= Solution
Let $T=S+\{\operatorname{Con}_S\}$ and assume $T$ is consistent. The allowed arithmetizations of the previous equivalences give
$$
S\vdash\neg B(\neg R)\leftrightarrow\operatorname{Con}_S,\qquad S\vdash\neg B(\neg G)\leftrightarrow\operatorname{Con}(T).
$$
Suppose $S\vdash R\to G$. Its contrapositive is $\neg G\to\neg R$, and the <Hilbert-Bernays-Löb derivability conditions> then give
$$
S\vdash B(\neg G)\to B(\neg R),\qquad S\vdash\neg B(\neg R)\to\neg B(\neg G).
$$
Combining with the two internal equivalences yields $S\vdash\operatorname{Con}_S\to\operatorname{Con}(T)$. Since $T$ contains $\operatorname{Con}_S$, it would prove $\operatorname{Con}(T)$, contrary to the given <Gödel second incompleteness theorem> for this consistent extension. Hence
$$
\boxed{S\nvdash R\to G\quad\text{if }S+\{\operatorname{Con}_S\}\text{ is consistent}.}
$$
Together with the preceding implication, this is the <Strict Gödel-to-Rosser implication> under the stated consistency hypothesis.
Back to article page
