The Forcing Theorem and Formal Consistency Transfer

For input names $\sigma ,\tau$ form a set C by starting with those names, adjoining all first coordinates of their entries, iterating this operation through omega, and taking the union. Replacement and Union give a set closed under subnames. On $C\times C$ order pairs by the lexicographic order of $(\max ({\mathrm{rk}}_P(u),{\mathrm{rk}}_P(v)),\min ({\mathrm{rk}}_P(u),{\mathrm{rk}}_P(v)))$. This relation is well-founded: in a nonempty subset take the least first rank, then the least second rank. It is setlike since the domain is a set. Lowering one coordinate strictly lowers its sorted rank pair; swapping coordinates leaves the complexity unchanged.

At $(u,v)$ define a subset $E(u,v)$ of P by the equality clause of F1 with both subset clauses expanded. Its only equality calls involve a subname of u and a subname of v, in either order; these have strictly smaller complexity. Thus a supplied predecessor function determines membership of every p in $E(u,v)$ by quantifiers over sets P, u and v. Separation forms the unique subset. F2 supplies all these subsets on $C\times C$. Then the subset and membership relations are uniquely specified by F1 using these E-values; no recursive call to the same equality pair is needed.

For any two descendant-closed cones containing an input pair, their intersection remains descendant-closed. Induction on sorted rank pairs shows the E-values agree there, since their defining clauses use identical smaller pairs. The derived subset and membership values agree as well. Accordingly the formula asserting that the canonical cone recursion has p in its designated value defines the atomic relation independently of the cone. Every putative solution restricts to this recursion, so uniqueness follows.

Inside transitive M the canonical cone formed in step 1.1 is the same set: first-coordinate extraction, each finite iteration, and its omega-union agree, and M has actual omega. F3 identifies its ranks. Induct on the common rank pairs. Every condition, coefficient and subname quantified over in the expanded equality clauses is in the identical set on both sides; all predecessor E-values agree by induction. Equality therefore agrees, and the derived subset and membership clauses agree for the same reason. All recursions and restricted forcing sets exist inside M by its ZF axioms. This proves atomic absoluteness without comparing power sets of name levels, using AC, or asserting that a class of all names is a set.

Every atomic forcing clause persists to stronger conditions: in the subset clause the tested common extensions below q are a subset of those below p, and equality is the conjunction of two such requirements; membership restricts its tested extensions in the same way. For density closure of subset, given $⟨u,s⟩\in \sigma$ and $q\le p,s$, choose $a\le q$ forcing the subset, then apply its clause with that entry and common extension a. For equality, take a densely available condition forcing equality and perform this argument separately for each subset direction. For membership, given $q\le p$, first refine to a condition forcing membership and then refine once more to its equality/coefficient witness. These arguments prove atomic persistence and density closure.

If D is dense below p, the set $D^{\mathrm{\prime }}=\{q\in D:q\le p\}\cup \{q:q\perp p\}$ is dense in P. Indeed a condition compatible with p has a common extension, which can be refined into D; an incompatible condition already belongs to the second set. For $D,p\in M$, Separation makes $D^{\mathrm{\prime }}\in M$. A generic G containing p meets $D^{\mathrm{\prime }}$, and directedness prevents it from meeting its incompatible part. Thus it meets $D\cap \{q:q\le p\}$.

Induct on formula complexity for persistence and density closure. For conjunction, persistence holds for each conjunct by induction; if conjunction is forced densely, each conjunct is forced densely and hence at p by induction. For negation, no extension of p forcing $\psi$ implies the same at every stronger condition. If negation is forced densely below p, a hypothetical $q\le p$ forcing $\psi$ has an extension r forcing its negation; persistence of $\psi$ makes r force $\psi$, contradicting the negation clause at r itself.

For an existential, let $W=\{r:\mathrm{\exists }\sigma (r⊩\psi (\sigma ,\vec{\tau }))\}$. Forcing the existential means W is dense below p. It is then dense below every stronger condition, proving persistence. If conditions below p forcing the existential are dense below p, any $q\le p$ has a refinement a below which W is dense, and hence a further refinement in W. Thus W is dense below p, proving density closure. Together with step 2.1, this completes the induction.

