If $M[G] \subseteq M[H]$ are forcing extensions, why is $M[H]$ a generic extension of $M[G]$?

Question

I know that, wlog, we may assume $G = H \cap A$ for some complete subalgebra $A$ of the complete Boolean algebra $B$ over which $H$ is $M$-generic.

Answer 1

Just for humor value, here's a poset-based proof (all the proofs I've seen have been Boolean algebra-based):

Let $G$ be $\mathbb{P}_1$-generic over $M$, and $H$ be $\mathbb{P}_2$-generic over $M$. Let $\nu$ be a $\mathbb{P}_2$-name such that $\nu[H]=G$.

We can define a subset $\mathbb{Q}$ of $\mathbb{P}_2$ as follows:

• $\mathbb{Q}_0=\{p\in\mathbb{P}_2: \forall q\in \mathbb{P}_1\setminus G, p\not\Vdash q\in G\}\cap \{p\in\mathbb{P}_2: \forall q\in G, p\not\Vdash q\not\in G\}$.

• $\mathbb{Q}_\lambda=\bigcap_{\alpha<\lambda}\mathbb{Q}_\alpha$ for $\lambda$ limit.

• $\mathbb{Q}_{\alpha+1}=\{p\in\mathbb{Q}_\alpha: \forall D\in M\text{ dense open subset of $\mathbb{P}_2$, $\exists p'\le p(p'\in\mathbb{Q}_{\alpha}\cap D)$}\}$.

• $\mathbb{Q}=\mathbb{Q}_{\vert\mathbb{P}\vert^+}$. Note that this is just $\bigcap_{\alpha\in ON}\mathbb{Q}_\alpha$, for cardinality reasons.

Basically, we take $\mathbb{P}_2$ and we "carve out" all the conditions that could force $\nu\not=G$. Note that this process takes place in $M[G]$.

It's now not hard to show that $H$ is $\mathbb{Q}$-generic over $M[G]$.

---

The construction of $\mathbb{Q}$ is a construction which I suspect has been introduced before, but which I haven't seen; see https://mathoverflow.net/questions/227937/reverse-engineer-forcing-am-i-reinventing-the-wheel.