# Translate the following sentence into conjunctive normal form

"Anyone who has cats as pets will not have mice": $$\forall x[\exists zHave(x,cat(z))]\rightarrow \forall y[\neg Have(x,mouse(y))]$$

I need to translate this into conjunctive normal form. So the first thing I do is eliminate the $\rightarrow$:

$$\forall x [\neg \exists z Have(x,cat(z))] \vee \forall y[\neg Have(x,mouse(y))]$$

Then we apply the negation:

$$\forall x[\forall z \neg Have(x,cat(z))] \vee \forall y[\neg Have(x,mouse(y))]$$

Then apply the Skolem function & drop universal quantifiers (?):

$$\neg Have(x,F(x)) \vee \neg Have(x, G(y))$$

So this last sentence is in conjunctive normal form, but I'm not sure if it means the same thing as the original sentence. The last sentence may read as "$x$ has a cat or $x$ has a mouse." Is this the same thing as "Anyone who has cats as pets will not have mice?" Are my steps correct?

• The $\exists y \neg Have(x,mouse(y))$ is translated as there is a mouse you don't have, not that you don't have a mouse. You need the negation on the outside, or a universal quantifier. Oct 21 '14 at 0:19
• @James Thank you. I fixed that. Is the resulting reduction correct now? Oct 21 '14 at 0:25
• No, there are still problems. In the first step, you have introduced a negation in front of the $\forall x$ and after it. There should only be one negation. I presume that the $\forall x$ is supposed to have widest scope, even though this isn't consistent with your brackets. Hence you need to drop the $\neg$ out front. Oct 21 '14 at 1:32
• Also, a less pressing, but still strange thing, is that you are using $cat(z)$ and $mouse(y)$ as functions, even though it would be more conventional to have relations representing the property of being a cat, and a mouse, respectively. Oct 21 '14 at 1:34
• @James I have tried to correct my mistakes. Does this look good now? Oct 21 '14 at 1:37

Ok, I decided to convert the comments into an answer. The sentence in English is "Anyone who has cats as pets will not have mice". This naturally translates as $$\forall x (\exists y(Cat(y) \land Have(x,y))\rightarrow \neg \exists z (Mouse(z) \land Have(x,z)))$$ remove $\rightarrow$

$$\forall x (\neg\exists y(Cat(y) \land Have(x,y))\lor \neg \exists z (Mouse(z) \land Have(x,z)))$$

move negations in

$$\forall x (\forall y(\neg Cat(y) \lor \neg Have(x,y))\lor \forall z (\neg Mouse(z) \lor \neg Have(x,z)))$$

Pull out quantifiers

$$\forall x,y,z (\neg Cat(y) \lor \neg Have(x,y) \lor \neg Mouse(z) \lor \neg Have(x,z))$$

Skolem function things (trivial step as there are no existentials). Drop universals

$$\neg Cat(y) \lor \neg Have(x,y) \lor \neg Mouse(z) \lor \neg Have(x,z)$$