CNF quantifier elimination

Question

Hello I have the following formula that I need to transform to a normal form required for the resolution rule. I understand that this from is a sum of OR's as in: $(V1 \lor V2 ) \land ( V3 \lor V4 ) )$

The formula:

$\forall x \forall y \bigl[P(x,y) \Rightarrow \exists z [Q(y,z] \land \lnot R(x,z)]\bigl] \lor \forall z Q(x,y,z)$

so, I use Skolem to substitute $\exists z$ with a constant A, then removed the universal quantifiers and following the general logic rules I came up with this:

$\bigl( \lnot P(x,y) \lor Q(y,A) \lor Q(x,y,z) \bigl) \land \bigl( \lnot P(x,y) \lor R(x,A) \lor Q(x,y,z) \bigl)$

Or should I first move the right most $\forall z$ to the left and then through skolem substitute the $\exists z$ with a function f(z) ?

$\bigl( \lnot P(x,y) \lor Q(y,f(z)) \lor Q(x,y,f(z)) \bigl) \land \bigl( \lnot P(x,y) \lor R(x,f(z)) \lor Q(x,y,f(z)) \bigl)$

Which solution is correct?

Answer 1

The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y. so if we rename the right most z to v we get: ∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v) and later substitute ∃z with f(x,y) the CNF that we get is [¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]

Answer 2

Neither is correct.

First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.

Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have

$\neg \exists P(x)$

you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get

$\forall x \ \neg P(x)$

and so you see that you shouldn't skolemize at all.

Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $\forall x \forall y$ which I believe is meant):

$\forall x \forall y ((P(x,y) \rightarrow \exists z (Q(y,z) \land \neg P(x,z))) \lor \forall z \ Q(x,y,z)) \Leftrightarrow$

$\forall x \forall y ((\neg P(x,y) \lor \exists z (Q(y,z) \land \neg P(x,z))) \lor \forall z \ Q(x,y,z)) \Leftrightarrow $

$\forall x \forall y (\exists z (\neg P(x,y) \lor (Q(y,z) \land \neg P(x,z))) \lor \forall z \ Q(x,y,z)) \Leftrightarrow$

$\forall x \forall y \exists z ((\neg P(x,y) \lor (Q(y,z) \land \neg P(x,z))) \lor \forall z \ Q(x,y,z)) \Leftrightarrow$

$\forall x \forall y \exists z ((\neg P(x,y) \lor (Q(y,z) \land \neg P(x,z))) \lor \forall w \ Q(x,y,w)) \Leftrightarrow$

$\forall x \forall y \exists z \forall w ((\neg P(x,y) \lor (Q(y,z) \land \neg P(x,z))) \lor Q(x,y,w)) \Leftrightarrow$

$\forall x \forall y \exists z \forall w (((\neg P(x,y) \lor Q(y,z)) \land (\neg P(x,y) \lor \neg P(x,z)) \lor Q(x,y,w)) \Leftrightarrow$

$\forall x \forall y \exists z \forall w ((\neg P(x,y) \lor Q(y,z) \lor Q(x,y,w)) \land (\neg P(x,y) \lor \neg P(x,z) \lor Q(x,y,w))$

So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.

OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:

$(\neg P(x,y) \lor Q(y,f(x,y)) \lor Q(x,y,w)) \land (\neg P(x,y) \lor \neg P(x,f(x,y)) \lor Q(x,y,w))$