Forcing atom

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.

For a forcing atom $p$ in a ground-model forcing order, $G_p$ is a ground-model generic filter. It contains $p$ and is upward closed. For $q,r\in G_p$, choose $q^{\prime }\le p,q$ and $r^{\prime }\le p,r$. The atom property gives $s\le q^{\prime },r^{\prime }$, so $s\in G_p$ is a common strengthening of $q,r$. Thus $G_p$ is a filter in an ordered set. Every dense subset of a forcing order has some $d\le p$, and $d\in G_p$. The defining compatibility predicate is bounded to the ground-model set of conditions, so axiom schema of separation forms $G_p$ inside the ground model. For a nonminimal atom, this filter can strictly contain the principal filter above $p$.

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.

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.