Interpretations with proof-translation data

An interpretation of a sentence theory S in T specifies formulas D(x) and E(x,y), invariant relation formulas, and functional graph formulas. T proves D nonempty, E an equivalence on D, invariance under E of all relations and graphs, and totality and uniqueness modulo E of each function graph on domain-valued inputs. Fixed parameters are target constants. No other free variables occur in the interpretation data.

Define a domain-valued term graph by $V_x(z):=D(z)\wedge E(x,z)$ and $V_{f(\bar{t})}(z):=D(z)\wedge \mathrm{\exists }\bar{u}({\bigwedge }_i{V}_{t_i}(u_i)\wedge F_f(\bar{u},z))$; the nullary case uses the constant graph. Atomic relations and equality quantify term values and then apply the interpreted relation or E. Translation commutes with negation/conjunction and replaces $\mathrm{\exists }x\varphi$ by $\mathrm{\exists }x(D(x)\wedge {\varphi }^I)$, always using fresh bound variables. T must prove every translated source axiom.

For a source formula $\varphi$ put $G_{\mathrm{F}\mathrm{V}(\varphi )}={\bigwedge }_{v\in \mathrm{F}\mathrm{V}(\varphi )}D(v)$. Its guarded proof translation is $G_{\mathrm{F}\mathrm{V}(\varphi )}\to {\varphi }^I$. For sentences the empty guard is a fixed tautology.

For the following effective and formalized layers, fix separately for S and T the effectively presented countable finite-arity signatures, primitive-recursive symbol-kind/arity tests, primitive-recursive axiom-certificate predicates, and sentinel numerical encoding of Effective theories and certified numerical proof codes. All syntax, annotations and certified derivations use those presentations. Write ${\mathrm{Prf}}_S(p,a)$ and ${\mathrm{Prf}}_T(q,b)$ for the corresponding certified proof-checking predicates, with proof code first; malformed inputs are rejected. The abstract interpretation above does not require effective signatures.

Effective certificate data supplies the interpretation formulas uniformly effectively from source symbol codes, target certificates for their interpretation obligations uniformly effectively, and a target translation certificate effectively from each certified source axiom. Fix increasing variable-index order for guards, a fixed closed tautology for the empty guard, and a deterministic fresh-variable convention. Thus the guarded formula translation has a definite numerical code.

Formalized proof-translation data additionally specifies an arithmetic base $B$, total primitive-recursive functions $t,r:\mathbb{N}\to \mathbb{N}$, and chosen arithmetic representations of these functions and the two certified proof predicates. On source formula codes, $t$ codes the guarded translation; on nonformula inputs set $t=0$. The representations must describe these numerical functions and predicates, and $B$ must prove totality and single-valuedness of the function graphs and the uniform correctness assertion

$B⊢\mathrm{\forall }p\mathrm{\forall }a({\mathrm{Prf}}_S(p,a)\to {\mathrm{Prf}}_T(r(p),t(a)))\mathrm{.}$

Function notation here abbreviates the chosen graph formulas; with graphs $R(p,q)$ for r and $H(a,b)$ for t, the assertion is $B⊢\mathrm{\forall }p\mathrm{\forall }a\mathrm{\forall }q\mathrm{\forall }b(({\mathrm{Prf}}_S(p,a)\wedge R(p,q)\wedge H(a,b))\to {\mathrm{Prf}}_T(q,b))$. The value of r on invalid proof inputs is immaterial, but r is total on all natural numbers. These verifications are required data, not consequences of correctness on standard numerals alone.

For contradiction transfer use the fixed sentence $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$ in each signature, with numerical codes $b_S,b_T$. Formalized data also includes the fixed target proof block refuting the translated source contradiction, its primitive-recursive appending/explosion operation c, chosen arithmetic graph representation, and B proofs of its totality, single-valuedness and

$B⊢\mathrm{\forall }q({\mathrm{Prf}}_T(q,t(\overline{b_S}))\to {\mathrm{Prf}}_T(c(q),\overline{b_T}))\mathrm{.}$

Here overlines denote numerals, and c is interpreted by its graph as above. Composing c with r gives the B-verified map from S-contradiction certificates to T-contradiction certificates. Effectiveness alone supplies neither primitive recursiveness of all these data nor their verification in B; mere totality of a map does not satisfy the correctness requirements.

Use Formal proofs from sentence theories for the calculus and Primitive-recursive syntax and certified proof checking for the finite numerical operations. Logical theorem preservation is a conclusion of the next lemma, not an interpretation axiom. No quotient representatives or choice function are specified.