Boolean Prime Ideal Theorem in the Basic Cohen Model

If $m=0$, take the empty family of clopens: there is one empty tuple, and the conclusion is the given truth. Assume $m>0$. By the truth lemma choose $p^{\mathrm{\prime }}\in G$ which forces $\phi (\check{\stackrel{ˉ}{x}},\dot{s},\dot{A})$, where ${\dot{s}}_j={\dot{a}}_{h(j)}$. It is enough to show that below every such $p^{\mathrm{\prime }}$ there is a condition forcing the asserted clopen-box conclusion, because density closure and the truth lemma then put that conclusion in $V[G]$.

Extend $p^{\mathrm{\prime }}$ to a condition $p$ and choose $k\in \omega$ so that $\mathrm{dom}(p)=k\times k$, $\mathrm{rng}(h)\subseteq k$, and the rows $p_i=p\upharpoonright (\{i\}\times k)$ are pairwise distinct for $i<k$. This is a finite construction: first enlarge the rectangle, then give each pair of rows a fresh column on which their bits differ. Put $U_j=[p_{h(j)}]$. The $U_j$ are pairwise disjoint because their defining binary strings are incompatible, and $p$ forces ${\dot{a}}_{h(j)}\in U_j$.

Suppose, towards a contradiction, that some $r\le p$ forces that a tuple $\dot{t}\in {\dot{A}}^m$ lies in ${\prod }_{j<m}{U}_j$ but fails $\phi (\check{\stackrel{ˉ}{x}},\dot{t},\dot{A})$. By finitely many applications of the membership forcing clause and density, strengthen $r$ so that ${\dot{t}}_j={\dot{a}}_{z(j)}$ for a ground-model map $z:m\to \omega$. The disjointness of the $U_j$ and F2 make $z$ injective. Moreover, if $z(j)<k$, then $r\le p$ and $r⊩{\dot{a}}_{z(j)}\in [p_{h(j)}]$ give $p_{z(j)}=p_{h(j)}$; the pairwise distinct rows imply $z(j)=h(j)$. Thus every $z(j)\mathrm{\ne }h(j)$ lies outside $k$.

Let $\pi$ interchange $h(j)$ and $z(j)$ whenever they differ and fix every other coordinate. The transpositions are disjoint by the last conclusion of step 2.1. The symmetry lemma gives

A common extension of $p$ and $\pi r$ would force both $\phi (\check{\stackrel{ˉ}{x}},\dot{s},\dot{A})$, by persistence from $p\le p^{\mathrm{\prime }}$, and its negation, by step 3.1. This is impossible. Hence $p$ forces that every tuple from $A$ in the displayed clopen box satisfies $\phi$. Since such a $p$ is available below every $p^{\mathrm{\prime }}$ forcing the original instance, step 1.1 and density closure prove the first assertion in $V[G]$.

For the consequence, choose fixed formulas and ordinal parameters which uniquely define the finitely many supported parameters from $A,u$. Replace their occurrences in the desired assertion by those definitions and conjoin uniqueness. Apply the first assertion to the concatenated tuple $u^{⌢}s$. Keep the coordinates belonging to $u$ at their original values and retain only the clopens belonging to $s$. All clopens in the larger box are pairwise disjoint, so the retained ones avoid $\mathrm{rng}(u)$; unique definability restores the fixed parameters after every permitted substitution. The construction is finite and makes no choice from an arbitrary family.

If $F=\mathrm{\varnothing }$, then $T$ is empty unless $r=0$. In either case there are no coordinates to vary: take the empty clopen family, and the fixed sentence $\mathrm{\Phi }$ remains true. Assume henceforth that $F$ is nonempty, enumerate it without repetition as $⟨a_0,\dots ,a_{m-1}⟩$, and concatenate this tuple after $f$.

Choose the finitely many formulas and ordinal parameters which uniquely define $B,d$, and the sets occurring in $\mathrm{\Phi }$ from $A,f$. In one formula $\psi (A,f,a_0,\dots ,a_{m-1})$, assert those unique definitions, reconstruct each member of $T$ by its finite list of coordinate positions, and assert the entire conjunction $\mathrm{\Phi }$. If $S=B\setminus I$ occurs, replace it by the conjunction “belongs to $B$ and does not belong to $I$”; replace ${\mathrm{\neg }}_{B}d(t)$ by the uniquely specified Boolean complement in $B$. Thus $\psi$ is a single fixed membership formula and is true of the concatenated tuple.

