Existential clause of syntactic forcing (source code)

= Existential clause of syntactic forcing

For the usual recursive <syntactic forcing relation>, $p\Vdash^*\exists x\,\varphi(x)$ means that conditions $q\leq p$ forcing $\varphi(\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$.