Monotonicity, density, and decision for forcing

Every atomic forcing clause persists to stronger conditions: in the subset clause the tested common extensions below q are a subset of those below p, and equality is the conjunction of two such requirements; membership restricts its tested extensions in the same way. For density closure of subset, given $⟨u,s⟩\in \sigma$ and $q\le p,s$, choose $a\le q$ forcing the subset, then apply its clause with that entry and common extension a. For equality, take a densely available condition forcing equality and perform this argument separately for each subset direction. For membership, given $q\le p$, first refine to a condition forcing membership and then refine once more to its equality/coefficient witness. These arguments prove atomic persistence and density closure.

If D is dense below p, the set $D^{\mathrm{\prime }}=\{q\in D:q\le p\}\cup \{q:q\perp p\}$ is dense in P. Indeed a condition compatible with p has a common extension, which can be refined into D; an incompatible condition already belongs to the second set. For $D,p\in M$, Separation makes $D^{\mathrm{\prime }}\in M$. A generic G containing p meets $D^{\mathrm{\prime }}$, and directedness prevents it from meeting its incompatible part. Thus it meets $D\cap \{q:q\le p\}$.

Induct on formula complexity for persistence and density closure. For conjunction, persistence holds for each conjunct by induction; if conjunction is forced densely, each conjunct is forced densely and hence at p by induction. For negation, no extension of p forcing $\psi$ implies the same at every stronger condition. If negation is forced densely below p, a hypothetical $q\le p$ forcing $\psi$ has an extension r forcing its negation; persistence of $\psi$ makes r force $\psi$, contradicting the negation clause at r itself.

For an existential, let $W=\{r:\mathrm{\exists }\sigma (r⊩\psi (\sigma ,\vec{\tau }))\}$. Forcing the existential means W is dense below p. It is then dense below every stronger condition, proving persistence. If conditions below p forcing the existential are dense below p, any $q\le p$ has a refinement a below which W is dense, and hence a further refinement in W. Thus W is dense below p, proving density closure. Together with step 2.1, this completes the induction.

Given any p, either some $q\le p$ forces $\phi$, or no such q exists and p forces $\mathrm{\neg }\phi$ by definition. This proves external decision density. When the parameters belong to M, Separation inside M instead forms the set decided by ${⊩}^M$; F1 does not identify that set with the external one for quantified formulas. No condition forces both $\phi$ and $\mathrm{\neg }\phi$, because p is one of its own extensions. All refinements used above are finitely many existential instantiations; no choice principle is used.