# CNF quantifier elimination

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?

• 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$. Nov 29 '18 at 15:58
• so if we rename the right most z to v we get: $\forall x \forall y \bigl [P(x,y)⇒\exists z [q(y,z) \land \lnot R(x,z)]\ \bigl ] \lor \forall v Q(x,y,v)$ and later substitute $\exists z$ with f(x,y) the CNF that we get is: $[\lnot P(x,y) \lor Q(y,f(x,y)) \lor q(x,y,v)] \land [\lnot P(x,y) \lor R(x,f(x,y) \lor Q(x,y,v) ]$ Nov 29 '18 at 16:20
• You have Q overloaded: is it bivariate or trivariate? Nov 29 '18 at 22:44
• In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $\forall x$ and $\forall y$ quantifiers ... in fact, they are free variables. Is that what you want? Nov 30 '18 at 3:55

## 2 Answers

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)]

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))$$

• (by the way, I am adding a set of parentheses to get the Q(x,y,z) what is the rule that allows to do that? Can I assume that sinsce in $\forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula? Nov 30 '18 at 11:48
• @JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem. Nov 30 '18 at 20:41