Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 2 / d / ii / 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. HencePA 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 ${\mathrm{Pr}}_S^{\ast }(┌C┐)$ 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.