Is my conversion of $\forall x(P(x)\rightarrow\forall yQ(y))$ to prenex normal form correct?

Question

I convert using the following equivalences.

1. $\forall x(P(x)\rightarrow\forall yQ(y))$
2. $\forall x\neg(P(x)\land\exists y\neg Q(y))$
3. $\forall x\neg\exists y(P(x)\land\neg Q(y))$
4. $\forall x\forall y(P(x)\rightarrow Q(y))$

Is this correct formally?

Answer 1

Yes, they are all equivalent, and the last one is in Prenex Normal form.

Now, I don;t know if you were asked to do this transformation step-by-step, using elementary equivalence laws, but if so, then I would say to break it up a little more:

1. $\forall x(P(x)\rightarrow\forall yQ(y)) \overset{\text{Implication}}{\Leftrightarrow}$
2. $\forall x\neg(P(x)\land \neg \forall y Q(y)) \overset{\text{Quantifier Negation}}{\Leftrightarrow}$
3. $\forall x\neg(P(x)\land\exists y\neg Q(y)) \overset{\text{Prenex Law}}{\Leftrightarrow}$
4. $\forall x\neg\exists y(P(x)\land\neg Q(y))\overset{\text{Quantifier Negation}}{\Leftrightarrow}$
5. $\forall x\forall y\neg(P(x)\land\neg Q(y))\overset{\text{Implication}}{\Leftrightarrow}$
6. $\forall x\forall y(P(x)\rightarrow Q(y))$

Also note that one of the Prenex Laws is:

$\forall x(Q\rightarrow P(x)) \Leftrightarrow (Q\rightarrow \forall x \ P(x)) $

And with that Prenex Law, the desired transformation is just 1 step:

1. $\forall x(P(x)\rightarrow\forall yQ(y)) \overset{\text{Prenex Law !}}{\Leftrightarrow}$
2. $\forall x\forall y(P(x)\rightarrow Q(y))$