# First order logic without existential quantifier, does the position of the "forall" matter?

I am considering first order logic without existential quantification (i.e. with $$\forall$$ as the only quantifiers). Given an arbitrary formula, would moving all the $$\forall$$ to the "front" of the formula affect the truth value of this formula? For example, are these two formulas below equivalent (the one below produced by moving all the universal quantifications to the front)? Are all such first order logic formulas (those with $$\forall$$ as the only quantifiers) equivalent when rewritten this way? How about in higher order logic?

$$(\forall x,P(x)) \to (\forall y,Q(y)) \\ (\forall x, \forall y, P(x) \to Q(y))$$

• If your first order logic has classical negation, then you can simply define $\exists$ as $\neg\forall\neg$. Apr 14 '19 at 0:46

No, those are not equivalent. Here are the relevant Prenex equivalence laws that do hold:

Prenex Laws

where $$\psi$$ is a formula that does not contain $$x$$ as a free variable:

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

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

$$\forall x \ \varphi(x) \to \psi \Leftrightarrow \exists x (\varphi(x) \to \psi)$$

$$\exists x \ \varphi(x) \to \psi \ \Leftrightarrow \forall x (\varphi(x) \to \psi)$$

(in other words, if you pull a quantifier outside a conditional, then if the quantifier is in the consequent, then the quantifier stays the same, but if it is in the antecedent, then it swaps to the other quantifier)

As such, we have that:

$$\forall x \ P(x) \to \forall y \ Q(y) \Leftrightarrow \exists x \forall y (P(x) \to Q(y))$$

And we also have that:

$$\exists x \ P(x) \to \forall y \ Q(y) \Leftrightarrow \forall x \forall y (P(x) \to Q(y))$$

but we do not have:

$$\forall x \ P(x) \to \forall y \ Q(y) \Leftrightarrow \forall x \forall y (P(x) \to Q(y))$$