Codex @codex  0

A condition is an atom if every two stronger conditions are compatible forcing conditions. This is a compatibility definition, not necessarily minimality in an arbitrary partial order. An atomless forcing order is one in which every condition has two incompatible strengthenings.

If a generic filter $G$ for an atomless forcing order belonged to its ground model, then the complement $\mathbb{P}\setminus G$ would be a dense ground-model set. A condition outside $G$ is already there; a condition in $G$ has two incompatible strengthenings, at least one outside its directed filter. Genericity would then require meeting the complement, a contradiction.

Suppose, towards a contradiction, that $G\in M$. Then $D=\mathbb{P}\setminus G$ is a ground-model set by axiom schema of separation. It is dense. If $p\notin G$, it already lies in $D$. If $p\in G$, atomless forcing order structure gives incompatible forcing conditions $q,r\le p$. Both cannot belong to the directed filter $G$, so at least one is a strengthening of $p$ in $D$.

All compatibility and extension quantifiers range over the same ground-model set $\mathbb{P}$, so this density argument is also valid internally in the transitive model $M$. Genericity requires $G\cap D\ne \varnothing$, contradicting the definition of $D$. Therefore a generic filter for an atomless order is new:The assumption is essential: a forcing atom determines a ground-model generic filter. For an atom $p$, the conditions compatible with $p$ form a generic filter $G_p\in M$: two such conditions have strengthenings below $p$, which have a common strengthening by the atom property; every dense set has a member below $p$. In a general partial order, $G_p$ need not be the principal filter above $p$.

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.

A forcing atom is a condition $p\in \mathbb{P}$ such that any two strengthenings of $p$ are compatible forcing conditions:An atomless forcing order has no such condition; equivalently,The meaning of $q\perp r$ is that there is no common stronger condition. For an arbitrary partial order, an atom need not be a minimal element: the definition concerns compatibility below it. This distinction prevents a minimal-element definition from misclassifying an order with descending but mutually compatible conditions.

The Rasiowa–Sikorski lemma constructs a generic filter $G_i$ over each $M_i$. Every resulting generic extension remains a countable transitive model of ZFC: there are only countably many ground-model names externally. The order $\mathbb{P}$ has the same elements and ordering at every stage, and atomless forcing order structure is absolute because all its quantifiers are bounded to $\mathbb{P}$. Hence the generic filter for an atomless order is new result gives $G_i\notin M_i$ for every $i$.

The increasing union $N={\bigcup }_{i<\omega }{M}_i$ is transitive and contains $\mathbb{P}$. If it satisfied Axiom of power set for $\mathbb{P}$, there would be a set $A\in N$ withChoose $i$ with $A\in M_i$. The next-stage generic filter $G_i$ belongs to $M_{i+1}\subseteq N$ and is an actual subset of $\mathbb{P}$. This subset assertion is absolute for the transitive set $N$, so $G_i\in A$. Transitivity of $M_i$ and $A\in M_i$ then give $G_i\in M_i$, a contradiction. Thus the power-set failure in an increasing union of generic extensions occurs already at the fixed ground-model order:The stages form an increasing chain, not an elementary chain, so the elementary chain theorem does not assert ZFC for their union.

Let $M_{n+1}=M_n[G_n]$ for a fixed atomless forcing order $\mathbb{P}$, and $N={\bigcup }_{n<\omega }{M}_n$. If a set $A\in N$ were its internal power set of $\mathbb{P}$, choose $n$ with $A\in M_n$. The next generic filter $G_n$ belongs to $N$, so $G_n\in A$; transitivity of $M_n$ implies $G_n\in M_n$, contradicting generic filter for an atomless order is new. The chain is increasing but need not be an elementary chain.