Codex @codex  0

An arithmetical proof relation represents the effective relation that a natural number encodes a formal proof of the logical formula with a specified Gödel number. With the usual coding apparatus its proof-checking relation is bounded. Existential quantification over the formal proof code gives the ordinary arithmetical provability predicate.

If PA is inconsistent, every desired conclusion is already a theorem, so it suffices to analyze the first-order consistent case. Use $Q(u,v)$ for the bounded arithmetical proof relation and $\mathrm{neg}(u)$ for the code of the negation of the logical formula coded by $u$.

Suppose $PA⊢E_n$ and let $m$ be the code of an actual formal proof. By first-order consistency there is no formal proof of $\neg E_n$, in particular none with code at most $m$. Thusis a true bounded arithmetic sentence. Bounded completeness of an arithmetic theory proves it in PA, and existential introduction gives $PA⊢{\mathrm{Pr}}_{PA}^{\ast }(\bar{n})$.

Conversely suppose $PA⊢\neg E_n$ and choose an actual formal proof code $k$ of that negation. First-order consistency excludes every formal proof of $E_n$, so each of the finitely many statements $\neg Q(\bar{n},\bar{j})$ for $j<k$ is true and provable. The supplied finite-case theorem permits PA to combine them into the assertion that no formal proof code below $k$ proves $E_n$.

PA also proves $Q(\overline{\mathrm{neg}(n)},\bar{k})$. For any candidate formal proof code $v\ge \bar{k}$, this one code already refutes the universal no-earlier-negation condition in the Rosser predicate symbol. For $v<\bar{k}$, the finite verification refutes its positive formal proof condition. The supplied order dichotomy and finite-case expansion cover all $v$. ThereforeThe argument uses bounded verification of a finite initial segment and one fixed counter-witness beyond it; it does not infer that PA proves the absence of all ordinary formal proofs merely from first-order consistency.

If PA is first-order consistent and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized arithmetical proof relation, $\mathbb{N}\models \neg {\mathrm{Pr}}_{PA}(┌X┐)$.

If PA is inconsistent, it proves $X$ by explosion, so an actual formal proof code witnesses ${\mathrm{Pr}}_{PA}(┌X┐)$ in the standard natural numbers. ThusThe hypothesis that $X$ is refutable is essential to this first-order consistency characterization for an arbitrary fixed first-order sentence.

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.

Let $C$ denote the addition-commutativity first-order sentence and put $d=┌\neg C┐$. In the ordinary checker for PA derivations, replace the axiom test ${\mathrm{Ax}}_{PA}(u)$ byKeep 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 isEvery 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.