Should $\to$-elimination always have precedence over $\lnot$-elimination when transforming formulas to Prenex CNF?

Question

I'm currently learning the resolution method of proof and before it can be applied we need to transform a FOL formula into prenex, then skolemise it, then transform it to CNF, correct? I encountered a doubt when converting the following formula to CFN:

1) $\forall x \forall y ((H(x,y) \land C(y)) \to \lnot\exists z(H(x,z)\land Mouse(z)))$

Now, if I use $\to$-elimination before $\lnot$-elimination, I'll get the following transformation:

2) $\forall x \forall y (\lnot(H(x,y) \land C(y)) \lor \lnot\lnot\exists z(H(x,z)\land Mouse(z)))$

forcing me to convert $\lnot \lnot \exists z$ to $\exists z$

and get the following formula after $\lnot$-elimination:

3) $\forall x \forall y ((\lnot H(x,y) \lor \lnot C(y)) \lor \exists z(\lnot H(x,z)\lor \lnot Mouse(z)))$

And, after moving quantifiers to the front:

4) $\forall x \forall y \exists z ((\lnot H(x,y) \lor \lnot C(y)) \lor \lnot H(x,z)\lor \lnot Mouse(z)))$

Which will inevitably force me to skolemize the existential quantifier and finally arrive at:

5) $\forall x \forall y ((\lnot H(x,y) \lor \lnot C(y)) \lor \lnot H(x,f(x,y)))\lor \lnot Mouse(f(x,y))))$

Now, this is where my doubt comes into play. Had I used $\lnot$-elimination before $\to$-elimination -between 1) and 2)-, I'd have arrived at:

2*) $\forall x \forall y (\lnot(H(x,y) \land C(y)) \lor \forall z \lnot(H(x,z)\land Mouse(z)))$

By doing so, I wouldn't have to skolemize the existential quantifier away and would not have a skolem-function in my result. My question is: can I save myself the hassle of skolemising the existential quantifier in this way or will I run into trouble later on?

Thank you for your time.

Answer 1

1) $\forall x \forall y ((H(x,y) \land C(y)) \to \lnot\exists z(H(x,z)\land Mouse(z)))$

Now, if I use $\to$-elimination before $\lnot$-elimination, I'll get the following transformation:

2) $\forall x \forall y (\lnot(H(x,y) \land C(y)) \lor \lnot\lnot\exists z(H(x,z)\land Mouse(z)))$

No, you don't. You get:

$\forall x \forall y (\lnot(H(x,y) \land C(y)) \lor \lnot\exists z(H(x,z)\land Mouse(z)))$

and thus:

$\forall x \forall y (\lnot(H(x,y) \land C(y)) \lor \forall z \neg (H(x,z)\land Mouse(z)))$

and thus you don't get an existential to skolemise that way either.

In general, when you put a statement in prenex, the nature of the quantifiers will be forced. That is, you will not be able to get a different quantifier depending on the order in which you perform the steps. So, the fact that you got $\forall x \forall y \exists z ...$ one way, but $\forall x \forall y \forall z ...$ thew other way, immediately means that something went wrong.

However, what can happen, is that the order of the quantifiers can change. That is, doing steps in one order, you may get $\forall x \exists y...$, and doing it a different way, you might get $\exists y \forall x...$, and in that case doing it the second way avoids you having to introduce a function when skolemising.