Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 1 / d

The preceding Gödel sentence argument gives $S⊢G\to {\mathrm{Con}}_S$. The permitted arithmetized positive half of the Rosser sentence argument isPure first-order logic gives $\neg BR\to R$: if there is no proof of $R$, each antecedent in its defining universal implication is false. ThereforeThis uses the supplied internal Rosser implication, rather than replacing an external nonprovability fact by an unproved internal first-order sentence.