1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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

$\endgroup$
6
  • $\begingroup$ thanks indeed a typo, can i try skolemize it and you tell if its correct ? btw i thought skolemization drops existential quantifiers ??? $\endgroup$
    – asddf
    Sep 23 '17 at 20:10
  • $\begingroup$ @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! $\endgroup$
    – Bram28
    Sep 23 '17 at 20:16
  • $\begingroup$ @asddf Just saw your skolemization: since the existentials come after the universal, you need to use functions. I'll add to my post ... $\endgroup$
    – Bram28
    Sep 23 '17 at 20:16
  • $\begingroup$ i edited it can you take a look ? $\endgroup$
    – asddf
    Sep 23 '17 at 20:18
  • 1
    $\begingroup$ @asddf You're welcome! P.s. use \Leftrightarrow for the logical equivalence symbol $\endgroup$
    – Bram28
    Sep 23 '17 at 20:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.