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.

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.