How to translate the following sentences into first order logic?

Question

I have the following facts that I would like to know if I correctly translated them to FOL.

1. All dogs howl at night.

   ∀x(Dog(x) -> Howl(x))

2. Anyone who has any cats will not have any mice.

   ∀x∀y(Cat(y) ∧ Have(x,y) -> ¬∃z (Mouse(z) ∧ Have (x,z)))

   or (would like to know if this other way is possible as well)

   ∀x∀y(Cat(y) ∧ Have(x,y) -> ∀z (Mouse(z) -> ¬Have (x,z)))

3. Light sleepers do not have anything which howls at night.

   ∀x(LS(x) -> ∀y (Have(x,y) -> ¬ Howl(y)))

4. Peter has either a cat or a dog.

   ∃x((Dog(x) ∨ Cat(x)) ∧ Have(Peter,x))

5. If Peter is a light sleeper, then Peter does not have any mice.

   LS(Peter) -> ∀y(Mouse(y) -> ¬Have(Peter, y))

Will these be correct translations?

Translations:

DOG(x): x is a dog

CAT(x): x is a cat

MOUSE(x): x is a mouse

HOWL(x): x howls at night

HAVE(x,y): x has y

LS(x): x is a light sleeper

Answer 1

Edit: The question was updated; this answer refers to the original posting.

---

You haven't specified the meanings of Howl, Have, etc. I have made the most charitable assumptions, but if I'm wrong you may need to make some changes (for instance, if "Howl" doesn't have "at night" baked in).

1. This is probably fine.
2. Your two options are logically equivalent, and they're logically equivalent to how I would translate it, but my personal preference would be for something like $\forall x\left((\exists y(\ldots))\to\ldots\right)$. Even though it's equivalent, the phrasing "has any cats" makes me think of an embedded $\exists y$.
3. Your answers are odd because the sentence says "have" but you don't use the $\mathrm{Have}(x,y)$ construction.
4. This is close, but your FOL form is false in a world with no cats at all, even though "Peter has either a cat or a dog" could still be true if he has a dog.
5. This is probably fine.