Given any p, either some $q\le p$ forces $\phi$, or no such q exists and p forces $\mathrm{\neg }\phi$ by definition. This proves external decision density. When the parameters belong to M, Separation inside M instead forms the set decided by ${⊩}^M$; F1 does not identify that set with the external one for quantified formulas. No condition forces both $\phi$ and $\mathrm{\neg }\phi$, because p is one of its own extensions. All refinements used above are finitely many existential instantiations; no choice principle is used.

First induct on the sorted pair of name ranks to prove the equivalence for equality. Suppose $p\in G$ forces $\sigma \subseteq \tau$, and $u_G\in {\sigma }_G$ comes from $⟨u,s⟩\in \sigma$ with $s\in G$. Directedness gives $q\in G$ with $q\le p,s$. The set of $r\le q$ admitting $⟨v,t⟩\in \tau$ with $r\le t$ and $r⊩u=v$ is in M by atomic definability and is dense below q by the subset clause. F1 gives such r in G; then t is in G, and equality induction on the two proper subnames gives $u_G=v_G\in {\tau }_G$. Applying this to both subset clauses proves the forward semantic implication from forced equality.

For the converse define $K_{\sigma ,\tau }$ to consist of r for which some $⟨u,s⟩\in \sigma$ satisfies $r\le s$ and there are no $a\le r$ and $⟨v,t⟩\in \tau$ with $a\le t$ and $a⊩u=v$. The union of $K_{\sigma ,\tau }$, $K_{\tau ,\sigma }$ and the equality-forcing conditions is dense. Indeed, if p fails equality, one subset clause fails; its negation supplies an entry and $q\le p,s$ with no such further witness, putting q in the corresponding K. All these sets belong to M by Separation and atomic definability.

If ${\sigma }_G={\tau }_G$, neither K meets G. For otherwise its witness u satisfies $u_G\in {\sigma }_G={\tau }_G$, so some $⟨v,t⟩\in \tau$ has $t\in G$ and $u_G=v_G$. Equality induction gives $b\in G$ forcing $u=v$. A common refinement in G of r,t,b still forces that equality by F1, contradicting r's K-condition. The reverse K is excluded identically with the names exchanged. Genericity applied to the dense union in step 1.2 therefore gives a condition in G forcing equality. The induction is legitimate in both equality directions because both names in each equality appeal are proper subnames. This establishes equality in both directions, including the empty-name base.

If $p\in G$ forces $\sigma \in \tau$, its dense set of coefficient/equality witnesses is in M; F1 gives $r\in G$ and $⟨v,t⟩\in \tau$ with $r\le t$ and $r⊩\sigma =v$. Equality gives ${\sigma }_G=v_G\in {\tau }_G$. Conversely if ${\sigma }_G\in {\tau }_G$, choose such an entry with $t\in G$ and ${\sigma }_G=v_G$ by F2. Equality gives $b\in G$ forcing $\sigma =v$. A common refinement p of b and t lies in G; every extension of p is a membership witness by persistence. Thus p forces membership.

Induct on formula complexity. Conjunction forced by a member of G makes both conjuncts true by induction. Conversely, truth of both conjuncts gives two forcing conditions in G; their common refinement forces both. If $p\in G$ forces $\mathrm{\neg }\psi$, truth of $\psi$ would give $b\in G$ forcing $\psi$ by induction, and a common refinement would contradict the negation clause. Conversely, if $\psi$ is false in M[G], G meets the ground decision set for $\psi$; its chosen condition cannot force $\psi$ by induction, hence forces $\mathrm{\neg }\psi$.

