Artificial intelligent assistant

Quantifier order for prenex normal form $\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?

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.

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy 01f20eef44016ab5b223cc6331a1492b