= Solution
Let $C$ denote the addition-commutativity <first-order sentence> and put $d=\ulcorner\neg C\urcorner$. In the ordinary checker for PA derivations, replace the axiom test $\operatorname{Ax}_{PA}(u)$ by
$$
\operatorname{Ax}_S(u)\equiv\operatorname{Ax}_{PA}(u)\vee u=\bar d.
$$
Keep all tests for sequence formation, earlier lines, logical axiom schemes and <inference rules> unchanged. This gives a <formal proof> checker $Q_S(u,w)$ which recognizes exactly ordinary $S$-derivations. The finite syntactic modification is arithmetizable by the same bounded coding apparatus as the original checker.
For the proof-order comparison in the next part, make the choice of coding explicit. Reserve code $0$ for the one-line derivation of the newly added axiom $\neg C$, and give an ordinary derivation with code $w$ the new code $w+1$. A corresponding bounded relation is
$$
\boxed{\operatorname{Prov}_S(u,v)\equiv
(v=0\wedge u=\bar d)\vee(\exists w\le v)(v=w+1\wedge Q_S(u,w)).}
$$
Every code has a specified decoding, every genuine <formal proof> is represented, and no false <formal proof> is admitted. The reserved code duplicates one genuine derivation, which is harmless. This is one explicit arithmetized <arithmetical proof relation> obtainable from the PA checker by the requested axiom change and a simple renumbering. Stating the proof-order convention matters because a Rosser <predicate symbol> uses code order, not merely the existence of <formal proofs>.
Back to article page
