= Solution
We prove <mutual genericity for product forcing>. Let $D\in M[G_0]$ be a dense <subset> of $\mathbb Q$, and take a <forcing name> $\dot D\in M$ evaluating to $D$. By the <forcing theorem>, some $p_0\in G_0$ forces that $\dot D$ is a dense <subset> of the <canonical forcing name> for $\mathbb Q$.
In $M$ define
$$
E=\{(p,q):p\perp p_0\}\ \cup\ \{(p,q):p\leq p_0\text{ and }p\Vdash\check q\in\dot D\}.
$$
This <set> is dense in the <product forcing> order. Given $(p,q)$, the incompatible case is immediate. Otherwise first strengthen $p$ below $p_0$. The forced density assertion and the <existential clause of syntactic forcing> supply a further $r\leq p,p_0$ and a ground-model $q'\leq q$ with $r\Vdash\check q'\in\dot D$. To justify choosing a ground-model $q'$, a name forced to lie in $\check{\mathbb Q}$ can densely be made equal to some $\check q'$ by the atomic membership clause; strengthen to that equality and use the forced order comparison. Thus $(r,q')\in E$ lies below $(p,q)$.
The <generic filter> $H$ meets $E$. It cannot meet the first part, because its first projection contains $p_0$ and is directed. Hence there is $(p,q)\in H$ with $p\in G_0$ and $p\Vdash\check q\in\dot D$. Soundness of the <forcing theorem> gives $q\in D$, and the projection gives $q\in G_1$. Since every such $D$ is met,
$$
\boxed{G_1\text{ is }\mathbb Q\text{-generic over }M[G_0].}
$$
This establishes the stronger property, rather than merely meeting dense ground-model <subsets>.
Back to article page
