Conversion of formula in Prenex Normal Form

Question

Let we have a formula $\psi = \forall x (P(x) \vee \forall y Q(y,x))$. Is the formula equivalent to $\psi' = \forall x \forall y (P(x) \vee Q(y, x))$ in Prenex Normal Form. If so, What are the rules that are being used while pulling the quantifier $\forall y$.

Here again with a slight change in the above formula :

Let we have a formula $\phi = \forall x (P(x) \wedge \forall y Q(y,x))$. Is the formula equivalent to $\phi' = \forall x \forall y (P(x) \wedge Q(y, x))$ in Prenex Normal Form. If so, What are the rules that are being used while pulling the quantifier $\forall y$.

Answer 1

The rules for producing a PNF are :

$(\forall x\phi) \land \psi$ is equivalent to $\forall x(\phi \land \psi)$

and

$(\forall x\phi )\lor \psi$ is equivalent to $\forall x(\phi \lor \psi )$,

under the condition that $x$ does not appear as a free variable in $\psi$ (and similar for the existential quantifier).

Thus, considering $\psi = ∀x(P(x) ∨ ∀yQ(y,x))$, we can "pull out" the $∀y$ quantifier using the second rule above, because there is no $y$ variable in the $P(x)$ subformula, getting the equivalent :

$\psi' = ∀x∀y(P(x) ∨ Q(y,x))$.

The same for $\phi$ and the equivalent $\phi'$, using the first rule above.