Cfrgtkky

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....)

First, as others have pointed out, the use of 'only' in English is ambiguous.

Still, given that it says 'the only', I would very much give preference to your interpretation instead of your TA's interpretation.

Second, here is a more efficient way to formalize your interpretation:

$$forall x forall y (x + y = x leftrightarrow y = 0)$$

Finally, while this formalization will work just fine in practice when working with numbers, I have to agree with Mees that a technically more correct symbolization would be of the form:

$$forall y (y text{ is a neutral element for addition } leftrightarrow y = 0)$$

i.e.:

$$forall y (forall x x + y = x leftrightarrow y = 0)$$

Or, if one wants to get really pedantic:

$$forall y (forall x ( x + y = x land y + x = x) leftrightarrow y = 0)$$