Logical Formalization of: "Children don't eat pasta with spinach or mushrooms on it" I want to formalize the following sentence in predicate logic:

If a children has spinach or mushrooms on its pasta then it will not
  eat its pasta.

The headline contains a shorter version. I have four solutions where l like your opinion or recommendation on:
\begin{align}
\forall x \forall y \, &((IsChildren(x) \land IsPasta(y) \land {} \\
&\land (hasIngridient(y,Spinach) \lor hasIngridient(y,Mushroom)) \rightarrow \neg Eatspasta(x,y) )
\end{align}


*

*Modification: Could I omit $IsChildren(x)\land IsPasta(y)$ though naming $x$ in child and $y$ in pasta? For example:
\begin{align}
\forall child \forall pasta \, &((hasIngridient(pasta,Spinach) \lor hasIngridient(pasta,Mushroom)) \\
&\rightarrow \neg EatsPasta(child,pasta) )
\end{align}


Q1.1 Are variables allowed with more then one letter?
Q1.2 I think the name of a variable (is child or $x$) does not matter for its interpretation. So after the first modification child could be anything from my discourse universe. 


*Modification: Could I omit $\forall y$ by changing the formalization as follows:
\begin{align}
\forall x \, &(isChilrden(x) \land (hasIngridientSpinachOnPasta(x) \lor hasIngridientMushroomOnPasta(x)) \\
&\rightarrow \neg EatsPasta(x) )
\end{align}

*Modification: Could I omit $\forall y$ by changing the formalization as follows:
\begin{align}
\forall x \, &(isChilrden(x) \land (hasIngridientSpinach(Pasta) \lor hasIngridientMushroomOnPasta(Pasta)) \\ 
&\rightarrow \neg EatsPasta(x,Pasta) )
\end{align}

*Modification: Could I say instead there exist no chilrden that eats pasta with Spinat und Mushrooms:
$$\neg \exists x \forall y x(isChilrden(x) \land (Pasta(y,Spinach) \lor Pasta(y,Mushroom)) \rightarrow EatsPasta(x,y) )$$
Main question: which one are incorrect and why?
 A: 
Q1.1 Are variables allowed with more then one letter?

It's unusual in maths; usually a one-letter symbol with descriptive index is preferred, such as $n_\mathrm{mushrooms}$. But IMO multi-character names are fine, as are multi-character functions ($\sin$, $\log$...). But LaTeX won't typeset these properly if you just write out the letters like that; notice the bad kerning in your post. You should instead wrap such names in a suitable \math??{.} styling. Options are:


*

*$Spinach$ ($Spinach$) (bad!)

*$\mathit{Spinach}$ ($\mathit{Spinach}$)

*$\mathrm{Spinach}$ ($\mathrm{Spinach}$)

*$\mathbf{Spinach}$ ($\mathbf{Spinach}$)

*$\mathsf{Spinach}$ ($\mathsf{Spinach}$)

*$\mathtt{Spinach}$ ($\mathtt{Spinach}$)


I would recommend \mathit for multi-character variables, \mathrm for constants and standard functions, and \mathsf or \mathtt for special situations (like when you're paraphrasing computer code).

Q1.2 I think the name of a variable (is child or x) does not matter for its interpretation

Correct. This is what's in CS called $\alpha$-conversion: any variable that's quantified over with $\forall$ or $\exists$ can be renamed.
Your modifications 2 and 3 don't quite express the original thing, because you don't quantify over the pasta anymore. Basically this means that the pasta is a “global constant”, you only ever consider one. This is often done in maths/science for simplification, but logic-wise it does make a difference.
Modification 4 just turns around the quantors. This can always be done in classical logic:
$$
  (\forall x. \neg P(x)) \leftrightarrow \neg(\exists x. P(x))
$$
