Prove that John is not a light sleeper

Question

Define each sentence in terms of CNF. Prove that John is not a light sleeper.

(1): All wolves howl.
(2): Anyone who has casts as pets will not have mice.
(3): Anyone who is a light sleeper can't live near anything that howls.
(4): John either has cats or lives near wolves.
(5): If John is a light sleeper, John has mice.

$Wolf(x): x$ is a wolf

$Howl(x): x$ howls

$Have(x,y): x$ has y

$Cat(x): x$ is a cat

$Mouse(x): x$ is a mouse

$LS(x): x$ is a light sleeper

$Live(x,y): x$ lives near y

I began by writing each sentence in terms of quantifiers:

(1): $\forall x(Wolf(x)\rightarrow Howl(x))$

(2): $\forall x\forall y\forall z(Have(x,Cat(y)) \rightarrow \neg Have(x,Mouse(z))$

(3): $\forall x \forall y((\neg LS(x) \wedge Howls(y)) \rightarrow \neg Live(x,y))$

(4): $\exists x, \exists y(Have(Frank,Cat(x))\vee Live(Frank,Wolf(y)))$

(5): $\exists (LS(Frank)\rightarrow Have(Frank,Mouse(x)))$

So my first question is whether these quantifier sentences are correct. My second question is how we can take these to CNF. I understand that something like $x\rightarrow y$ can turn into $\neg x \vee \neg y$, but I don't see how we can eliminate quantifiers altogether. Can someone perhaps show me how this is done with one of the quantifier sentences?

Answer 1

Hints :

Let P denotes an animal, and A denotes a person:

(1): $P$ is a wolf $\implies$ P howl.

(2): $A$ has cats as pets $\implies $ A don't have mice.

(3): $A$ is a light sleeper $\implies$ $A$ don't live near anything that howls.

(4): John has cats XOR John lives near wolves. [ this one can be expressed as : (John has cats AND John doesn't live near wolves) OR (John don't have cats AND John lives near wolves ]

(5): John is a light sleeper $\implies$ John has mice.

begin with (5) and do a proof by contradiction.

Update :

by contradiction let us suppose that John is a light sleeper. by (5) this implies that John has mice. by (2) [ its Contraposition] this implies that John don't have cats. by (4) this implies that John lives near wolves. by the (3) [ its Contraposition] AND (1) : this implies that John is not a light sleeper ( and this is the contradiction because we supposed that John is a light sleeper)

Hence, John is not a light sleeper