Pre-nex normal form. Correct way to distribute negations among quantifiers

Question

Start point:

$$(¬∀x P(x) ∨ ¬∀y Q(y)) → ¬∃x G(x)$$

Implication to Disjunction (DeMorgans Laws):

$$¬(¬∀x P(x) ∨ ¬∀y Q(y)) ∨ ¬∃x G(x)$$

Now I am at the point where I need to move in the negations to precede the quantifiers but there are two ways I can see that i can do this to get a step closer to Prenex normal form (PNF)

1) Before distributing negations, I can deal with the negations already preceding the universal quantifiers so they precede the propositions ($P$ and $Q$) like so...

$$¬(∃x ¬P(x) ∨ ∃y ¬Q(y)) ∨ ¬∃x G(x)$$

At which point, I can THEN move the negations into the brackets to get..

$$(¬∃x ¬P(x) ∧ ¬∃y ¬Q(y)) ∨ ¬∃x G(x)$$

OR

I can move the furthermost negations in to precede the universal quantifiers, like so...

$$(¬¬∀x P(x) ∧ ¬¬∀y Q(y)) ∨ ¬∃x G(x)$$

and then I can eliminate the double negation...

$$(∀x P(x) ∧ ∀y Q(y)) ∨ ¬∃x G(x)$$

As you can see, this has resulted in two VERY different formulas and I don't want to go any further while i'm still in two minds about this step.

Therefore, my question is, which is the correct way to go about rewriting this formula (to this stage at least) Do I do one step before another or have I missed a step completely

Thanks in advance

Answer 1

I'll take it from your second option which is more handy.

Note that $$(\forall xP(x)\land \forall yQ(y))\lor \neg \exists xG(x)$$ and $$(\forall xP(x)\land \forall yQ(y))\lor \forall z\neg G(z)$$

are equivalent. (Change of variable is the crux of it all).

Also note that $\forall yQ(y)\iff \forall x\forall yQ(y)$ so the above statement is equivalent to $$\forall x(P(x)\land \forall yQ(y))\lor \forall z\neg G(z).$$

The same idea applied to the other predicates ultimately yields $$\forall x\forall y\forall z((P(x)\land Q(y))\lor \neg G(z)).$$

Answer 2

Both results are equivalent! Indeed, if you take your first result and move the negations through the quantifiers, we obtain the second result: \begin{align*} (\neg \exists x \, \neg P(x) \land \neg \exists y \, \neg Q(y)) \lor \neg \exists x \, G(x) &\iff (\forall x \, \neg\neg P(x) \land \forall y \, \neg\neg Q(y)) \lor \neg \exists x \, G(x) \\ &\iff (\forall x \, P(x) \land \forall y \, Q(y)) \lor \neg \exists x \, G(x) \\ \end{align*}