Logic: Find the prenex form of a formula I want to find the prenex form of the following formula:
$\forall x P(X) \rightarrow \neg (\forall xQ(x) \rightarrow \exists y R(y))$
I found:
$\forall x'  \forall y  \exists x (P(x) \rightarrow \neg (Q(x')\rightarrow R(y)))$
Can someone verify whether this is correct? And, also, how can I verify myself that this is the correct answer?
 A: First, your $\forall x P(X) \rightarrow \neg (\forall x(Q(x) \rightarrow \exists y R(y)$ has some missing parentheses ... I assume it is:
$\forall x P(X) \rightarrow \neg (\forall x Q(x) \rightarrow \exists y R(y))$
OK, the relevant Prenex Laws (where Q does not contain any free variable $x$) are:
1A. $Q \rightarrow \exists x P(x) \Leftrightarrow \exists x (Q \rightarrow P(x))$
1B. $Q \rightarrow \forall x P(x) \Leftrightarrow \forall x (Q \rightarrow P(x))$
1C. $\exists x P(x) \rightarrow Q \Leftrightarrow \forall x (P(x) \rightarrow Q)$
1D. $\forall x P(x) \rightarrow Q \Leftrightarrow \exists x (P(x) \rightarrow Q)$
And of course we have:
2A. $\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x) $
2B. $\neg \exists x P(x) \Leftrightarrow \forall x \neg P(x) $
2C. $\forall x P(x) \Leftrightarrow \forall x' P(x')$
2D. $\exists x P(x) \Leftrightarrow \exists x' P(x')$
So:
$\forall x P(X) \rightarrow \neg (\forall x Q(x) \rightarrow \exists y R(y)) \Leftrightarrow$ (2C)
$\forall x P(X) \rightarrow \neg (\forall x'Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1D)
$\forall x P(X) \rightarrow \neg \exists x'(Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1A)
$\forall x P(X) \rightarrow \neg \exists x' \exists y (Q(x') \rightarrow R(y)) \Leftrightarrow$ (2B * 2)
$\forall x P(X) \rightarrow \forall x' \forall y \neg (Q(x') \rightarrow R(y)) \Leftrightarrow$ (1B * 2)
$\forall x' \forall y(\forall x P(X) \rightarrow  \neg (Q(x') \rightarrow R(y))) \Leftrightarrow$ (1D)
$\forall x' \forall y \exists x( P(X) \rightarrow  \neg (Q(x') \rightarrow R(y)))$
So yes, if I place the parentheses correctly, then you are correct!
If, however, you meant:
$\forall x P(X) \rightarrow \neg \forall x (Q(x) \rightarrow \exists y R(y))$
then you get:
$\forall x P(X) \rightarrow \neg \forall x (Q(x) \rightarrow \exists y R(y)) \Leftrightarrow$ (2D)
$\forall x P(X) \rightarrow \neg \forall x' (Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1A)
$\forall x P(X) \rightarrow \neg \forall x' \exists y (Q(x') \rightarrow  R(y)) \Leftrightarrow$ (2A + 2B)
$\forall x P(X) \rightarrow \exists x' \forall y \neg (Q(x') \rightarrow  R(y)) \Leftrightarrow$ (1A + 1B)
$\exists x' \forall y (\forall x P(X) \rightarrow \neg (Q(x') \rightarrow  R(y))) \Leftrightarrow$ (1D)
$\exists x' \forall y \exists x( P(X) \rightarrow \neg (Q(x') \rightarrow  R(y))) $
A: Fast way:
$$\forall x ~Px \Rightarrow_1 \lnot \forall z~( Qz \Rightarrow_2 \exists y ~ Ry) $$
Count the number of $\lnot$s and $\Rightarrow$ that the quantifier is part of the condition of.  If it is odd, change the quantifier to the other kind.


*

*$\forall x$ is in the condition of $\Rightarrow_1$, so it gets changed

*$\forall z$ is inside the $\lnot$ and is not part of the condition of any implication, (it is part of the consequence of $\Rightarrow_1$, but consequences don't count), so it gets changed

*$\exists y$ is not part of the condition of any implications, it is in 1 $\lnot$, so it gets changed


So moving everything to the left and changing:
$$\exists x \exists z \forall y~(Px \Rightarrow \lnot (Qz \Rightarrow Ry))$$
You pull them out in a way that changes the order, which requires a more complicated approach.
For the updated question:
$$\forall x ~Px \Rightarrow \lnot (\forall z~ Qz \Rightarrow \exists y ~ Ry) $$


*

*$\forall x$ is part of 1 condition and 0 negations, flipped.

*$\forall z$ is part of 1 condition and 1 negation, not flipped

*$\exists y$ is part of 0 conditions and 1 negation, flipped


$$\exists x \forall z \forall y~(Px \Rightarrow \lnot (Qz \Rightarrow Ry)) $$
