Quantifier order for prenex normal form

Question

$\exists x R(x) \land \forall y S(y)$ is this equivalent to $\exists x \forall y (R(x) \land S(y))$ as well as $\forall y \exists x (R(x) \land S(y))$?

Is there a rule for the order of pulling out quantifiers?

Answer 1

The rule is that you can pull out a quantifier when the term that gets included into its new scope does not have the variable that that quantifier quantifies as a free variable. Formally:

Prenex Laws

Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:

$ \forall x \ \varphi \land \psi \Leftrightarrow \forall x (\varphi \land \psi)$

$ \exists x \ \varphi \land \psi \Leftrightarrow \exists x (\varphi \land \psi)$

As such, you can pull out the existential first, and then the universal, as well as in the other order.

That is:

$\exists x \ R(x) \land \forall y \ S(y) \Leftrightarrow$

$\exists x (R(x) \land \forall y \ S(y)) \Leftrightarrow$

$\exists x \forall y (R(x) \land S(y))$

But also:

$\exists x \ R(x) \land \forall y \ S(y) \Leftrightarrow$

$\forall y (\exists x (R(x) \land S(y)) \Leftrightarrow$

$\forall y \exists x (R(x) \land S(y))$

All equivalences used here follow the general law.

So yes, these are all equivalent.