Apply F1 to $f^{⌢}⟨a_0,\dots ,a_{m-1}⟩$ and the formula from step 1.2. Retain the clopens assigned to the $a_i$ and discard those assigned to $f$. Pairwise disjointness of the larger family makes every retained clopen disjoint from every member of $\mathrm{rng}(f)$. If basic clopens $W_{a_i}$ were prescribed in advance, increase the finitely many defining prefix lengths so that the retained neighbourhood of $a_i$ lies in $W_{a_i}$; shrinking does not destroy the conclusion.

Let $g:F\to A$ select $g(a)\in U_a$. Since the $U_a$ are pairwise disjoint, $g$ is automatically injective, so every $g\circ t$ remains in $A_{\mathrm{\ne }}^r$ and repeated occurrences of one coordinate are replaced coherently. The continuity conclusion for $\psi$ keeps $f$ fixed and preserves all unique definitions and every conjunct of $\mathrm{\Phi }$. This proves the simultaneous assertion, including the specialization to $B\setminus I$. Only a finite tuple was enumerated and finitely many clopens were shrunk; no choice function on an arbitrary family was used.

Let $\mathcal{D}$ be the set of all proper ideals $J\subseteq B$ which are ordinal-definable from $A,f$. This is a set by Separation from $\mathcal{P}(B)$, because existence of a rank, formula code, and finite ordinal tuple giving a unique definition is the first-order property in F2. It is nonempty: nontriviality makes $\{0_B\}$ a proper ideal, and $0_B$ is uniquely definable from the supported algebra $B$. Assign to each member of $\mathcal{D}$ its unique least code in the rank–formula–fixed-arity tuple order of F2. Replacement makes the range a set; restriction of that setlike class order well-orders the range and therefore well-orders $\mathcal{D}$. Enumerate its order type as $⟨J_{\xi }:\xi <\theta ⟩$.

By F3 define an increasing sequence $⟨I_{\xi }:\xi \le \theta ⟩$. Put $I_0=\{0_B\}$. Given $I_{\xi }$, set

We prove by transfinite induction that every $I_{\xi }$ is a proper ideal and that $I_{\eta }\subseteq I_{\xi }$ for $\eta <\xi$. The initial ideal is proper by nontriviality. [F1, step 1.2, base] At a successor, either the value is unchanged or it is the proper ideal $J_{\xi }$ containing the preceding value. At a limit, the union of an increasing chain of ideals contains $0_B$, is downward closed, and is closed under binary joins because any two of its elements already occur together at some later one of their two stages. If $1_B$ belonged to the union, it would belong to one earlier $I_{\xi }$, contradicting that stage's propriety.

Put $I=I_{\theta }$. The recursion and its input well-order are uniquely definable from $A,f$ and the fixed definition of $B$, so F2 and F3 make $I$ ordinal-definable from $A,f$. Step 2.1 makes it a proper ideal. Moreover $\mathrm{TC}(I)\subseteq \{I\}\cup \mathrm{TC}(B)$ because $I\subseteq B$. The set $I$ has the displayed supported definition, while every descendant in $\mathrm{TC}(B)$ has the hereditary definability required by $B\in C$. The parameter-HOD convention in the Statement therefore gives $I\in C$ directly; no theorem about ordinary parameter-free HOD is being substituted.

Suppose $J\in \mathcal{D}$ and $I\subseteq J$. Write $J=J_{\beta }$. Since $I_{\beta }\subseteq I\subseteq J_{\beta }$, the successor rule gives $I_{\beta +1}=J_{\beta }$. Monotonicity then gives $J\subseteq I$, and hence $J=I$. This proves the asserted maximality within $\mathcal{D}$. It neither applies Zorn's lemma nor chooses a maximal member of an arbitrary partially ordered set; every stage is forced by a fixed definable well-order and a yes-or-no inclusion test, as F4 permits.

For an infinite ground set $I$, write $P_I=\mathrm{Fn}(I\times \omega ,2,<\omega )$ and let ${\mathcal{G}}_I$ be the finite permutations of $I$, with the normal filter generated by pointwise stabilizers of finite subsets. The support-restriction lemma holds: if finite $S$ supports every name in a forced formula, then $r⊩\phi$ implies $r\upharpoonright (S\times \omega )⊩\phi$. Indeed every strengthening of the restriction is compatible, after a permutation fixing $S$, with an image of $r$; F2 transports $\phi$ to that image, and dense decision rules out a condition forcing its negation.

