Formal consistency transfer from a verified reduction

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.

Finite-fragment model transfer proves relative consistency: Let T extend enough ZF to formalize set-model soundness, and let U be an explicitly countable sentence theory. Suppose that for each external finite $\mathrm{\Delta }\subseteq U$ there are a finite $\mathrm{\Gamma }$ and T proofs of existence of a suitable TM/CTM of $\mathrm{\Gamma }$ and of its conversion into a set model of $\mathrm{\Delta }$. Then external Con(T) implies Con(U). This is a metatheorem with fixed finite proof inputs, not a uniform internal all-fragment assertion.

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.