= Atomic membership truth lemma for forcing
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.
Back to article page
