= Solution
For <Rosser separation by a bounded stage comparison>, use the <numeralwise enumeration in arithmetic> properties meant by enumeration in $S$: membership supplies some standard stage with a provable positive instance, while nonmembership makes every standard-stage instance refutable. These are stronger than merely attaching a $\Sigma_1$ syntactic label to an arbitrary formula. The finite-initial-segment <axiom> lets us combine finitely many numeralwise refutations into a bounded universal assertion.
If $n$ is provable, choose a standard stage $p$ with $S\vdash P(\overline n,\overline p)$. <consistent first-order theory>[Consistency] means $n$ is not refutable. Therefore $S\vdash\neg R(\overline n,\overline j)$ for each $j\le p$. Using the displayed finite-segment <axiom> and equality substitution, combine these proofs to get $S\vdash\forall z\le\overline p\,\neg R(\overline n,z)$. <existential quantifier introduction rule>[Existential introduction] with stage $p$ proves the separator at $n$.
If $n$ is refutable, choose a standard stage $q$ with $S\vdash R(\overline n,\overline q)$. <consistent first-order theory>[Consistency] implies that $n$ is not provable, so all standard instances of $P(\overline n,\cdot)$ are refutable. In particular their finitely many instances through $q$ give $S\vdash\forall z\le\overline q\,\neg P(\overline n,z)$. For an arbitrary proposed witness $z$, the total-comparison <axiom> gives $z\le\overline q$ or $\overline q\le z$. In the first case its $P$ conjunct fails; in the second case the known $R$ instance at $q$ contradicts its bounded no-refutation conjunct. <universal generalization rule>[Generalize] on $z$ to refute the existential separator. Hence \b[the proposed first-proof-before-refutation formula separates the two <sets>].
Back to article page
