= Solution
The preceding <Gödel sentence> argument gives $S\vdash G\to\operatorname{Con}_S$. The permitted arithmetized positive half of the <Rosser sentence> argument is
$$
S\vdash\operatorname{Con}_S\to\neg BR.
$$
Pure first-order logic gives $\neg BR\to R$: if there is no proof of $R$, each antecedent in its defining universal implication is false. Therefore
$$
\boxed{S\vdash G\to\operatorname{Con}_S\to\neg BR\to R,\qquad S\vdash G\to R.}
$$
This uses the supplied internal Rosser implication, rather than replacing an external nonprovability fact by an unproved internal <first-order sentence>.
Back to article page
