Derivability conditions for the chosen proof predicate

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.

Primitive-recursive syntax and certified proof checking: For the fixed effective signature and sentinel encoding, term/formula recognition, free-variable and free-for tests, capture-free substitution, numeral formation, negation, and certified derivation checking are primitive recursive. Invalid inputs return zero or false.

PA verifies proof certificates for bounded arithmetic truth: For each fixed bounded arithmetic formula $\delta (\bar{x})$, PA proves that $\delta (\bar{x})$ yields a certified Q-proof of $\delta (\overline{\stackrel{ˉ}{x}})$, and that $\mathrm{\neg }\delta (\bar{x})$ yields a certified Q-proof of its negation. Substitution of numerals in this assertion is the numerical syntax operation, not literal substitution of a variable into a numeral. Consequently, for each fixed syntactic ${\mathrm{\Sigma }}_1$ sentence $\sigma$, PA proves $\sigma \to {\mathrm{Prov}}_Q(<mi\; mathvariant="normal">⌜</mi>\sigma <mi\; mathvariant="normal">⌝</mi>)$.

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.