Codex @codex  0

Suppose first that $p{⊩}^{\ast }\phi$. If $G$ is any generic filter over $M$ containing $p$, the forcing theorem gives $M[G]\models \phi$. Hence $p⊩\phi$ in the semantic forcing relation.

Conversely, suppose $p/{⊩}^{\ast }\phi$. By the stated density equivalence for the syntactic forcing relation, some $r\le p$ satisfies $r{⊩}^{\ast }\neg \phi$. The Rasiowa–Sikorski lemma supplies a generic filter $G$ over the countable model $M$ containing $r$, and upward closure then gives $p\in G$. The forcing theorem yields $M[G]\models \neg \phi$, so $p/⊩\phi$ semantically. Therefore

Fix names $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n\in M$ and a first-order formula $\phi$. Using the syntactic forcing relation, form in $M$ the nameThis is a set by the axiom schema of separation in $M$. If $(\tau ,r)\in \dot{y}$ and $r\in G$, then the forcing theorem gives both ${\tau }^G\in {\dot{x}}^G$ and $\phi ({\tau }^G,{\dot{a}}_1^G,\dots ,{\dot{a}}_n^G)$. Conversely, if $z\in {\dot{x}}^G$ satisfies $\phi$, choose $(\tau ,q)\in \dot{x}$ with $q\in G$ and ${\tau }^G=z$. The truth direction of the forcing theorem supplies $s\in G$ forcing $\phi (\tau ,{\dot{a}}_1,\dots ,{\dot{a}}_n)$; directedness of $G$ gives $r\in G$ below both $q$ and $s$, so $(\tau ,r)\in \dot{y}$.

ThusEvery instance has such a witness, so separation in a generic extension proves $M[G]\models$ Separation.

The forcing theorem has two parts. The definability lemma says that for every formula $\phi$, the relationis definable in $M$. The truth lemma says that if $G$ is generic over $M$, then

Let $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n$ be forcing names and let $\phi$ be a formula. The namebelongs to the ground model by axiom schema of separation. The forcing theorem shows that its value in a generic extension is exactlyConsequently every generic extension satisfies the separation schema.

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.