A condition can be strengthened so that its nonempty coordinate rows all have one finite length and are pairwise distinct. Such a condition distinguishes its support: images of two different rows under compatible coordinate permutations cannot land on the same coordinate, because their common-length binary strings would then have to be equal. This uses only finitely many fresh bit positions.

We record the compatible-type lemma used below. Fix a finite condition type $t$, represented by an ordered $k$-element support and a fixed ordered list of $k$ Cohen rows. For every finite $d,m$ there is $R=R(t,d,m)$ such that, from any family $(r_{\vec{\alpha }}:\vec{\alpha }\in R^d)$ of type $t$, one can find $m$-element $K_i\subseteq R$ for which the conditions indexed by ${\prod }_{i<d}{K}_i$ are pairwise compatible. This is Ransom's compatible-type lemma in §4, derived in Appendix C as Corollary C.4 from the exact finite Todorčević--Farah compatible-type lemma, Lemma C.3 there. For the present Cohen-row specialization, its reduction is direct. Flatten a condition $r$ by writing each actual finite binary row $r(\xi )$ into the disjoint ordinal block $[\omega \xi ,\omega (\xi +1))$. Because $t$ fixes the ordered list of row strings, all flattened conditions have one fixed Todorčević--Farah type. Two original conditions are compatible exactly when, at every shared coordinate, their two binary rows agree on their common domain; this is exactly when the flattened finite bit conditions agree on every common block position. Thus flattening preserves compatibility in both directions. Applying Lemma C.3 to the flattened family gives the required rectangle, and unflattening gives the displayed conclusion. The finite lemma is the Ramsey-theoretic input recorded abstractly by F5. No fresh bits are introduced, and the flattened type depends only on $t$, not on the size or incompatibility graph of the indexed family.

Second, there is an infinite cardinal $\mathrm{\Theta }$ such that every countably colored finite product ${\mathrm{\Theta }}^d$ has pairwise disjoint infinite coordinate subsets with constant color. For each $d$, apply F6 high enough above ${\mathrm{\aleph }}_0$ to the coloring of ordered $d$-tuples, first restricting to increasing tuples and then assigning the $d$ positions to disjoint blocks; take a cardinal above the resulting countable family of bounds, one for each $d<\omega$. Ground AC supplies the cardinal arithmetic and the simultaneous sequence of bounds.

The finite-support system has minimal supports. If finite $S$ and $T$ support a name, then $S\cap T$ does too: the group fixing $S\cap T$ is generated by the two pointwise stabilizers of $S$ and $T$. Indeed, decompose a finite permutation into transpositions off $S\cap T$; a transposition already fixes $S$ or $T$ unless it exchanges a point of $S\setminus T$ with one of $T\setminus S$, and in that case factor it into three transpositions through a fresh coordinate outside $S\cup T$, alternating between the two stabilizers. Thus every such permutation is a finite product of permutations that fix the name. Choosing a finite support of minimum cardinality and intersecting it with any other support shows that it is contained in every support, hence is the least one. Now take $\omega \subseteq \mathrm{\Theta }$. For an $M$-name $\dot{z}$ in the $\omega$-coordinate symmetric system, recursively define $\mathrm{\Sigma }(\dot{z})={\bigcup }_{(\dot{u},r)\in \dot{z}}\{(\pi \mathrm{\Sigma }(\dot{u}),\pi r):\pi \in \mathrm{fix}(S_z)\},$ where $S_z\subseteq \omega$ is the least finite support of $\dot{z}$. For a $P_{\mathrm{\Theta }}$-name $\dot{w}$ whose support lies in $\omega$, define $\mathrm{\Gamma }(\dot{w})$ by retaining exactly the immediate pairs whose condition and recursively gathered subname have support in $\omega$. Equivariance and rank induction give $\mathrm{\Gamma }\mathrm{\Sigma }(\dot{z})=\dot{z}$; they also give $\mathrm{\Sigma }\mathrm{\Gamma }(\dot{w})=\dot{w}$ whenever $\mathrm{supp}(\dot{w})\subseteq \omega$. For arbitrary hereditarily symmetric $\dot{w}$, a finite permutation first moves its finite support into $\omega$, so $\dot{w}$ is a permutation image of a name in the range of $\mathrm{\Sigma }$. These are precisely the spreading and gathering maps of Ransom Section 5.

