Syntactic forcing relation ($p{⊩}^{\ast }\phi$)

The syntactic forcing relation is defined recursively inside the ground model from the ranks of forcing names and the logical complexity of $\phi$. The forcing theorem proves that it agrees with the semantic forcing relation.

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