I meet the following formula:
$$(\exists xAx\rightarrow\exists yBy)\rightarrow(\exists x\Box Ax\rightarrow\exists y\Box By)$$
I wonder what amounts to a prenex form of this formula, that is, putting all quantifiers in front of a quantifier-free formula.
Following the prenex rules for implication, I obtain the following:
$$\exists y\forall x(Ax\rightarrow By)\rightarrow\exists y\forall x(\Box Ax\rightarrow\Box By)$$
But now, $x$ and $y$ occur in both formulas. I don't know how to proceed. Can anyone help?
Here's one way to do it, step by step.
$$ (\exists x A x \to \exists y B y) \to (\exists x \square A x \to \exists y \square B y) $$
replace $x \to y $ with $(\lnot x) \lor y$.
$$ (\exists x A x \not\to \exists y B y) \lor (\forall x \lozenge \lnot A x \lor \exists y \square B y ) $$
Replace $x \not\to y$ with $x \land \lnot y$.
$$ (\exists x A x \land \lnot \exists y B y) \lor \forall x \lozenge \lnot A x \lor \exists y \square B y $$
Move $\lnot$ inside the quantifier.
$$ (\exists x A x \land \forall y \lnot B y) \lor \forall x \lozenge \lnot A x \lor \exists y \square B y $$
Rename the variables so that no bound variables have the same name.
$$ (\exists z A z \land \forall w \lnot B w) \lor \forall x \lozenge \lnot A x \lor \exists y \square B y $$
None of the variables are shared between multiple subexpressions, so we can extract them in whatever order we want.
$$ \exists z \mathop. \exists y \mathop. \forall w \mathop. \forall x \mathop. (Az \land \lnot B w) \lor \lozenge \lnot A x \lor \square B y $$