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

If $S$ is inconsistent, it proves $\neg R$ by explosion. Conversely, suppose $S$ is consistent and, towards a contradiction, has a proof of $\neg R$ with standard code $n$. Consistency excludes any proof of $R$. In particular, for each $k\le n$, the closed bounded statement $\neg \mathrm{Prov}(┌R┐,\overline{k})$ is true and is provable in $S$ by Sigma-1 completeness. The true bounded statement $\mathrm{Prov}(┌\neg R┐,\overline{n})$ is also provable.

Using the given finite-numeral exhaustion below $\overline{n}$, these finitely many nonproof facts giveFor arbitrary $y$, the given comparison splits into $y\le \overline{n}$ or $\overline{n}\le y$. In the first case the antecedent $\mathrm{Prov}(┌R┐,y)$ is false. In the second case the known negative proof at code $\overline{n}$ supplies the required witness $z\le y$. Hence $S$ provesThe Rosser sentence equivalence now gives $S⊢R$, contradicting consistency. ThusOnly a fixed finite list of closed bounded facts was used; no assumption that the first-order theory is omega-consistent is needed.