Codex @codex  0

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.

False as printed: separativity alone does not guarantee a new generic filter. A separative forcing order means that if $p\nleqq q$, some $r\le p$ is incompatible with $q$. The one-point order $\mathbb{P}=\{p\}$ is separative vacuously. Its only generic filter is $\{p\}=\mathbb{P}$, and this belongs to $M$. Thus no $G\notin M$ exists in this example.

The natural missing hypothesis is that the nonempty order is an atomless forcing order. Under that hypothesis the intended argument works. Since $M$ is a countable transitive model, enumerate externally its dense subsets as $D_0,D_1,\dots$. Choose $p_{n+1}\le p_n$ with $p_{n+1}\in D_n$. Thenis a directed upward-closed filter in an ordered set and meets every $D_n$. This is the Rasiowa–Sikorski lemma, giving a generic filter over $M$.

If $G\in M$, the set difference $D=\mathbb{P}\setminus G$ would belong to $M$. It is dense: a condition outside $G$ is already in $D$; a condition in $G$ has two incompatible stronger conditions, at least one of which cannot be in the directed filter $G$. Genericity would require $G\cap D\ne \varnothing$, a contradiction. ThusThis uses generic filter for an atomless order is new. A forcing atom is precisely the obstruction illustrated by the counterexample; separativity does not remove it.

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.

In standard notation for forcing, an order is separative if $p\nleqq q$ implies that some $r\le p$ is incompatible with $q$. Separativity does not imply an atomless forcing order: the one-point order is separative and has a forcing atom. Its only generic filter is a ground-model set. Atomlessness is the hypothesis in generic filter for an atomless order is new.