If $p\in G$ forces $\mathrm{\exists }x\psi (x,\vec{\tau })$, its ground set of witness-forcing conditions is dense below p. F1 supplies r in G and a name $\sigma \in M$ with $r⊩\psi (\sigma ,\vec{\tau })$. Induction gives a witness ${\sigma }_G$ in M[G]. Conversely a true existential has a witness $x={\sigma }_G$ by F2; induction gives r in G forcing its matrix. Every stronger condition forces the same matrix by persistence, so r forces the existential by F4. Together with step 4.1 this finishes the formula induction and both directions of the assertion. Only finitely many refinements and existential witnesses were used at each argument, so no AC enters.

Atomic relations are definable by F1. At conjunction and negation insert the already obtained subformula predicates into the clauses in F2; at an existential quantify over the definable class of M-names and over the set P. This gives a fixed first-order predicate for each fixed formula. Every parameter is P, its order, or one of the name arguments. F4 then supplies the truth lemma for this very internally defined predicate.

If $p{⊩}^M\phi$ and G is M-generic containing p, the right-to-left direction of F4 makes $\phi$ true in M[G]. This implication needs no assumption that any generic exists.

Suppose p does not force $\phi$. By density closure F3 the conditions forcing $\phi$ cannot be dense below p. Hence some $q\le p$ has no stronger condition forcing $\phi$, which says $q{⊩}^M\mathrm{\neg }\phi$ by F2. The extra generic-existence hypothesis supplies an M-generic G containing q; upward closure puts p in G. F4 makes $\mathrm{\neg }\phi$ true there. Thus the asserted truth in every generic through p fails.

Steps 2.1 and 2.2 give both directions of the display. The argument selected only one generic under the stated existence hypothesis; it did not select generics simultaneously or infer their existence from definability. Formula construction used an external finite induction, so no uniform truth predicate for the universe or AC was assumed.

F2 and F4 give transitivity and the stated containments. Empty Set and Infinity hold since the actual empty set and omega belong to M and hence to M[G]. Extensionality holds in a transitive domain: every member of either set is in that domain. For Foundation, any nonempty $x\in M[G]$ has an ambient membership-minimal $y\in x$; transitivity puts y in M[G], and $y\cap x=\mathrm{\varnothing }$ remains true there. F3 constructs an unordered pair name $S(\{\sigma ,\tau \})$, giving Pairing.

For Separation, let $a={\sigma }_G$ and let $\vec{b}={\vec{\tau }}_G$ be the parameters of a fixed formula $\phi$. Put $T=\mathrm{dom}(\sigma )$ and form in M the name $\eta =\{⟨\rho ,p⟩\in T\times P:p{⊩}^M(\rho \in \sigma \wedge \phi (\rho ,\vec{\tau }))\}$. It is a set by internal Separation using definability in F1. A member of its value satisfies the displayed conjunction by the truth lemma. Conversely any $x\in a$ has a representative $\rho \in T$; if $\phi (x,\vec{b})$ holds, the truth lemma supplies a p in G for that conjunction. Hence ${\eta }_G=\{x\in a:M[G]\models \phi (x,\vec{b})\}$, proving every Separation instance.

For Union, for $a={\sigma }_G$ form $T={\bigcup }_{\rho \in \mathrm{dom}(\sigma )}\mathrm{dom}(\rho )$ in M. F3 gives $u=S(T{)}_G\in M[G]$. If $z\in y\in a$, valuation first gives a subname $\rho$ of sigma for y and then a subname of rho for z, so $z\in u$. Separation from step 1.2, with predicate $\mathrm{\exists }y\in a(z\in y)$, cuts out exactly $\bigcup a$ from u.

For Replacement, suppose a fixed formula $\phi (x,y,\vec{b})$ defines exactly one y for every $x\in a={\sigma }_G$. For each $(\rho ,p)\in \mathrm{dom}(\sigma )\times P$, define in M $\gamma (\rho ,p)$ to be the least ordinal $\gamma$ for which some name $\tau \in V_{\gamma }^M$ has $p{⊩}^M\phi (\rho ,\tau ,\vec{\tau })$; put it equal to zero if there is no such name. This is a definable ordinal function, so internal Replacement gives an ordinal $\delta$ strictly above every such $\gamma$. Internal Separation forms the set U of names in $V_{\delta }^M$. F3 gives $u=S(U{)}_G\in M[G]$. Given $x\in a$ and its unique y, choose a representing subname rho for x and any name for y. F1 gives p in G forcing the matrix. By the definition of the least rank, there is a witnessing name in U forced by that same p; F1 and uniqueness identify its value with y. Thus u contains every output. Separation using $\mathrm{\exists }x\in a\phi (x,y,\vec{b})$ gives the exact range. Only least ranks were collected, never a chosen name from each witness class.

