Forcing transfer for finite ZFC fragments

For each target sentence retain the supplied finite forcing-verification derivation, expanding its theorem invocations into their finite proofs. Also retain the finite truth-lemma proof for each subformula of those finitely many sentences, the defining recursions on names and valuations, and the generic-enumeration construction used in F1. Only these fixed formulas are involved. In particular the existential clause needs Separation for its specific witness-forcing predicate; the atomic clauses need the specific descendant-cone recursions; a target Replacement instance needs the specific least-witness-rank Replacement from the extension proof. Each invoked Separation or Replacement schema therefore contributes a particular finite formula instance from F4.

Take the union of all ground axiom instances occurring in the retained finite derivations, also including the finitely used namehood, rank, finite-syntax and valuation absoluteness instances, Infinity and Extensionality, and the supplied proofs of the forcing-definition/parameter requirements. This is a finite list of ZFC axioms, denoted Gamma. The proof is a finite syntactic traversal: at a cited theorem expand the fixed proof actually used, and at a schema invocation retain its instantiated formula. Recursion or induction on ranks uses its finitely stated instance, not one axiom for each ordinal. Thus every retained ground argument is valid in any transitive model of Gamma. No application of the full-ZFC hypothesis of F1 is made to a mere Gamma-model.

F2 gives a ZFC proof of a countable transitive M satisfying Gamma, and the parameter/preorder construction retained in step 2.1 produces $P^M$ there. Use the external countable enumeration with least-index refinements to obtain a generic. The retained valuation and truth arguments are valid over this M by step 2.1. For each $\delta \in \mathrm{\Delta }$, its retained verification makes every condition force delta; the generic is nonempty, so the truth lemma makes delta true in M[G]. Hence this is a set model of Delta. Ambient AC enters through the countable elementary-submodel construction in F2; the generic enumeration itself uses no further choice.

The two proofs just obtained are precisely the source-existence and model-conversion data in F3. All references to Gamma and Delta were to these fixed finite lists. If Delta is empty the same elementary setup gives a nonempty set model without any target forcing assertions. No conclusion that M satisfies all ZFC follows, and no uniform arithmetic verification of all proof constructors has been asserted.