= 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\leq n$, the closed bounded statement $\neg\operatorname{Prov}(\ulcorner R\urcorner,\overline k)$ is true and is provable in $S$ by <Sigma-1 completeness>. The true bounded statement $\operatorname{Prov}(\ulcorner\neg R\urcorner,\overline n)$ is also provable.
Using the given finite-numeral exhaustion below $\overline n$, these finitely many nonproof facts give
$$
S\vdash\forall y\leq\overline n\,\neg\operatorname{Prov}(\ulcorner R\urcorner,y).
$$
For arbitrary $y$, the given comparison splits into $y\leq\overline n$ or $\overline n\leq y$. In the first case the antecedent $\operatorname{Prov}(\ulcorner R\urcorner,y)$ is false. In the second case the known negative proof at code $\overline n$ supplies the required witness $z\leq y$. Hence $S$ proves
$$
\forall y\left(\operatorname{Prov}(\ulcorner R\urcorner,y)\to\exists z\leq y\,\operatorname{Prov}(\ulcorner\neg R\urcorner,z)\right).
$$
The <Rosser sentence> equivalence now gives $S\vdash R$, contradicting consistency. Thus
$$
\boxed{S\nvdash\neg R\iff S\text{ is consistent}.}
$$
Only a fixed finite list of closed bounded facts was used; no assumption that the <first-order theory> is omega-consistent is needed.
Back to article page
