I've recently seen
\begin{align} F_1 &= \forall x p(x) \rightarrow \forall x q(x)\\ F_2 &= \forall x_2 \exists x_1 (p(x_1) \rightarrow q(x_2))\\ F_1 &= F_2 \end{align}
Why is that the case?
Can you read the first part of the equation as
If p is true for all x, then q is true for all x.
? Why isn't it $F_3 = \forall x_1 \forall x_2 (p(x_1) \rightarrow q(x_2)) = F_1$? Is there a model for $F_1$ which is not a model of $F_3$?
See Prenex normal form :
See Conversion to prenex form for the rules to be applied for the conversion.
We have :
Applying it to your $F_1$ we get :
because $y$ is not free in $∀xq(x)$.
Then we need :
We have to apply it to (*) above to get :
due to the fact that $x$ is not free in $q(x)$.
We can use this "intuitive" argument to convince ourselves of the reason why in $∀y(∀xp(x) → q(y))$ the "inner" universal quantifier "switch" to an existential one when it is "moved outside".
Consider $∀y(∀xp(x) → q(y))$ and apply the tautological equivalence : $(p \to q) \leftrightarrow (\lnot p \lor q)$ to get :
But $\lnot \forall$ is equivalent to : $\exists \lnot$; thus we have :
and thus :
due to the fact that $\exists$ "distribute" over $\lor$ and that $x$ is not free in $q(y)$.
Now "reverse" the tautological equivalence above and we finally have :