Search-and-shift prime-ideal construction in the basic Cohen model

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.