Does modal replacement hold in modal logic of forcing? Let $M$ be a countable model of set theory, and let $\mathbb{M}$ be the generic multiverse on $M$. $\mathbb{M}$ forms a Kripke model for modal logic with $\Diamond \phi$ being true at a world if $\phi$ holds in a forcing extension of that world. The logic in this model is known to be at least $S4.2$.
For $\phi$ in the first order language of set theory, let $\phi^\Diamond$ denote the formula that results by prepending each universal quantifier with a $\Box$ and each existential with a $\Diamond$.
Let $\Phi$ be an arbitrary instance of the replacement schema in the first order language of set theory. Does $\Phi^\Diamond$ hold in $\mathbb{M}$, considered as a Kripke model?
I have an argument that it does, but I'm not sure it's right. Here's a sketch:
Let $W$ be a world of $\mathbb{M}$ and suppose $\forall x \in a \Diamond \exists y \phi^\Diamond(x, y)$. We must show that there is a forcing extension of $W$ that contains a $b$ with $\Box \forall x \in a \Diamond \exists y \in b \phi^\Diamond(x, y)$. Since we can't add elements to sets by forcing, this reduces to showing that there is a $b$ in an extension of $W$ with $\forall x \in a \exists y \in b \Box \Diamond \phi^\Diamond(x, y)$. Since in $S4.2$, any formula of the form $\phi^\Diamond$ is provably equivalent to $\Box \phi^\Diamond$ and $\Diamond \phi^\Diamond$, this in turn reduces to showing $\forall x \in a \exists y \in b \phi^\Diamond(x, y)$. (See e.g. Linnebo, "Thin Objects", Lemma 3.1.)
By assumption, for each $x$ we have an extension $W[G_x]$ with $W[G_x] \models \phi^\Diamond(x, y)$, and by the just cited lemma we also have $W[G_x] \models \Box \phi^\Diamond(x,y)$, so any forcing extension of $W[G_x]$ will similarly satisfy $\phi^\Diamond(x,y)$. Since $M$ is countable we can enumerate the $G_x$s as $\langle G_n : n \in \omega \rangle$. Identify $G_n$ with the product forcing $G_1 \times .... \times G_n$. Since we are dealing only with $x$ in some fixed $a$ in $W$, the cardinality of these forcings $G_n$ is bounded in $W$, and hence (by Fuchs Hamkins & Reitz, 'set theoretic geology', Theorem 39) there is an extension $W[H]$ of all the $W[G_n]$s. This $W[H]$ satisfies $\forall x \in a \exists y \phi^\Diamond(x, y)$, so in $W[H]$ we have $\exists b \forall x \in a \exists y \in b \phi^\Diamond(x, y)$, as req'd.
I'm not super confident in this reasoning, or that the result holds. Any direction is much appreciated.
 A: I'm not sure about the argument you give, but here's how I'd be tempted to go about proving it.
First, we establish a translation between the modalised and unmodalised languages of set theory (where $[x]$ is the cannonical name of $x$ (I forget the actual notation)).

*

*($x\in y)^* = x\in y$

*$^*$ commutes with conjunction and negation

*$(\Diamond\exists x\phi^\Diamond(x, \vec{y}))^* = \exists P\exists p\in P(p\Vdash \exists x\phi^*(x, \vec{[y]})) $
Then we can prove:
$\forall \vec{x}\in w(w\vDash \phi^\Diamond \leftrightarrow w\vDash \phi^*)$
Now, assume that in $w$ for all $y\in x$, $w\vDash \Diamond\exists z\phi^\Diamond(z, y)$. By the lemma, that means for all $y\in x$, there is some $P_y$ and $p_y\in P_y$ and name $z_y$ in $w$ such that $w\vDash p_y\Vdash  \phi^*(z_y, [y])$. So, applying Replacement in $w$, we can assume they form a set. Now, $\langle p_y,..., p_{y'},...\rangle$ will be a condition in $P_y\times...\times P_{y'}...$. Let $G_y\times...\times G_{y'}...$ be a generic for this partial order containing that condition. Then it will be the case that:
$w[G_y]\vDash \phi^*(z_y^{G_y}, y)$
and so:
$w[G_y]\vDash \phi^\Diamond(z_y^{G_y}, y)$
And since $w[G]$ is a forcing extension of $w[G_y]$ (by the product forcing lemma) and we have S4.2:
$w[G]\vDash \phi^\Diamond(z_y^{G}, y)$
Finally, the set $t$ of names $z_y...$ etc in $w$ will be in $w[G]$ and thus so will $t^{G}$. So:
$w[G]\vDash \forall y\in x \exists z\in t^{G}\phi^\Diamond(z, y)$
So:
$w\vDash \Diamond\exists t \Box\forall y\in x\Diamond\exists z\in t \phi^\Diamond(z, y)$