For Power Set, put $T=\mathrm{dom}(\sigma )$ for $a={\sigma }_G$ and form $Q=\mathcal{P}(T\times P{)}^M$ in M. Every element of Q is a name, so $u=S(Q{)}_G$ belongs to M[G]. If $y\in M[G]$ and $y\subseteq a$, choose a name eta for y and form $\theta =\{⟨\rho ,p⟩\in T\times P:p{⊩}^M\rho \in \eta \}\in Q$. By F1 its value is contained in y. Conversely a member x of y is in a and has a representative rho in T; the truth lemma supplies p in G forcing its membership in eta, so x is in ${\theta }_G$. Thus $y={\theta }_G\in u$. Separation of u by $y\subseteq a$ now gives exactly the internal power set of a. This uses only M's subsets of $T\times P$, not its external power set.

The preceding steps give every axiom of ZF: the elementary axioms, Union, each Separation and Replacement instance, and Power Set. The target instances were derived from fixed internal forcing predicates; no truth predicate for M[G] was assumed inside M. This establishes the entire ZF branch.

Assume now, only for this branch, that M satisfies AC. Given $a={\sigma }_G$, F5–F7 inside M provide a bijection $h:\xi \to \mathrm{dom}(\sigma )$ for some ordinal xi; this is the exact use of ground-model AC. F3 constructs in M a graph name whose value in M[G] is the function $f(i)=h(i{)}_G$ on xi. Its range covers a. In the ZF model from step 3.1, for each $x\in a$ the nonempty fibre $\{i<\xi :f(i)=x\}$ has a least ordinal. Least fibres inject a into xi and well-order a. For a family of nonempty sets in M[G], apply this to its union and take the least member of each family member; target Replacement yields the choice function. Empty a and the empty family need only the empty maps. Thus M[G] satisfies AC, with no ambient AC assumption.

If $\gamma \in \mathrm{Ord}\cap M$, F3 gives a ground name whose value is gamma, so $\gamma \in M[G]$. Its being an actual ordinal is unchanged. Thus $\mathrm{Ord}\cap M\subseteq \mathrm{Ord}\cap M[G]$.

If $\gamma \in \mathrm{Ord}\cap M[G]$, write $\gamma ={\tau }_G$ for a name $\tau \in M$. By F4, $\beta ={\mathrm{rk}}_P(\tau )$ is an actual ordinal in M. Since an ordinal has membership rank equal to itself, F2 gives $\gamma \le \beta$. If $\gamma =\beta$ it is in M directly; if $\gamma <\beta$, transitivity of M puts $\gamma \in M$. This includes gamma zero.

The inclusions in steps 1.1 and 1.2 prove the equality. The upper-bound argument compares actual ordinal sets and uses no enumeration, cardinal arithmetic, cofinal map or AC; it therefore makes no claim that the extension has the same cardinals or cofinalities.

We first record a refinement calculation. If $q\le e(p_1),\dots ,e(p_n)$, choose $a$ with $e(a)\le q$. Compatibility reflection makes $a$ compatible with $p_1$, so refine $a$ below $p_1$. Its image is still below $q$ and hence compatible with $e(p_2)$; reflect compatibility again and continue. After finitely many steps obtain $r\le p_1,\dots ,p_n$ with $e(r)\le q$. For $n=0$ this is image density. Consequently the image of $\{r:r\le p\}$ is dense below $e(p)$. Also, if $e(a)\le e(b)$, every extension of $a$ is compatible with $b$, and conditions below $b$ are dense below $a$. Only finitely many existential instantiations are involved.

