Finite-fragment model transfer proves relative consistency

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.

Transitive models and finite-fragment transfer data: For a sentence theory $\mathrm{\Gamma }$ in the membership language, $\mathrm{TM}(\mathrm{\Gamma })$ means that some nonempty transitive set M, with actual restricted membership, satisfies every sentence of $\mathrm{\Gamma }$. Transitive means $\mathrm{\forall }x\in M\mathrm{\forall }y\in x(y\in M)$. The assertion $\mathrm{CTM}(\mathrm{\Gamma })$ additionally requires an external injection $M\to \omega$.

A finite-fragment transfer specifies, for each external finite target fragment $\mathrm{\Delta }$, a finite source fragment $\mathrm{\Gamma }$ and a theorem converting every suitable TM or CTM of $\mathrm{\Gamma }$ into a set model of $\mathrm{\Delta }$. Suitability includes every auxiliary axiom, parameter restriction and metatheory needed by the conversion. Inclusion $\mathrm{\Gamma }\subseteq \mathrm{Z}\mathrm{F}$ is syntactic, using the fixed axiom presentation.

The model convention is def-theories-models-and-semantic-consequence, and the schema syntax is def-coded-first-order-zf-theory. For definable classes use def-relativization-to-a-definable-class separately for each fixed formula; do not quantify over a universe truth predicate. Countability in this definition is outside the proposed model. A model or CTM of the full source theory is not part of finite-fragment data unless explicitly assumed.

Models and consistency for countable theories: In external ZF, an explicitly countable sentence theory is consistent iff it has a nonempty set model, and iff it has a model with carrier injecting into $\omega$. For an effective presentation, external consistency agrees with the truth of its certified Con formula in standard arithmetic. No transitivity or external well-foundedness of a model follows.