I'm learning about the prenex normal form right now and I'm having trouble getting the following formula in prenex form:
$\forall q (\exists x G(x,q) \longleftrightarrow \exists x L(x,q))$
I understand that I first have to rewrite the double arrow, then work out the negations, then rename the variables and finally move the quantifiers to the front.
If I did it right, the first three steps would give me this:
$\forall q ((\exists x G(x,q) \wedge \exists y L(y,q)) \vee (\forall z \neg G(z,q) \wedge \forall w \neg L(w,q)) $
But what I can't figure out is how to move the quantifiers to the front. I think that the two existential quantifiers can be moved to the front just like that, but what about the two universal ones? Do I have to maintain the order of them? If so, can I just write Ex Ey Az Aw, or will the universal quantifiers be left out and their variables become constants?
I would appreciate it if anybody could give me a hand.
Best Answer
Yes, you have a choice here. Picking a smaller example, the formula $\forall x(Px) \lor \exists y(Qy)$ has two different prenex normal forms: $$ \forall x\exists y(Px \lor Qy) \qquad\qquad \exists y\forall x(Px \lor Qy) $$
Usually $\forall x\exists y$ and $\exists y\forall x$ are not interchangeable, but in this particular example, the two prenex normal forms are actually logically equivalent, due to the special structure of the formula under the quantifiers.
In practice you would usually try to choose the one of $\forall x\exists y$ or $\exists y\forall x$ that results in fewest changes between $\exists$ and $\forall$ in the final prenex form -- but that's just because such a formula will usually be more convenient to continue working with afterwards, not because the other choice would be incorrect.