It remains to derive the internal ultrafilter statement from filter extension. Given any hereditarily symmetric name $\dot{Y}$, form the nice name for its intersection with $\dot{X}$, $\widehat{Y}=\{(\dot{z},r)\in \mathrm{dom}(\dot{X})\times P_{\omega }:r⊩\dot{z}\in \dot{Y}\wedge \dot{z}\in \dot{X}\}\mathrm{.}$ The forcing theorem proves $1⊩\widehat{Y}=\dot{Y}\cap \dot{X}$, and equivariance shows that the union of supports of $\dot{X}$ and $\dot{Y}$ supports $\widehat{Y}$. Let $C(\dot{X})$ be the set of all hereditarily symmetric names in the ground power set $\mathcal{P}(\mathrm{dom}(\dot{X})\times P_{\omega })$ that $1$ forces to be subsets of $\dot{X}$. If $Y\subseteq X={\dot{X}}^G$ belongs to $N$, choose an HS name $\dot{Y}$ with value $Y$; then $\widehat{Y}\in C(\dot{X})$ and ${\widehat{Y}}^G=Y\cap X=Y$. Thus $C(\dot{X})$ represents every subset of $X$ in $N$, and ground AC well-orders $C(\dot{X})$ and $P_{\omega }$.

Work first with the $\mathrm{\Theta }$-coordinate system. Retain the supplied common support $E$ of $\dot{F},\dot{X}$, choose a finite support $S_Y$ of $\dot{Y}$, and put $S=E\cup S_Y$ and $D=S_Y\setminus E$. Preserve the originally supplied condition as $p^{\ast }$ and put $p_0=p^{\ast }\upharpoonright (S\times \omega )$. We first construct a witness $q_0\le p_0$ supported by $S$. Once this is done, $q=q_0\cup p^{\ast }$ is a well-defined condition below $p^{\ast }$, and for every $\pi \in \mathrm{fix}(E)$ the condition $\pi q$ strengthens $\pi q_0$. Consequently $1$ forces the orbit name based on $(q,{\dot{Y}}^{\mathrm{\prime }})$ to be a subfamily of the one based on $(q_0,{\dot{Y}}^{\mathrm{\prime }})$, so FIP for the latter implies FIP for the required former orbit. This is the restoration of the coordinates of $p^{\ast }$ omitted by $p_0$. If $D=\mathrm{\varnothing }$, ground Choice in the full forcing extension and the maximum principle supply a name for an ultrafilter extending the filter generated by $\dot{F}$, and some $r\le p_0$ forces one side ${\dot{Y}}^{\mathrm{\prime }}$ into it. Hence $r$ forces that $\dot{F}\cup \{{\dot{Y}}^{\mathrm{\prime }}\}$ has FIP; applying support restriction to this latter formula gives $q_0=r\upharpoonright (E\times \omega )$, which forces the same assertion. Every permutation fixing $E$ fixes both $q_0$ and ${\dot{Y}}^{\mathrm{\prime }}$. The orbit name is empty off $q_0$ and contributes the single FIP-compatible side below $q_0$, so the assertion for $q_0$, and hence by the preceding paragraph for $q=q_0\cup p^{\ast }$, is forced by $1$. Assume henceforth that $D\mathrm{\ne }\mathrm{\varnothing }$. For each $i\in D$ choose pairwise disjoint sets $H_i\subseteq \mathrm{\Theta }\setminus S$ of size $\mathrm{\Theta }$. For $\vec{\alpha }\in {\prod }_{i\in D}{H}_i$, let ${\pi }_{\vec{\alpha }}$ be the product of transpositions $(i,{\alpha }_i)$; it fixes $E$.

The full forcing extension satisfies ZFC. By A1 and the maximum principle choose a $P_{\mathrm{\Theta }}$-name $\dot{U}$ such that $1$ forces that $\dot{U}$ is an ultrafilter on $\dot{X}$ extending the filter generated by $\dot{F}$. For each $\vec{\alpha }$, choose a condition $r_{\vec{\alpha }}\le {\pi }_{\vec{\alpha }}{p}_0$ deciding which of ${\pi }_{\vec{\alpha }}\dot{Y}$ and its complement belongs to $\dot{U}$, put $q_{\vec{\alpha }}={\pi }_{\vec{\alpha }}^{-1}{r}_{\vec{\alpha }}$, and strengthen $q_{\vec{\alpha }}$ as in step 1.2, also putting every coordinate of $S$ into its support, while preserving the decision. Reset $r_{\vec{\alpha }}={\pi }_{\vec{\alpha }}{q}_{\vec{\alpha }}$. Color $\vec{\alpha }$ by the chosen side, the finite condition type of $r_{\vec{\alpha }}$, and $q_{\vec{\alpha }}\upharpoonright (S\times \omega )$. There are countably many colors. Step 1.4 yields infinite subblocks on which all three data are constant. Call the common restriction $q_0\le p_0$ and the common side ${\dot{Y}}^{\mathrm{\prime }}$. Then $q_0$ distinguishes its support, and every ${\pi }_{\vec{\alpha }}{q}_{\vec{\alpha }}=r_{\vec{\alpha }}$ forces ${\pi }_{\vec{\alpha }}{\dot{Y}}^{\mathrm{\prime }}\in \dot{U}$, has one fixed type, and distinguishes its support.

