In my home work assignment I was asked to formalize different statements. One of them was (assuming that we are talking about whole numbers): "Zero is the only neutral element in respect to addition." My way of formalizing it was: $$\forall_x \left( x + 0 = x \; \wedge \; \forall_y \left( (y + x = x) \rightarrow y = 0 \right) \right) $$ I thought that to formalize it correctly I need to state, first of all, that zero is neutral element with respect to addition, and after that to state that zero is the only neutral element, by saying that for any other element, if it's neutral with respect to addition, that means that it is zero.
Today I get back my assignment and my TA marked this formalization as not correct, stated that my formalization is "stronger" that required, and provided the following formalization as the correct one: $$\forall_y \forall_x \left( (x + y = x) \rightarrow (y = 0) \right)$$
In my understanding this formalization means that for all $y$ if $y$ is neutral element with respect to addition then $y$ is zero, but in this formalization there is no statement about existence of zero as neutral element.
So my question is: What is the right formalization of the statement and if my way of formalization was wrong, please explain why it's not correct.
It depends on the logical interpretation of the English phrase "Zero is the only neutral element", and specifically the word "only". Does it mean precisely one, or does it mean at most one? Your interpretation gives the former, his interpretation gives the latter. Personally I prefer your interpretation, but this appears to be what the difference comes down to.
As a side note, I would add that I would consider both of your formalizations wrong. Consider for example the model $(\mathbb Z \cup \{\infty\}, +, 0)$, where $+$ is defined the obvious way on $\infty$: anything plus infinity equals infinity. In this case, I would still call 0 the only neutral element for addition: it is the only element that, when added to anything, gives back that same element. However, neither your nor your TA's sentence holds in this structure: instantiating either sentence with $x = y = \infty$ shows that the sentences do not hold. I would consider a correct formalization to be $$ \forall x (x + 0 = x) \land \forall y(\forall x (x + y = x) \to y = 0). $$ (Although even this may not be the right formalization if $+$ is not commutative....)