Interpretation transports derivations and inconsistency

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.

Derived propositional, quantifier and equality rules: In the fixed calculus, Boolean identity, double negation, contraposition, conjunction introduction/elimination and explosion are derivable. Equality is symmetric and transitive and permits free-for formula substitution. Existential introduction, existential monotonicity, quantified double-negation replacement and fresh-variable quantifier renaming are derivable without completeness. Monotonicity means: from $T⊢\varphi \to \psi$ infer $T⊢\mathrm{\exists }x\varphi \to \mathrm{\exists }x\psi$. Renaming uses a variable $y$ absent from $\varphi$.

Deduction theorem for sentence assumptions: In ZF, for a sentence theory $T$, a sentence $\sigma$ and any formula $\theta$,

$T\cup \{\sigma \}⊢\theta ⟺T⊢\sigma \to \theta \mathrm{.}$

The forward transformation also works for an open discharged assumption $\sigma$ provided every variable generalized or existentially eliminated in the given derivation is absent from $\mathrm{FV}(\sigma )$; the other assumptions remain sentences.

Formal proofs from sentence theories: Fix a set signature $L$ and a set $T$ of $L$-sentences, as in def-theories-models-and-semantic-consequence. Use exactly the finite syntax of def-set-coded-terms-and-formulas: negation, conjunction and existential quantification are primitive. In particular, $\mathrm{\forall }x\varphi$ abbreviates $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\varphi$ and $\varphi \to \psi$ abbreviates $\mathrm{\neg }(\varphi \wedge \mathrm{\neg }\psi )$. Equality below between displayed formulas means equality after expansion of these abbreviations, not equivalence under first-order semantics.

The logical axioms are all instances of the following schemes. Terms are arbitrary $L$-terms and formulas may have free variables. Substitution and the free-for condition are those of def-free-variables-and-syntactic-substitution.

1. Every propositional tautology instance: substitute formulas for the letters of a finite Boolean expression whose value is true for every Boolean valuation. Expand Boolean abbreviations first. A quantified subformula may be substituted as a whole; first-order validity is not the definition of a tautology here.
2. $\mathrm{\forall }x\varphi \to \varphi [t\mathrm{/}x]$, when $t$ is free for $x$ in $\varphi$.
3. $\mathrm{\forall }x(\varphi \to \psi )\to (\varphi \to \mathrm{\forall }x\psi )$, when $x\mathrm{\notin }\mathrm{FV}(\varphi )$.
4. $\varphi [t\mathrm{/}x]\to \mathrm{\exists }x\varphi$, when $t$ is free for $x$ in $\varphi$.
5. $t=t$.
6. $s=t\to (\varphi [s\mathrm{/}x]\to \varphi [t\mathrm{/}x])$, when both $s$ and $t$ are free for $x$ in $\varphi$.

There are exactly three inference rules:

• Modus ponens: from $\varphi$ and $\varphi \to \psi$, infer $\psi$.
• Universal generalization: from $\varphi$, infer $\mathrm{\forall }x\varphi$.
• Restricted existential elimination: from $\varphi \to \psi$, infer $\mathrm{\exists }x\varphi \to \psi$, provided $x\mathrm{\notin }\mathrm{FV}(\psi )$.

A formal derivation from $T$ is a nonempty finite list of formulas, with each line annotated as an assumption in $T$, a displayed axiom instance, or an application of one of these rules to specified earlier line indices. Rule parameters and substitution data are part of the finite annotation. Write $T⊢\theta$ when such a derivation ends with $\theta$, and $⊢\theta$ when $T=\mathrm{\varnothing }$. All formulas, finite annotations and finite lists range over sets; imposing the displayed line conditions therefore specifies a set of proof codes, without a choice principle.

The premise that $T$ consists of sentences matters. For the same formal line rules applied to additional open assumptions, semantic soundness and discharge require restrictions: a generalized or existentially eliminated variable must not occur free in the undischarged assumptions on which that line depends. The sentence deduction theorem automatically satisfies this restriction; an open-assumption deduction theorem must check both rules.

Existential introduction is an axiom scheme, not a consequence silently imported from completeness. Neither replacement inside an existential quantifier nor quantified double-negation equivalence is part of the syntax convention; each must be derived from these rules when used. Soundness, deduction, fresh-constant proof transformations and completeness are separate proof obligations for this specified calculus. Domains are nonempty, as in the structure convention; no model-existence theorem is assumed here.

Finite support, weakening, and composition of derivations: In ZF, every derivation from a sentence theory uses finitely many assumptions. Weakening, concatenation and replacement of proved sentence premises by their proofs preserve derivability. The union of an inclusion-chain of consistent sentence theories in one fixed signature is consistent, including the empty chain.