= Solution
Use <standard notation for forcing>: $q\leq p$ means that $q$ is stronger. A <generic filter> is nonempty, upward closed and downward directed, and meets every <dense subset of a forcing order> in the ground model. Names below are <forcing names> in $M$, with pairs ordered as $(\text{name},\text{condition})$.
The <semantic forcing relation> is
$$
\boxed{p\Vdash\varphi(\tau_1,\ldots,\tau_n)\ \Longleftrightarrow\ \text{for every }M\text{-generic }K\ni p,\ M[K]\models\varphi(\tau_1^K,\ldots,\tau_n^K).}
$$
Here $\tau^K=\operatorname{val}(\tau,K)$ is the <evaluation of a forcing name>. Countability of $M$ supplies such <generic filters> through every condition by the <Rasiowa–Sikorski lemma>.
Define the <syntactic forcing relation> by mutual well-founded recursion on the <forcing names> for the atomic cases, then induction on the <first-order formula>. Its membership clause is
$$
p\Vdash^*\sigma\in\tau\ \Longleftrightarrow\ \forall q\leq p\ \exists s\leq q\ \exists(\rho,r)\in\tau\ (s\leq r\ \land\ s\Vdash^*\sigma=\rho).
$$
For equality, first abbreviate
$$
p\Vdash^*\sigma\subseteq\tau\ \Longleftrightarrow\ \forall(\rho,r)\in\sigma\ \forall q\,(q\leq p\land q\leq r\Rightarrow q\Vdash^*\rho\in\tau),
$$
and set $p\Vdash^*\sigma=\tau$ exactly when both inclusions hold. Each recursive call lowers the rank of at least one <forcing name> without raising the other. This makes the mutual recursion well-founded.
For a basis of connectives consisting of <logical conjunction>, <negation> and existential quantification, the remaining clauses are
$$
\begin{aligned}
p\Vdash^*(\varphi\land\psi)&\Longleftrightarrow(p\Vdash^*\varphi\ \land\ p\Vdash^*\psi),\\
p\Vdash^*\neg\varphi&\Longleftrightarrow\text{no }q\leq p\text{ satisfies }q\Vdash^*\varphi,\\
p\Vdash^*\exists v\,\varphi(v)&\Longleftrightarrow\forall q\leq p\ \exists s\leq q\ \exists\rho\in M^{\mathbb P}\ (s\Vdash^*\varphi(\rho)).
\end{aligned}
$$
The last line is the <existential clause of syntactic forcing>; witnesses need only occur densely, rather than be forced by $p$ itself with one preselected name. Other connectives are defined by logical abbreviations. The recursion gives a definable relation inside $M$ for each fixed <first-order formula>, with quantification over the class of its names. If $\mathbb P$ has no greatest element, use <canonical forcing names> $\check a=\{(\check b,p):b\in a,\ p\in\mathbb P\}$, which still evaluate to $a$. It also proves monotonicity: strengthening a condition preserves what it forces. The <forcing theorem> identifies the two relations and supplies the truth lemma.
Back to article page
