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

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.