Fix $m<\omega$. Step 1.3 thins the infinite subblocks to $m$-element sets $K_i^m$ so that all deciding conditions ${\pi }_{\vec{\alpha }}{q}_{\vec{\alpha }}$, for $\vec{\alpha }\in {\prod }_i{K}_i^m$, are mutually compatible. For any subset $T$ of that finite product, their union forces every ${\pi }_{\vec{\alpha }}{\dot{Y}}^{\mathrm{\prime }}$ with $\vec{\alpha }\in T$ into $\dot{U}$ and hence forces that these sets together with $\dot{F}$ have FIP. By step 1.1 restrict this union to the supports of $\dot{F},\dot{X}$, and those finitely many image names. The restriction is exactly ${\bigcup }_{\vec{\alpha }\in T}{\pi }_{\vec{\alpha }}{q}_0$: pairwise compatibility and the distinguishing property from step 1.2 prevent two unequal source rows from being identified, while the common type makes equal source rows agree. Therefore the following assertion holds.

Let $\mathrm{\Delta }$ be any finite part of ${\mathrm{Orb}}_{\mathrm{fix}(E)}(q_0,{\dot{Y}}^{\mathrm{\prime }})$. If $\mathrm{\Delta }=\mathrm{\varnothing }$ there is nothing to prove. Otherwise discard pairs whose conditions cannot occur together; it suffices to handle every mutually compatible subfamily. Write the remaining name--condition pairs as $({\pi }_j{\dot{Y}}^{\mathrm{\prime }},{\pi }_j{q}_0)$ for $j<n$. For each $i\in D$, the finite sets $J_i=\{{\pi }_j(i):j<n\}$ are mutually disjoint and avoid $E$: an intersection ${\pi }_j(i)={\pi }_k(i^{\mathrm{\prime }})$ for $i\mathrm{\ne }{i}^{\mathrm{\prime }}$ would place two distinct distinguished rows at one coordinate of compatible conditions. Choose $m\ge {\max }_i\mathrm{\mid }{J}_i\mathrm{\mid }$ and a finite permutation $\sigma$ fixing $E$ which sends every $J_i$ injectively into $K_i^m$. Step 3.1 applies to $\sigma \mathrm{\Delta }$; F2 applied to ${\sigma }^{-1}$ fixes $\dot{F},\dot{X}$ and transfers FIP back to $\mathrm{\Delta }$. Since every finite orbit subfamily was arbitrary, the orbit based on $q_0$ has FIP. Finally restore the discarded coordinates by taking $q=q_0\cup p^{\ast }$ as in step 2.1. Then $q\le p^{\ast }$ and the orbit based on $q$ is forced to be a subfamily of the orbit based on $q_0$, proving the filter-extension property for $P_{\mathrm{\Theta }}$.

In an auxiliary $\mathrm{Coll}(\omega ,\mathrm{\Theta })$-extension $V$ of $M$, fix a bijection $b:\omega \to \mathrm{\Theta }$. Reindex conditions by $b$ and names recursively, obtaining maps $b:P_{\omega }\cong P_{\mathrm{\Theta }}$ and ${\phi }_b$. Ordinary rank induction makes $(b,{\phi }_b)$ an isomorphism of forcing relations in $V$. If $\dot{z}\in M$ is hereditarily symmetric and $\rho$ agrees with $b$ on its finite support, step 1.5 gives ${\phi }_b(\dot{z})=\rho \mathrm{\Sigma }(\dot{z})\in M$; conversely, move the finite support of a $P_{\mathrm{\Theta }}$-name into $\omega$ and use $\mathrm{\Gamma }$ to obtain its $M$-preimage. Hence ${\phi }_b$ restricts in $V$ to a bijection between the two classes of $M$-hereditarily symmetric names and is an isomorphism of the forcing relations relativized to $M$. Apply it to the first-order assertion of the filter-extension property. The large-index witnesses from step 4.1 have inverse images $b^{-1}(q),{\phi }_b^{-1}({\dot{Y}}^{\mathrm{\prime }})$ in $M$, so they witness the countable-index assertion. The collapse supplies only the external comparison map and inserts no object into the symmetric model.

