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

Question

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.

Answer 1

Your steps are all correct!

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