Apply F5 on the subname relation F4. The rule for $T$ takes a set image of the entries. The rule for $R$ takes a subset of the product of the entry set with $P$, then its set image. Both outputs are names by F4. These operations are definable and use no chosen inverse of $e$. Their recursion exists internally in any ground ZF model. For a transitive ground containing the data, induction on subnames identifies its output with the external translation: each entry and each tested coefficient ranges over the same ground sets, and the already translated subnames agree. The displayed definition shows that $TR(\tau )$ has entries $⟨TR(v),e(p)⟩$ for every entry $⟨v,q⟩\in \tau$ and every $p$ with $e(p)\le q$; this is a coefficient refinement, not literal equality with $\tau$.

Here are the equality rules needed below, proved directly from F1. Induction on name rank gives $p⊩a=a$ for all $p$: for an entry of $a$ and a tested common extension use that same entry and the induction hypothesis for its subname. Symmetry is built into the two subset tests. For transitivity induct on the decreasing lexicographic order of the three name ranks sorted in nonincreasing order. Suppose $p⊩a=b$ and $p⊩b=c$. For an entry $⟨u,s⟩\in a$ and $q\le p,s$, the first equality refines $q$ to $r$ below the coefficient of an entry $⟨v,t⟩\in b$, forcing $u=v$. The second refines $r$ to $w$ below the coefficient of $⟨z,h⟩\in c$, forcing $v=z$. Persistence and transitivity at the smaller triple $(u,v,z)$ give $w⊩u=z$. This verifies $a\subseteq c$; exchanging $a,c$ and using symmetry verifies $c\subseteq a$. The triple strictly decreases because all three entries are proper subnames.

If $p⊩a=b$ and $p⊩a\in c$, any extension of $p$ refines to an entry of $c$ with $a$ forced equal to its subname. Symmetry and transitivity from the preceding equality rules replace $a$ by $b$, proving $p⊩b\in c$. If $p⊩c=d$ and $p⊩a\in c$, first obtain an entry $⟨u,s⟩\in c$ with $a=u$ forced and coefficient above the current condition. Apply the $c\subseteq d$ test to obtain an entry of $d$ with subname forced equal to $u$; transitivity gives the required membership witness in $d$. Density closure proves both membership substitution assertions at $p$. Transitivity itself gives substitution in equality, in either argument.

We prove $p{⊩}_{P}a=b$ iff $e(p){⊩}_{Q}T(a)=T(b)$ by induction on the sorted pair of source name ranks. For the forward direction, an entry $⟨T(u),e(s)⟩$ of $T(a)$ comes from an entry $⟨u,s⟩$ of $a$. Given $q\le e(p),e(s)$, the refinement calculation supplies $r\le p,s$ with $e(r)\le q$. The source subset test refines $r$ to a coefficient of an entry $⟨v,t⟩\in b$ and forces $u=v$. The smaller-pair induction transports this equality, giving the target witness. Apply this reasoning to both subset directions. For the reverse direction, given $⟨u,s⟩\in a$ and $r\le p,s$, apply the target test below $e(r)$ to find $q\le e(r),e(t)$ and an entry $⟨v,t⟩\in b$ with $q{⊩}_{Q}T(u)=T(v)$. Refine to $w\le r,t$ with $e(w)\le q$; persistence and the smaller-pair induction give $w{⊩}_{P}u=v$. Again apply this to both subset directions. Duplicate image entries require only one witnessing source entry at a time.

For each $Q$-name $a$, every $Q$-condition forces $TR(a)=a$, by induction on its name rank. For an entry $⟨TR(u),e(s)⟩$ of $TR(a)$ coming from $⟨u,t⟩\in a$ with $e(s)\le t$, every tested condition below $e(s)$ is already below $t$ and forces $TR(u)=u$ by induction. This verifies $TR(a)\subseteq a$. For the other direction, given $⟨u,t⟩\in a$ and a condition $q$ below its coefficient and the condition being tested, image density gives $e(s)\le q$. The entry $⟨TR(u),e(s)⟩$ exists in $TR(a)$ and induction and symmetry give the required equality. These are exactly the two subset clauses. In particular, this proves forced equality for the coefficient closure, rather than assuming that closure leaves a name literally unchanged.

