= Solution
Let $\bot$ abbreviate the fixed false <arithmetic> equality, and fix an actual proof of $\neg\bot$ with code $m$. For a proposed proof code $y\geq m$, that known proof of the <negation> already violates the bounded negative-proof test in $R(\ulcorner\bot\urcorner)$.
For the finitely many codes $y<m$, either one is an actual proof of $\bot$, in which case <Peano arithmetic> is inconsistent and proves the requested conclusion by explosion, or none is. In the latter case the finitely many true bounded facts $\neg\operatorname{Prf}(\ulcorner\bot\urcorner,\overline y)$ are all provable by bounded completeness. Their conjunction excludes every code below $m$. The positive bounded fact that $m$ proves $\neg\bot$ is likewise provable. Splitting $y<m$ and $y\geq m$ inside <arithmetic> now gives
$$
\boxed{PA\vdash\neg R(\ulcorner\bot\urcorner).}
$$
Thus the consistency statement for this <Rosser provability predicate> is provable. The argument uses only a fixed finite initial segment of proof codes; it does not prove the usual unbounded consistency statement.
Back to article page
