Discrete Mathematics Quantified Statements - (with zombies!)

Does this sound right?
The original statement is:
All zombies eat brains.
Formally: ∀ zombies z, z eats brains.
Formal negation: ∃ a zombie z such that z does not eat brains.
Informal negation: Some zombies don't eat brains. (They're on a diet.)

Does that sound right? Did I miss anything?

The proper formation of the statement is:

∀z[ Zombie(z) => Eats_brains(z)]

or equivalently

∀z[ ~Zombie(z) V Eats_brains(z)]

So the formal negation is:

∃z[Zombie(z) Λ ~Eats_brains(z)]

or informally

There exists at least one "thing" z that is both a zombie and does not eat brains

or more informally

there's at least one zombie that doesn't eat brains.


Avoid "some zombies", it doesn't have a clear meaning.