Explicit definitions are conservative

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. Effective certificate data provides the required target certificates effectively. Formalized data additionally provides a base-verifiable total primitive-recursive map on proof codes; effectiveness alone does not assert that stronger property.

Use def-set-coded-formal-derivation for the calculus and lem-primitive-recursive-syntax-and-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.

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.

Consistency and syntactic completeness: Fix a set signature $L$ and sentence theory $T$, with derivability as in def-set-coded-formal-derivation. Fix the sentence $\mathrm{\perp }:=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$.

The theory $T$ is consistent when $T⊬\mathrm{\perp }$. It is syntactically complete when for every $L$-sentence $\sigma$, $T⊢\sigma$ or $T⊢\mathrm{\neg }\sigma$. Deductive closure of a sentence theory means closure under its sentence consequences; it does not include open formulas as members.

If $L\subseteq L^{\mathrm{\prime }}$ and $T\subseteq U$ are sentence theories in their respective signatures, $U$ is conservative over $T$ when every $L$-sentence provable from $U$ is provable from $T$. The reverse preservation follows by retaining the same derivation in the expansion. These are syntactic definitions, including when $T$ is empty; no model existence is asserted.