Rosser incompleteness from consistency

The syntactic diagonal lemma: For every formula $\psi (v)$ with no other free variables in an effective signature extending arithmetic, there is a sentence $\theta$ such that Q in that signature proves $\theta \leftrightarrow \psi (<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$. The construction is effective and requires neither consistency nor soundness.

The standard certified provability predicate: For a fixed effective theory T, let ${\mathrm{Prf}}_T(p,a)$ be the chosen numeralwise arithmetic representation of certified proof checking, with proof code first. Use lem-primitive-recursive-syntax-and-proof-checking and the strengthened representation constructed in thm-primitive-recursive-numeralwise-representability. Retain also the finite PA proof of equivalence to its syntactic ${\mathrm{\Sigma }}_1$ computation form. Thus “Sigma1” for this chosen predicate may mean PA-Sigma1; it does not assert Q equivalence.

Put ${\mathrm{Prov}}_T(a):=\mathrm{\exists }p{\mathrm{Prf}}_T(p,a)$ and $\mathrm{Con}(T):=\mathrm{\neg }{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)$, where $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$ is in the appropriate signature and corner brackets denote the numeral of a code. External consistency means that there is no actual finite T-refutation; the displayed Con is an arithmetic formula.

For theories extending Q, $0=1$ may replace the fixed contradiction: Q proves $0\mathrm{\ne }S0$, so from $0=S0$ explosion gives $\mathrm{\perp }$; conversely reflexivity refutes $\mathrm{\perp }$ and explosion gives $0=S0$. Appending these fixed finite proof blocks gives primitive-recursive transformations between refutation certificates, verified in PA. We use the fixed $\mathrm{\perp }$ throughout. Correctness only on standard numerals is insufficient to replace this predicate in a derivability or second-incompleteness theorem.

Q calculates numerals and finite bounded cases: Q decides every closed arithmetic atomic formula and every closed bounded formula. For every external $n$, it proves $x\le \bar{n}\to {\bigvee }_{i=0}^{n}x=\bar{i}$ and $x\le \bar{n}\vee \overline{n+1}\le x$. These are metatheoretic schemes; induction on $n$ here is not an induction axiom in Q.

Interpretation transports derivations and inconsistency: An interpretation as defined above sends every S-derivation of $\varphi$ to a T-derivation of $G_{\mathrm{F}\mathrm{V}(\varphi )}\to {\varphi }^I$. In particular a source contradiction gives a target contradiction, so external Con(T) implies Con(S). Effective certificate data gives an effective translation. A formal Con implication additionally follows in any base B that verifies a total map from S-contradiction certificates to T-contradiction certificates.