Let $G$ be $P$-generic and put $H=\{q:\mathrm{\exists }p\in Ge(p)\le q\}$. It is nonempty and upward closed, and directedness follows by taking a common refinement in $G$. For a ground dense set $D\subseteq Q$, the set $E=\{p:e(p)\in D\}$ need not be dense if $D$ is not open. Instead use $E^{\mathrm{\prime }}=\{p:\mathrm{\exists }d\in De(p)\le d\}$: from $p$, find $d\le e(p)$ in $D$, and then $r\le p$ with $e(r)\le d$. Thus $E^{\mathrm{\prime }}$ is dense; meeting it puts such a $d$ in $H$. Hence $H$ is generic. Certainly $G\subseteq e^{-1}H$. If $e(p)\in H$, take $s\in G$ with $e(s)\le e(p)$. Conditions below $p$ are dense below $s$ by the refinement calculation, so F3 and genericity yield $r\in G$ below $p$, and $p\in G$. This proves $e^{-1}H=G$.

Conversely let $H$ be $Q$-generic and put $G=e^{-1}H$. For a ground dense $D\subseteq P$, the set $\{q:\mathrm{\exists }d\in Dq\le e(d)\}$ is dense in $Q$: first refine to an image, then to the image of a member of $D$. Meeting it gives a member of $D$ in $G$, so $G$ meets every ground dense set and is nonempty. Order preservation gives upward closure. For $p,s\in G$, the set $D_{p,s}=\{r:r\perp p\text{ or }r\perp s\text{ or }r\le p,s\}$ is dense: refine successively toward $p$ and $s$ whenever compatible, and otherwise stop at the corresponding incompatible alternative. A point in $G\cap D_{p,s}$ cannot be incompatible with either, by compatibility preservation and directedness of $H$; it is the needed common refinement in $G$. Finally, for $q\in H$, the image is dense below $q$, and F3 gives $e(p)\in H$ below $q$ for some $p$. Thus $q$ belongs to the upward closure of $e[G]$. The opposite inclusion is upward closure of $H$.

Equality substitution extends to each fixed formula by induction on its construction. Conjunction uses each conjunct. For negation, suppose $p$ forces the parameter equalities and $\mathrm{\neg }\psi (\vec{a})$; an extension forcing $\psi (\vec{b})$ would, by persistence and the induction hypothesis, force $\psi (\vec{a})$, contrary to F2. Reverse the equalities for the converse. For an existential, at every extension obtain its dense name witness, keep that witness fixed, and change the parameters by the induction hypothesis; the same dense-witness clause proves the substituted existential. Atomic cases are the equality and membership substitution calculations. This proves substitution at any condition forcing the parameter equalities, without appealing to generic semantics.

Membership is transported in both directions as well. If $p{⊩}_{P}a\in b$, first refine any $q\le e(p)$ to $e(r)$ with $r\le p$, then use the source membership witness and the equality equivalence. Conversely, for $r\le p$ apply the target membership clause below $e(r)$, obtaining an entry $⟨v,t⟩\in b$ and $q\le e(r),e(t)$ forcing $T(a)=T(v)$. Refine to $w\le r,t$ with $e(w)\le q$ and reflect equality. This is the source membership test. Empty right names fail both membership tests.

Apply the Q-name round trip to $a=T(\sigma )$. Every $e(p)$ forces $T(R(T(\sigma )))=T(\sigma )$, so equality reflection proves that every $p$ forces $RT(\sigma )=\sigma$. Thus both translations are inverse modulo forced equality. The empty name translates to the empty name.

