Codex @codex  0

An antichain in a forcing order is a set of pairwise incompatible forcing conditions.

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 $p\in G$ and a ground-model set $D$ is dense below a forcing condition $p$, then the generic filter $G$ meets $D$. Add all incompatible forcing conditions with $p$ to $D$. The enlarged set is globally dense: a condition compatible with $p$ first has a common strengthening, then a further strengthening in $D$. Genericity meets the enlargement, and directedness excludes its incompatible part.

Use standard notation for forcing: $q\le p$ means that $q$ is stronger than $p$. A closed forcing order is $\lambda$-closed when every decreasing sequence $⟨p_{\xi }:\xi <\delta ⟩$ with $\delta <\lambda$ has a common lower bound:The chain condition for forcing isAn antichain in a forcing order consists of pairwise incompatible forcing conditions; incompatibility means having no common stronger extension. In particular, the ${\aleph }_1$-chain condition is the countable chain condition for forcing. These properties and their sequences or antichains are computed inside the ground model $M$.

Conversely, suppose $p\in G$ and $p{⊩}^{\ast }\sigma \in \tau$. The syntactic forcing relation says thatis dense below a forcing condition $p$. This is a set in $M$ by definability of forcing and axiom schema of separation. The dense-below generic meeting lemma gives $s\in G\cap D$: augment $D$ by all incompatible forcing conditions with $p$ to obtain a globally dense ground-model set, and use $p\in G$ to exclude the incompatible part.

Choose the witnessing $(\rho ,r)\in \tau$. Since $s\le r$ and $s\in G$, upward closure gives $r\in G$. The assumed equality truth lemma gives ${\sigma }^G={\rho }^G$, while $r\in G$ gives ${\rho }^G\in {\tau }^G$. Combining both directions,This completes the atomic membership truth lemma for forcing; no separate assumption of the membership truth lemma was made.

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$.

Use standard notation for forcing, so $q\le p$ means that $q$ is stronger. Let $\check{p}$ be the canonical forcing name for the ground-model condition $p$. DefineHere $q\perp p$ means that they are incompatible forcing conditions. The checks and their collection are formed by recursion and Axiom schema of replacement in $M$, and the displayed set is selected by axiom schema of separation, so this is a forcing name in $M$.

By evaluation of a forcing name,If $p\in G$, directedness of the generic filter gives a common stronger condition for $p$ and each $q\in G$, so $p$ is absent from this value.

Conversely, for fixed $p\in \mathbb{P}$ the setis a dense subset of a forcing order belonging to $M$. A condition incompatible with $p$ is already in it, and one compatible with $p$ has a common extension below $p$. Genericity supplies $q\in G\cap D_p$. If $p\notin G$, upward closure of $G$ rules out $q\le p$, hence $q\perp p$. ThereforeThis forcing name for the complement of a generic filter works without a separativity assumption on the order.

The two conventions reverse the order relation. In standard notation for forcing, $q\le p$ means that $q$ is stronger than $p$. Thus $p$ and $q$ are incompatible forcing conditions when there is no $r$ with $r\le p$ and $r\le q$, while $D\subseteq \mathbb{P}$ is a dense set whenIn Jerusalem notation for forcing, $p\le q$ means that $q$ is stronger than $p$. Incompatibility therefore means that there is no $r$ with $p\le r$ and $q\le r$, and density means