= Solution
\b[The external <necessitation rule> assertion is valid.] Suppose $PA\vdash X$ and fix a proof code $m$. If $PA$ is inconsistent the assertion follows by explosion. Otherwise there is no actual proof of $\neg X$. Each of the finitely many bounded checks up to $m$ is therefore a true bounded <arithmetic> fact and is provable. Together with the positive proof check at $m$ this gives
$$
\boxed{PA\vdash X\ \Longrightarrow\ PA\vdash R(\ulcorner X\urcorner).}
$$
\b[The requested internal modus-ponens assertion needs an additional coding property.] Combining a proof of $X$ and a proof of $X\to Y$ produces a proof of $Y$, but its code can exceed both original codes. The two Rosser hypotheses exclude proofs of $\neg X$ and $\neg(X\to Y)$ only up to their respective witness bounds. They provide no bound excluding proofs of $\neg Y$ below the new proof code. Ordinary internal <modus ponens rule> for the unbounded provability predicate does not fill this gap.
Consequently the premises printed here do not, just by themselves, justify
$$
R(\ulcorner X\to Y\urcorner)\to(R(\ulcorner X\urcorner)\to R(\ulcorner Y\urcorner)).
$$
This property varies with the <Rosser proof-order dependence>: some specially chosen proof predicates satisfy it, while general Rosser proof predicates need not. https://sartemov.ws.gc.cuny.edu/files/2012/10/Artemov-Beklemishev.-Provability-logic.pdf[Provability Logic, printed page 87: dependence of Rosser <modus ponens rule> on proof numbering]{ref}.
The reference to a proof predicate “as given in the course” would need an explicit additional proof-order lemma to establish this part for that particular coding. Standard correctness on numeral instances and the ordinary <Hilbert-Bernays-Löb derivability conditions> alone are insufficient. The next solution gives the intended argument with the missing condition stated explicitly.
Back to article page