Induction on source name rank and the equality $p\in G⟺e(p)\in H$ give $T(\sigma {)}^H={\sigma }^G$ directly from the valuation clause. For $R$, an active coefficient $p\in G$ coming from $⟨v,q⟩\in \tau$ has $e(p)\le q$, hence $q\in H$. Conversely if $q\in H$, the inverse correspondence supplies $p\in G$ with $e(p)\le q$, so the inverse entry is active. Induction identifies their subname valuations and yields $R(\tau {)}^G={\tau }^H$. These two equalities imply both inclusions of the extensions.

Induct now on each fixed formula for full forcing equivalence. Atomic cases have been proved. Conjunction is immediate from its two clauses. If $p{⊩}_P\mathrm{\neg }\psi (\vec{\sigma })$ and some $q\le e(p)$ forced $\psi (T\vec{\sigma })$, refine to $r\le p$ with $e(r)\le q$ and apply persistence and the formula induction hypothesis to contradict source negation. Conversely any source extension forcing $\psi$ maps to a target extension forcing its translation, which is impossible if $e(p)$ forces its negation.

For the existential forward direction, below any $q\le e(p)$ first find $r\le p$ with $e(r)\le q$, then refine $r$ to a source witness $\sigma$ for the matrix. The induction hypothesis transports that witness to $T(\sigma )$. For the converse, at $r\le p$ the target existential supplies $q\le e(r)$ and a $Q$-name $\tau$ forcing its matrix with parameters $T\vec{\sigma }$. Refine to $s\le r$ with $e(s)\le q$. Every condition forces $TR(\tau )=\tau$, so formula substitution changes this witness to $T(R(\tau ))$. The induction hypothesis for the matrix reflects it to the source witness $R(\tau )$ at $s$. This proves the dense-witness test at $p$, and completes the induction. All names quantified over here belong to the given ground when the proof is performed internally.

All constructions above are set images, Separation, definable recursion and finite refinements. The atomic inductions use ranks of set names; the formula induction is external for each fixed finite formula, interpreted inside the ground. Thus no generics were needed for the forcing equivalence, no external completeness or countability was used, and no choice function was selected. Empty preorders are excluded; singleton preorders and noninjective maps satisfy the same calculations. Boolean zero, if a target is presented as a Boolean algebra, must be removed so that its nonzero part is a forcing preorder. [step 1.2, step 5.1, step 3.4] QED.

Let $\pi :P\to S=P\mathrm{/}\sim$ be the quotient in F1. It preserves order and both compatibility directions. It is onto, hence has dense image: every class has some representative, and its own class is below itself. This uses the representative of one specified class at a time, not a choice of representatives of all classes. Therefore $\pi$ meets all of F3's hypotheses, even though it may fail to reflect the original order or to be injective.

In the downward-open topology on $P$, F2 constructs $B=\mathrm{RO}(P)$ and $e(p)=\mathrm{int}\overline{\downarrow p}$. It proves $e(p)\subseteq e(q)$ iff $p{\le }^{\ast }q$ and nonzero intersection iff original compatibility, and proves image density in $B\setminus \{0_B\}$. Thus $e$ too meets F3's hypotheses. Factoring through the quotient gives the dense order embedding $[p]\mapsto e(p)$ of $S$. The factor is well-defined and injective because mutual inclusion of the regular opens is exactly mutual ${\le }^{\ast }$. A nonzero Boolean meet is a common nonzero lower bound, so Boolean compatibility is exactly nonzero intersection.

Apply F3 separately to $\pi$, to $e$, and to the factored dense embedding. In each case its explicit $T$ translates coefficients forward and its $R$ uses all coefficients whose images refine an original coefficient. Both fixed-formula forcing directions follow, including existential names, from its syntactic proof. For supplied generics its inverse-image/upward-image maps are inverse, and its two valuation equalities give both inclusions between the generic extensions. In particular all three presentations produce the same extensions. This conclusion uses the proved forced equality of round-trip names; it does not identify their sets of pairs literally.

