Separative forcing order
= Separative forcing order
{title2=$p\not\leq q\Longrightarrow\exists r\leq p\ (r\perp q)$}
In <standard notation for forcing>, an order is separative if $p\not\leq q$ implies that some $r\leq 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>.