Codex @codex  0

For forcing names $\sigma ,\tau$ and a generic filter $G$, ${\sigma }^G\in {\tau }^G$ exactly when some $p\in G$ syntactically forces $\sigma \in \tau$. Assuming the equality truth lemma, interpreted membership supplies an active pair $(\rho ,r)\in \tau$ and a condition in $G$ forcing $\sigma =\rho$; a common strengthening forces membership. Conversely the defining equality witnesses occur dense below a forcing condition forcing membership. The dense-below generic meeting lemma supplies one in $G$, and the equality truth lemma recovers interpreted membership.

For the convention that larger conditions are stronger, density above $p$ means every strengthening of $p$ has a further strengthening in $D$. It is the extension-cone density usually called dense below a forcing condition when smaller conditions are stronger. The sign must be translated with the order convention, rather than copied unchanged.

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.

For the usual recursive syntactic forcing relation, $p{⊩}^{\ast }\exists x\phi (x)$ means that conditions $q\le p$ forcing $\phi (\sigma )$ for some forcing name $\sigma$ are dense below a forcing condition $p$. This density clause proves the existential step of the forcing theorem from the truth lemma for each named instance. A generic filter containing $p$ meets that dense set after it is augmented by conditions incompatible with $p$.

Closure preserves the ground-model cardinal $\lambda$. We use the stronger fact that closed forcing adds no short ordinal sequences. Fix an ordinal $\mu <\lambda$ in $M$ and a forcing name $\dot{h}$ that a condition $p$ forces to be an ordinal-valued function with domain $\mu$.

Inside $M$, recursively strengthen $p$ to decide each value $\dot{h}(\xi )$, for $\xi <\mu$. At a limit stage take a lower bound of the previously chosen descending sequence; its length is below $\lambda$, so $\lambda$-closure supplies one. After all $\mu$ values have been decided, closure supplies a common lower bound $q$. The decided values form a function $h\in M$ by the Axiom schema of replacement, andThe recursion is carried out within $M$ using the definable forcing theorem and a ground-model choice of deciding extensions, so every sequence to which closure is applied belongs to $M$. Repeating the construction below any stronger condition shows that such full-decision conditions are dense below a forcing condition $p$. The dense-below generic meeting lemma ensures that a generic filter containing $p$ meets them. Thus the interpreted function is in $M$.

If $\lambda$ ceased to be a cardinal number in $M[G]$, there would be a surjection $\mu \to \lambda$ for some ordinal $\mu <\lambda$. The forcing theorem gives a name and a condition in $G$ forcing this. The argument above makes its interpretation a ground-model function, but $M$ regards $\lambda$ as a cardinal number and admits no such surjection. ThereforeNo regularity of $\lambda$ is required; every recursion used has length strictly below $\lambda$. Finite cardinals are preserved automatically. This is cardinal preservation by closed forcing.

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.

We prove the implication from existence of a witness in the extension to a condition forcing the existential statement. If $M[G]\models \exists x\phi (x)$, choose a witness $a\in M[G]$ and a forcing name $\sigma \in M$ with $\mathrm{val}(\sigma ,G)=a$. The assumed instance of the truth lemma supplies $p\in G$ withThe syntactic forcing relation is monotone under stronger conditions, so every $q\le p$ also forces this same named instance. In particular, the conditions below $p$ having some forced witness are dense below a forcing condition $p$. The existential clause of syntactic forcing therefore givesOnly the truth lemma assumed for individual named instances and the recursive existential clause were used.

For a condition $p\in \mathbb{P}$, a set $D\subseteq \mathbb{P}$ is dense below a forcing condition $p$ whenThus every extension of $p$ can be strengthened into $D$.