Starting with a name for a proper filter $F_0$ on $X$, recursively traverse the well-order of $C(\dot{X})$. For one subset name $\dot{Y}$, traverse the condition well-order and repeatedly apply the countable-index filter-extension property from step 5.1; adjoining the chosen orbit at each successor stage produces a supported FIP name and a dense set of conditions forcing that it contains $\dot{Y}$ or $\dot{X}\setminus \dot{Y}$. Take unions at limits, repeat for the next member of $C(\dot{X})$, and finally take the filter generated by the accumulated FIP family. The fixed subgroup supporting $F_0$ and $\dot{X}$ supports every stage and the final name. Ground AC chooses the first witness at each ground recursion stage; F4 preserves FIP at increasing unions and properness after filter generation. By density and step 1.6, the final interpreted filter contains either every subset of $X$ in $N$ or its complement. It is therefore an ultrafilter in $N$ extending $F_0$.

Steps 5.1 and 6.1 prove UFL inside the transitive ZF model $N$. F7 gives BPI there. The ground uses of AC were exactly those listed in A1; no well-order, auxiliary ultrafilter, large-index bijection, or choice function is claimed to belong to $N$. The empty carrier has no proper filter, the one-element Boolean algebra is excluded by nontriviality, and the initial family for every actual proper filter already has FIP, so all degenerate cases are covered.

F1 and F2 give a transitive model $N$ of every ZF axiom.

F3 applies to the same $M$, $G$, finite-permutation group, normal filter, and class of hereditarily symmetric names, so $N$ satisfies the BPI assertion of F5. This route does not use the unsupported promotion of a parameter-definable maximal ideal in the Repický shortcut.

F4 applies to the same orbit set $A$ and shows internally that $A$ is infinite and Dedekind-finite. A well-order would enumerate its least unused elements and contradict Dedekind-finiteness, so $A$ is not well-orderable; by F5, AC would well-order it. Thus $N\models \mathrm{\neg }\mathrm{A}\mathrm{C}$.

Combining steps 1.1, 2.1, and 2.2 gives $N\models \mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\mathrm{\neg }\mathrm{A}\mathrm{C}$. The ground-model AC used by the search-and-shift construction is a metatheoretic construction hypothesis and is not asserted in $N$.

A standard finite refutation $R$ of $\mathrm{Z}\mathrm{F}+\mathrm{B}\mathrm{P}\mathrm{I}+\mathrm{\neg }\mathrm{A}\mathrm{C}$ contains only finitely many ZF schema instances. Fix this particular $R$, and let $\mathrm{\Delta }$ consist of those instances together with $\mathrm{\neg }\mathrm{A}\mathrm{C}$; BPI is retained as its single displayed target sentence. This is an external extraction from one alleged finite proof, not a claimed uniform construction formalized in PA.

Since $\mathrm{\Delta }$ is now one externally fixed fragment, F2 gives one finite ZFC proof that the basic Cohen symmetric construction has a set interpretation satisfying $\mathrm{\Delta }$. Append the fixed set-theoretic proof F3 to the same finite construction, enlarging the finite source fragment for the finitely many forcing, cardinal, name-rank, and symmetry instances occurring in F3. The result is a finite ZFC proof that this set interpretation also satisfies BPI, hence a finite ZFC proof of a model of $\mathrm{\Delta }+\mathrm{B}\mathrm{P}\mathrm{I}$. No effective dependence of this proof on arbitrary input codes is used.

Relativize every line of the fixed refutation $R$ to that set interpretation and append the ordinary finite satisfaction induction for the finitely many formulas occurring in $R$. This gives a finite contradiction proof in ZFC. No countable-transitive-model inference is made.

F1 says the assumed consistency of ZF implies consistency of the ZFC+GCH source and therefore of ZFC, contradicting step 3.1. Hence no standard finite target refutation exists, which is exactly the displayed external relative-consistency implication. The resulting consistent extension contains BPI and $\mathrm{\neg }\mathrm{A}\mathrm{C}$, so, under the same antecedent, ZF+BPI cannot prove AC.