Finally an arbitrary dense order embedding $j:P\to Q$ has the same properties. Order preservation preserves compatibility. If $j(p),j(r)$ have a common lower bound $q$, image density supplies $j(s)\le q$; order reflection gives $s\le p,r$, proving compatibility reflection. F3 therefore applies to this embedding as well. The singleton preorder yields the two-element regular-open algebra and its singleton nonzero part. Boolean zero is excluded because the nonzero image cannot be dense below zero in the full algebra; retaining zero still gives a preorder in the two-element case, but not the dense target required by F3. All uses of F1–F3 are in ZF, and no filter-extension principle is involved. [F1, F2, F3, step 2.1] QED.

From external countability choose one injection $j:M\to \omega$. Since M contains the empty set, define $e(n)$ to be the unique $x\in M$ with $j(x)=n$ if there is one, and empty otherwise. This is a surjection $e:\omega \to M$. F1 constructs G through p by least enumeration indices, so ambient Choice is unnecessary.

Apply F3 to M and this G. It gives transitivity and ZF, and the fact that M satisfies F6 licenses exactly its ground-name well-ordering step to obtain AC in M[G]. F4 then gives the same ordinals, and F2 gives the asserted equivalence between truth and a condition of G forcing the formula.

Define $h(n)=e(n{)}_G$ when e(n) is a P-name and $h(n)=\mathrm{\varnothing }$ otherwise. External Separation and Replacement make h a function on omega. Every member of M[G] is a value of a name in M, hence appears in h. Assigning each member its least preimage under h injects M[G] into omega. This proves external countability even when distinct names have the same value.

Steps 1.1–2.2 prove all conclusions from the supplied CTM. The single injection j was part of the external countability hypothesis; no collection of CTMs or full-theory model was constructed from a consistency assertion. The only use of AC was the internal one in step 2.1.

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.

On input p first check whether it is a certified T-proof with contradictory conclusion, using F3. For a valid such proof scan its finitely many lines, collecting each nonlogical axiom sentence with its certificate and retaining the line references. Denote the finite support by Delta(p); the same derivation is a refutation from that support. This is a bounded loop over the decoded list, using the operations in F3, and is among the B-verified constructors in the hypothesis. On any invalid input use the fixed default output zero.

On a valid refutation input, apply the stipulated total constructors to Delta(p). They return ZFC proofs of existence of a suitable finite-fragment CTM and of its conversion to a nonempty model N of Delta(p), the two proof roles in F1. Concatenate those proofs with renamed variables and corrected references. Append the stipulated soundness-constructor proof for the particular finite derivation p: a model of all its axiom lines satisfies every line by the logical axiom and inference checks, hence satisfies its contradictory final sentence. The nonempty set model N cannot satisfy that sentence, so the combined proof is a ZFC refutation. Denote its code by r(p).

Every operation used in r has a totality and correctness verification in B by the stated hypothesis; composition with the bounded parser and the invalid-input branch therefore gives a total r whose verified property is $\mathrm{\forall }p({\mathrm{Prf}}_T(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prf}}_{\mathrm{Z}\mathrm{F}\mathrm{C}}(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))$. This step uses the actual constructor verifications as inputs, rather than inferring them from the external fragment-existence scheme.

Apply F2 to r with source theory ZFC and target theory T. It yields the displayed Con implication in B. All CTMs used in constructing the proof code were confined to their fixed finite source fragments; neither the reduction nor its arithmetic consequence constructs a CTM of full ZFC.

Take $T=\mathrm{Z}\mathrm{F}\mathrm{C}+\phi$ in F1. Its certified axioms are either certified ZFC axioms or the single extra sentence phi, distinguished by a fixed tag and exact sentence-code equality. For a certified T-refutation its finite support is therefore a finite list of ZFC axioms, possibly together with phi. The assumed uniform verification supplies the constructors for that exact list; if phi is absent, restrict the same target verification to the smaller list. Thus T meets every hypothesis of F1.

F1 now yields the claimed implication in B. No existence assertion for a full ZFC CTM occurred in step 1.1: the hypothesis supplied verified proof constructors for the finite supports. Consequently a semantic extension of a single CTM does not suffice to instantiate this corollary unless those additional data are also provided.