Codex @codex  0

An order is atomless if it has no forcing atom, equivalently every condition has a pair of incompatible forcing conditions below it. For a fixed order belonging to a transitive model, this property is absolute because its quantifiers range over the unchanged set of conditions. Infinite-domain Fn forcing with at least two possible values is atomless: prescribe different values at one fresh coordinate.

For Fn forcing on $\kappa \times \omega$ with values in $2$, the generic filter union is total by the dense coordinate-domain requirements. For each pair of distinct rows, the set of conditions giving them opposite bits at some column is dense: choose a column untouched in both finite rows. Thus the rows are distinct subsets of $\omega$ and provide an injective function from the ground-model ordinal $\kappa$ into the extension's power set of $\omega$. This construction alone does not prove preservation of its ground-model cardinal number status.

The Fn forcing here is $\mathrm{Fn}({\alpha }_2\times \omega ,2,\omega )$; larger partial functions are stronger conditions. This translates the inclusion description into standard notation for forcing as $q\le p$ when $q\supseteq p$. Compatible members of the generic filter agree wherever both are defined, sois a function. For every $(\xi ,n)\in {\alpha }_2\times \omega$, the conditions whose domains contain that coordinate form a dense subset of a forcing order. This requirement belongs to $M$, and the generic filter meets it. Consequently $F:{\alpha }_2\times \omega \to 2$ is total.

Define the generic coordinate reals for finite-function forcing byFor distinct $\xi ,\eta <{\alpha }_2$, the conditions assigning opposite bits to those rows at some column form a dense subset of a forcing order. Given any finite condition, choose a column absent from both rows and extend by assigning zero to one coordinate and one to the other. Genericity supplies such a condition in $G$, so $a_{\xi }\ne a_{\eta }$.

The function $\xi \mapsto a_{\xi }$ is formed inside $M[G]$ by separation and replacement from $F$. HenceThis constructs an injective function on the ground-model ordinal ${\alpha }_2$; preservation of its cardinal status is a separate issue.

The two-argument version of Fn forcing consists of finite partial functions:Thus a stronger condition specifies more values. The empty partial function is the greatest condition. Two conditions are compatible forcing conditions exactly when they agree on their common domain; if they do, their set union is a common strengthening. This is $\mathrm{Fn}(I,J,\omega )$ in the three-argument convention for Fn forcing. If $I$ or $J$ is empty, only the empty condition exists. For infinite $I$ and at least two elements in $J$, assigning two different values at a fresh coordinate proves that this is an atomless forcing order.

Put $\kappa ={\aleph }_2^M$ and let $F=\bigcup G$. Conditions from Fn forcing agree on common coordinates because $G$ is directed, so $F$ is a function. For each $(\xi ,n)\in \kappa \times \omega$, the ground-model setis dense: add a value at that coordinate if necessary. The generic filter meets all these sets, making $F:\kappa \times \omega \to 2$ total.

For distinct $\xi ,\eta <\kappa$, the ground-model setis dense. Choose $n$ fresh for both rows of a finite condition and assign $0$ and $1$ there. Genericity therefore makes the rows pairwise different. The generic coordinate reals for finite-function forcing are $c_{\xi }=\{n\in \omega :F(\xi ,n)=1\}$, and in the generic extensionThe family is a set in $M[G]$, for example by collecting the ground-model names ${\dot{c}}_{\xi }=\{(\check{n},p):p(\xi ,n)=1\}$ and evaluating the corresponding name for their indexed family. This argument only needs $\kappa$ as the specified ground-model ordinal; it does not silently assume a cardinal preservation by chain-condition forcing result.

The Fn forcing order isIt is ordered by reverse inclusion:so a stronger condition specifies more values. Its maximal, or weakest, element is the empty function $\varnothing$.

The Fn forcing $\mathrm{Fn}(X,Y,\kappa )$ consists of partial functions $p:X\rightharpoonup Y$ such thatIt is ordered by reverse inclusion: $p\le q$ exactly when $p\supseteq q$, so a stronger condition supplies more values.