Spivak uses a property in its own proof?

Question

I'm reading Spivak's Calculus 4th Edition and in Chapter 1: Basic Properties of Numbers I'm having trouble understanding a proof of one of those basic properties.

He first establishes 3 basic properties:

1. $a + (b + c) = (a + b) + c$
2. $a + 0 = 0 + a = a$
3. $a + (-a) = (-a) + a = 0$

Here I quote Spivak:

Property P2 ought to represent a distinguishing characteristic of the number $0$, and it is comforting to note that we are already in a position to prove this. Indeed, if a number $x$ satisfies $$a+x=a$$ for any one number $a$, then $x = 0$ (and consequently this equation also holds for all numbers $a$). The proof of this assertion involves nothing more than subtracting $a$ from both sides of the equation, in other words, adding $-a$ to both sides; as the following detailed proof shows, all three properties P1—P3 must be used to justify this operation. $$ \begin{equation} \begin{split} &\text{If } \qquad\qquad\qquad\: a+x=a, \\ &\text{then }\qquad(-a)+(a+x)=(-a)+a=0; \\ &\text{hence } \:\:\quad ((-a)+a)+x=0; \\ &\text{hence } \:\:\,\,\qquad\qquad 0+x=0; \\ &\text{hence } \qquad\qquad\qquad\,\, x=0. \ \end{split} \end{equation} $$

From what I understood this is a proof of the second property, yet he explicitly states that the second property must be used in the proof. I can't see how this can be justified and I'm finding it frustrating to decipher the logic behind this proof. Can somebody point to where I'm getting this wrong because I'm confident it's a mistake on my behalf rather than an error in the textbook, which is hard to believe considering the many editions the book has been through and is rare for an author of Spivak's caliber.

Also wouldn't a property such as this simply be considered as an axiom of some set of numbers, such as the earlier ones, how does one know whether such a basic property can even be proved?

I found this relevant question Does the given proof show that 0 is the unique additive identity?, but the answer seems to point out that Spivak doesn't prove it but rather stipulates it through P2 which seems odd since Spivak himself states that it is proved.

Apologies in advance if I've made an embarrassing mistake/omission, this book isn't an easy read for me.

Answer 1

No, he's not using Property P2 to prove itself.

Property $2$ merely states that $0$ is an element that satisfies the equation $a + 0 = 0 + a = a$ for any number $a$. That is to say, this is an assertion of the existence of $0$.

What follows in the quoted text is a proof, using Properties P1, P2, P3, that if such an element exists, it is unique, as implied by his leading statement (emphasis mine)

Property P2 ought to represent a distinguishing characteristic of the number $0$.

In other words, the existence of $0$ as asserted in Property P2, along with the other two properties, assures that it must also be unique.

Answer 2

Here I quote Spivak:

Property P2 ought to represent a distinguishing characteristic of the number $0$, and it is comforting to note that we are already in a position to prove this.

"This" refers not to Property P2, but rather to $$\forall x \forall a\;\big(a+x=a\implies x=0\big).$$

(It does cursorily read like he was referring to P2 itself.)