iterated forcing and composition

There is a function satisfying forcings are equivalent if one is dense in the other $f:P_{\alpha }*Q_{\alpha }\to P_{\alpha +1}$.

Proof

Let $f(⟨g,\widehat{q}⟩)=g\cup \{⟨\alpha ,\widehat{q}⟩\}$. This is obviously a member of $P_{\alpha +1}$, since it is a partial function from $\alpha +1$ (and if the domain of $g$ is less than $\alpha$ then so is the domain of $f(⟨g,\widehat{q}⟩)$), if then obviously $f(⟨g,\widehat{q}⟩)$ applied to $i$ satisfies the definition of iterated forcing (since $g$ does), and if $i=\alpha$ then the definition is satisfied since $\widehat{q}$ is a name in $P_i$ for a member of $Q_i$.

$f$ is order preserving, since if $⟨g_1,{\widehat{q}}_1⟩\le ⟨g_2,{\widehat{q}}_2⟩$, all the appropriate characteristics of a function carry over to the image, and $g_1\upharpoonright \alpha {⊩}_{P_i}{\widehat{q}}_1\le {\widehat{q}}_2$ (by the definition of $\le$ in $*$).

If $⟨g_1,{\widehat{q}}_1⟩$ and $⟨g_2,{\widehat{q}}_2⟩$ are incomparable then either $g_1$ and $g_2$ are incomparable, in which case whatever prevents them from being compared applies to their images as well, or ${\widehat{q}}_1$ and ${\widehat{q}}_2$ aren’t compared appropriately, in which case again this prevents the images from being compared.

Finally, let $g$ be any element of $P_{\alpha +1}$. Then $g\upharpoonright \alpha \in P_{\alpha }$. If $\alpha \notin \mathrm{dom}(g)$ then this is just $g$, and $f(⟨g,\widehat{q}⟩)\le g$ for any $\widehat{q}$. If $\alpha \in \mathrm{dom}(g)$ then $f(⟨g\upharpoonright \alpha ,g(\alpha )⟩)=g$. Hence $f[P_{\alpha }*Q_{\alpha }]$ is dense in $P_{\alpha +1}$, and so these are equivalent.