# Turn $\exists z \forall y[p(y) \land r(z,y)] \to \exists y r(x,y)$ into CNF

Turn $\exists z \forall y[p(y) \land r(z,y)] \to \exists y r(x,y)$ into CNF.

What i tried: $\exists z \forall y[p(y) \land r(z,y)] \to \exists y r(x,y) \equiv \lnot(\exists z \forall y[p(y) \land r(z,y)]) \lor \exists y r(x,y) \equiv \forall z \lnot (\forall y [p(y) \land r(z,y)])\lor\exists yr(x,y) \equiv \forall z \exists y[\lnot p(y)\lor \lnot r(z,y)]\lor \exists yr(x,y) \equiv \forall z \exists y \exists l[\lnot p(y) \lor\lnot r(z,y)\lor r(x,l)]$

After skolemization: $\forall z [\lnot p(sk_1(z)) \lor\lnot r(z,sk_1(z))\lor r(x,sk_2(z))]$

And if i put l infront it would be $\forall z [\lnot p(sk_1(z)) \lor\lnot r(z,sk_1(z))\lor r(x,c_1)]$

Is it obligatory to skolemize for cnf ? Are my steps correct till now ?

Im sorry I used equiv for for logical equivalence i didnt find the symbol i should use.

The body of your formula is in CNF, but probably they want you to indeed skolemize and drop the universal quantifier.

Note that if you first pull out the second existential, you can avoid having to use one of the functions when skolemizing:

$\forall z \exists y[\lnot p(y)\lor \lnot r(z,y)]\lor \exists y \ r(x,y) \Leftrightarrow$

$\forall z \exists y[\lnot p(y)\lor \lnot r(z,y)]\lor \exists l \ r(x,l) \Leftrightarrow$

$\exists l (\forall z \exists y[\lnot p(y)\lor \lnot r(z,y)]\lor r(x,l))\Leftrightarrow$

$\exists l \forall z \exists y[\lnot p(y)\lor \lnot r(z,y)\lor r(x,l)]$

Skolemizing this, you get:

$\lnot p(f(z))\lor \lnot r(z,f(z))\lor r(x,c)$

• thanks indeed a typo, can i try skolemize it and you tell if its correct ? btw i thought skolemization drops existential quantifiers ??? Sep 23 '17 at 20:10
• @asddf Yes, you drop the existentials too, but you have to fill in constants or some function, while universals just get dropped without any changes ... sorry to confuse you! Sep 23 '17 at 20:16
• @asddf Just saw your skolemization: since the existentials come after the universal, you need to use functions. I'll add to my post ... Sep 23 '17 at 20:16
• i edited it can you take a look ? Sep 23 '17 at 20:18
• @asddf You're welcome! P.s. use \Leftrightarrow for the logical equivalence symbol Sep 23 '17 at 20:22