Fixed finite-fragment verification for the basic Cohen symmetric model

Fix the actual formulas of $\mathrm{\Delta }$ and their subformulas. Use $P=\mathrm{Add}(\omega ,\omega )$, the finite permutations of the first coordinate, and the finite-support normal filter of F2. For each of these fixed formulas the recursions in F1 give ordinary set-theoretic proofs of definability, strengthening, truth and equivariance. Name-rank induction is an object-level transfinite induction in those proofs, not a numerical search over names.

Here is the almost-universality argument used by the HS-model construction. In an ambient generic extension let $x={\dot{x}}_{G_0}\subseteq N={\mathrm{H}\mathrm{S}}^{G_0}$. In the ground model assign to each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$ the least rank of an HS name $\sigma$ such that $p⊩\tau =\sigma$, or zero if none exists. Ground Replacement bounds these ranks strictly by an ordinal $\gamma$. For every $u\in x$, a subname $\tau$ evaluating to $u$ and the truth lemma give such an equality at some condition in $G_0$. Thus $u$ has an HS name of rank below $\gamma$. The ground set of all HS names below that rank is invariant under every automorphism; placing all these names at the top condition gives an HS name for an $N$-set containing $x$. This proves relative almost universality. For a bounded matrix, rank-bounded HS subnames satisfying its ordinary forcing clause form the exact cut of an $N$-set. Bounded absoluteness identifies that clause with truth in $N$; the parameter stabilizers and equivariance make the cut HS.

For completeness, the failure-of-Choice argument in F3 has two supported-map branches. Distinct coordinate names ${\dot{a}}_n$ are forced unequal by assigning opposite values at a fresh bit. If an HS name $\dot{f}$ were an injection from $\omega$ to $A$, take a finite support $E$ for it and a condition $p$ forcing this, enlarging $E$ to include the finite first-coordinate support of $p$. If no strengthening decides any value outside $\{a_n:n\in E\}$, density of value decisions confines its range to that finite set, contradicting injectivity. Otherwise choose a strengthening $q$ deciding $f(i)=a_n$ with $n\mathrm{\notin }E$, and $m$ outside $E\cup \mathrm{supp}(q)\cup \{n\}$. The transposition of $n,m$ fixes $p,\dot{f}$; $q$ and its image agree off the swapped coordinates and have disjoint domains on them, so their union forces two distinct values for $f(i)$. Thus $A$ is infinite and has no injection from $\omega$; a well-order of $A$ would give one by successively choosing its least remaining element. Hence $N\models \mathrm{\neg }\mathrm{A}\mathrm{C}$. These are set-theoretic arguments within the chosen proof, not operations performed by a numerical proof constructor.

Pairing HS names directly gives unordered and Kuratowski pairs in $N$. Each of Jech's eight operations (pair, difference, product, domain, restricted membership and three triple-coordinate permutations) produces an ambient set of $N$-elements. Step 2.1 puts it inside an $N$-set; its bounded defining formula cuts out the operation's exact value. To obtain general Separation, induct externally on the fixed formula's complexity. Atomic relations follow from these operations, negation from relative difference, and conjunction from intersection. For an existential subformula $\mathrm{\exists }v\psi (v,\bar{u})$, ambient Separation and Replacement collect, for every parameter tuple, the set of all $N$-witnesses of least rank, or the empty set. Starting from the argument set and the parameters, close under these witness sets for $\omega$ stages. This yields an ambient set containing witnesses for every relevant tuple. Almost universality puts it inside a set $Y\in N$; the induction hypothesis constructs the relation for $\psi$ on $Y$, and projection followed by restriction gives the existential relation on the original argument set. This is the cited Jech all-witness and transitive-class argument, with no choice of a distinguished witness. For a fixed functional Replacement matrix, ambient Replacement bounds its unique $N$-values on the domain, almost universality supplies an internal container, and the just-proved internal Separation cuts out the image. Only bounded matrices used the direct subname cut of step 2.1.

For the externally fixed $\mathrm{\Delta }$, the finitely many formula inductions just described yield finite ZFC derivations of its HS-model axioms and step 2.2. Collect their actual Separation, Replacement, recursion and forcing instances into a finite ground support $\mathrm{\Gamma }$, enlarging it for the names, valuations and generic construction. The preceding argument applied to a countable transitive $\mathrm{\Gamma }$-model proves that its symmetric extension satisfies each member of $\mathrm{\Delta }$; full ZFC in that ground model is not used. F4 proves in ambient ZFC that such a countable transitive source model exists. Enumerate its dense subsets, construct a generic filter, and take the set of valuations of its HS names. This gives a set model of the particular $\mathrm{\Delta }$. Ambient AC has precisely the source-model and generic-construction role of F5.

The ambient ZFC derivation in step 4.1 is finite, so it too uses only finitely many axioms and schema instances. The choice of this proof is made separately for the given external $\mathrm{\Delta }$. Neither a single internally quantified model-existence assertion nor a PA-total selector of these proofs follows from this argument. This proves exactly the fixed-fragment assertion.