I have formulas of the following kind $\exists y \forall z(\exists x \neg p(z,g(x)) \implies q(g(y),z))$
Now, does that mean $\exists y \forall z((\exists x \neg p(z,g(x))) \implies q(g(y),z))$ or does it mean $$\exists y \forall z((\exists x \neg p(z,g(x)) \implies q(g(y),z)))$$ i.e. what is with higher priority? The quantifier or the implication rule? Does the same thing applies to the universal quantifier?
I want to turn the formula to CNF, so I have to remove the implication first.
Another formula which I have to deal with the same problem is $$ \forall y \forall z(\exists x q(y,f(x)) \implies p(z,y))\&\forall x \forall y(p(x,y) \implies r(y)) $$
Again, is the turning of implication $A \implies B$ to $\neg A \lor B$ going to affect the quantifier or is the quantifier with a higher scope for the whole implication?
Thanks in advance!
$$\exists y \forall z(\exists x \ \neg p(z,g(x)) \implies q(g(y),z))$$
means:
$$\exists y \forall z((\exists x \ \neg p(z,g(x))) \implies q(g(y),z))$$
In other words, you don't need that set of parentheses around the existential in the second statement. Buit if you want to extend the scope of the $\forall$ to include the $\Rightarrow$, then you will need parentheses, like you do:
$$\exists y \forall z((\exists x \ \neg p(z,g(x)) \implies q(g(y),z)))$$
Anyway, your original statement works out to:
$$\exists y \forall z(\exists x \ \neg p(z,g(x)) \implies q(g(y),z))$$
which is equivalent to:
$$\exists y \forall z(\neg \exists x \ \neg p(z,g(x)) \lor q(g(y),z))$$
and thus to:
$$\exists y \forall z (\forall x \ p(z,g(x)) \lor q(g(y),z))$$
Which by a Prenex Law becomes:
$$\exists y \forall z \forall x ( p(z,g(x)) \lor q(g(y),z))$$