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 Theories, models and semantic consequence, and the schema syntax is The set of first-order ZF axiom sentences. For definable classes use Relativization to sets and definable classes 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.