= Solution
Use the <arithmetical proof relation> and coding just constructed. A <formal proof> of $C$ cannot have code $0$, since that code was reserved for $\neg C$. Every candidate code $v$ for a <formal proof> of $C$ is therefore positive. But code $0\le v$ is already a <formal proof> of $\neg C$, so the no-earlier-negation condition fails for every candidate. Hence
$$
\boxed{\mathbb N\models\neg\operatorname{Pr}_S^*(\ulcorner C\urcorner).}
$$
PA proves $C$ by <induction>, while $S$ has $\neg C$ as an added axiom. Thus $S$ is inconsistent and its ordinary <arithmetical provability predicate> is true of every <first-order sentence>, including $C$. The displayed negative Rosser assertion can nevertheless be true, because the Rosser condition compares the order of opposite <formal proofs> rather than asking for their mere existence.
There is an important coding qualification. The PDF refers to a course <formal proof> coding but does not specify its numerical ordering. The truth of this Rosser assertion for an inconsistent <first-order theory> is not coding-invariant, so <formal proof> length alone cannot establish it for an unspecified fixed coding. For example, a different legitimate numbering could reserve code $0$ for a known PA <formal proof> of $C$, code $1$ for the new axiom $\neg C$, and higher codes for all other derivations. Then code $0$ would witness $\operatorname{Pr}_S^*(\ulcorner C\urcorner)$ instead. The explicit allowed construction in part (i) supplies a convention under which the requested assertion holds; interpreting it as a claim about some externally fixed course numbering requires that numbering's corresponding <order property>.
Back to article page
