Which quantifier to include while converting implication to disjunction Given a statement: Anything anyone eats and isn't killed by is food,
I formed a predicate for it like:
$$ \forall x \forall y ~ \operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y) \implies \operatorname{food}(y). $$
Now I want to convert this well formed formula to clause form, so I want to convert the implication to disjunction, but I don't understand which quantifier to include in negation or to include any at all, like:
$$ \forall x \lnot ( \forall y ~ \operatorname{eats}(x,y) \lnot \operatorname{killedby}(x,y)) \lor \operatorname{food}(y) $$
or,
$$ \forall x  \forall y \lnot(\operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y)) \lor \operatorname{food}(y) $$
and I also wanted to know how the meanings differ.
 A: All of these expressions are misbracketed, even allowing the conventional precedence among propositional operators. And in standard (non-Polish) syntax, correct bracketing matters.
Your first attempt should be bracketed

$$\forall x \forall y[\operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y) \to \operatorname{food}(y)]$$

using square brackets to highlight the necessary additional bracketing. Note: Quantifiers bind tightly to what immediately follows them, so your original expression would be parsed 
$\quad\quad\quad \quad\quad \quad\quad\quad \quad\{\forall x \forall y \operatorname{eats}(x,y)\} \land \lnot \operatorname{killedby}(x,y) \to \operatorname{food}(y)$
adding braces to make clear the scope of the quantifiers, and this isn't what you mean at all, not being a closed wff. The first wff is evidently equivalent to

$$\forall x \forall y[\neg[\operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y)] \lor \operatorname{food}(y)]$$

which is a correctly bracketing version of your third version. We can swap the order of universals, which gives us

$$\forall y \forall x[\neg[\operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y)] \lor \operatorname{food}(y)]$$

and since $\forall x(\varphi(x) \lor C)$ is equivalent to  $(\forall x\varphi(x) \lor C)$ where $C$ doesn't contain $x$ free, the last wff is in turn equivalent to

$$\forall y [\forall x\neg[\operatorname{eats}(x,y) \land \lnot \operatorname{killedby}(x,y)] \lor \operatorname{food}(y)]$$

which I take it is what your second attempt is a fumble for.
