How do you bring quantifiers to the front of a formula? 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$?
 A: See Prenex normal form :

A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers (referred to as the prefix) followed by a quantifier-free part (referred to as the matrix).

Every formula in classical logic is equivalent to a formula in prenex normal form.


See Conversion to prenex form for the rules to be applied for the conversion.

We have :

$(α → ∀xβ) ↔ ∀x(α → β)$, provided that $x$ does not occur free in $\alpha$..

Applying it to your $F_1$ we get :

(*) --- $(∀xp(x) → ∀yq(y)) ↔ ∀y(∀xp(x) → q(y))$

because $y$ is not free in $∀xq(x)$.
Then we need :

$(∀xβ → α) ↔ ∃x(β → α)$, provided that $x$ is not free in $\alpha$ [you can find the proof of it in this post].

We have to apply it to (*) above to get :

$∀y(∀xp(x) → q(y)) ↔ ∀y∃x(p(x) → q(y))$, which is your $F_2$,

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 :

$∀y(\lnot ∀xp(x) \lor q(y))$.

But $\lnot \forall$ is equivalent to : $\exists \lnot$; thus we have :

$∀y(∃x \lnot p(x) \lor q(y))$

and thus :

$∀y∃x (\lnot p(x) \lor q(y))$,

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 :



$∀y∃x (p(x) \to q(y))$.



A: Imagine that $p(x)$ is true for some $x$'s and false for others, and similarly for $q(x)$.  Then $F_1$ is true, because the antecedent is false.  $F_3$ is false, because I can choose an $x_1$ that makes $p(x_1)$ true and an $x_2$ that makes $q(x_2)$ false.
