Is my proof of the uniqueness of $0$ non-circular? Please try to avoid jumping directly the proof, the text before it is crucial to my question as well.
I had a proof of this here, but I have come to realize that the proof is circular since I implied the result in all $3$ lemmas. I also believe that the one liner given in a comment to that question ($e_1=e_1+e_2=e_2$) also relies on some assumptions which were not given in the text. So allow me to write exactly what is given, exactly as written from the text (Apostol's "Mathematical Analysis"):
Definition of addition and multiplication: 
Along with the set R of real numbers we assume the existence of two operations, called addition and multiplication, such that for every pair of real numbers $x$ and $y$ the sum $x+y$ and the product $xy$ are real numbers satisfying the following axioms. (In the axioms that appeat below, $x, y, z$ represent arbitrary real numbers unless something is said to the contrary)
Axiom 1:
Commutative Laws
$x+y=y+x$, $xy=yx$
Axiom 2: Associative Laws
$x+(y+z)=(x+y)+z$, $x(yz)=(xy)z$
Axiom 3: Distributive Law
$x(y+z)=xy+yz$
Axiom 4:
Given any two real numbers $x$ and $y$, there exists a real number $z$ such that $x+z=y$. This $z$ is denoted by $y-x$; the number $x-x$ is denoted by $0$ (it can be proved that $0$ is independent of $x$.) We write $-x$ for $0-x$ and call $-x$ the negative of $x$. 

Please Note: 
I will denote the number $x-x$ as $0_x$ and $y-y$ as $0_y$. 
We are not given $x + 0 = x$ or $x + (-x) = 0$ in the general sense (which would imply a piece of information that is not given in the text about $0$). What I mean by that is that we are given that $x + (x-x)=x$, but we are not given that $x+(y-y)=x$. And we are given $x + ((x-x)-x) = x-x$, but we are not given $x + ((y-y)-x) = x-x$. The only piece of information we have about $0$ is that it is the symbol which denotes $x-x$, the number which when added to $x$ results in $x$.
Before I start the actual proof, I want to make another note; the way I understand it, the "uniqueness of $0$" can have at least $2$ different meanings:
$1)$ The number $0_x$ that satisfies $x + 0_x = x$ is unique
$2)$ The number $0_x$ is the same as $0_y$
I believe the first meaning of uniqueness follows from the definition of $z$ in axiom $4$, as the wording in axiom $4$ seems to imply that $z$ in axiom $4$ is unique (please let me know if I am correct/incorrect here). Also, were are not given $y-x=y+(-x)$; $y-x$ is just a symbol for the number $z$ in axiom $4$.
So now I am trying to prove the second meaning of uniqueness (this proof is similar to the one in the linked question, only hopefully witouth circular assumptions):
Lemma: If $x+z=y+z$, then $x=y$
Let $x=y$
Add $z$ to both sides
$x+z=y+z$. 
Therefore, if $x+z=y+z$, then $x=y$
I think the proof of this lemma is correct only if we assume that addition is an operation which maps two real numbers to one unique real number. Is this a fair assumption to make from the definition of addition given above? Is there a way to prove this lemma without this assumption?
Proof that $0_x=0_y$
So just a refresher on the definition, $0_x=x-x$ and $0_y=y-y$
$x + 0_x = x$
$y + 0_y = y$
By axiom $4$, we are guaranteed that there exists a (unique?) $z$ such that $x + z = y$, so we will replace $y$ by $x + z$.
$x +z + 0_y = x+z$
By associative and commutative laws,
$(x + 0_y)+z = (x)+z$
By the lemma,
$(x + 0_y) = (x)$
but
$(x + 0_x) = (x)$
And if meaning number $1$ of uniqueness given above is true, then $0_x = 0_y$
 A: The "proof" of the lemma is incorrect: when you write "let $x=y$," you are assuming what you are trying to prove. You need to start with "$x+z=y+z$" and deduce "$x=y$."
As a matter of fact, I'm worried the axioms you've given are not enough, although I don't immediately see how to construct a model proving this. Apostol does give other axioms (the order axioms), but they seem to take the uniqueness of $0$ for granted. I wouldn't be too surprised if there is a clever way to show that $0_x=0_y$ just from the axioms he gives, but I can't see it right now, and I also wouldn't be surprised if it's his mistaske.

Note that the existence of a specific zero element is usually taken as one of the field axioms; see https://en.wikipedia.org/wiki/Field_(mathematics)#Definition_and_illustration.
A: I also believe that, in its current form, Axiom 4 is not strong enough to prove unicity. I think we need to modify the first sentence of Axiom 4 to read:

Given any two real numbers $x$ and $y$, there exists a unique real number $z$ such that $x + z = y$.

Then to show that $0_x$ = $0_y$ it suffices to show that $x + y + 0_x = x + y = x + y + 0_y$, and this follows from the definitions of $0_x$ and $0_y$ and the commutativity and associativity axioms.
A: I was thinking about this on the train today.
You left out axiom 6 and 7 : two order axioms:  
Axiom 6: Exactly one of the following holds: $x = y, x < y,$ or $x > y$.
Axiom 7: If $x < y$ then for every x $x + z < y + z$
With these we can conclude that $m + y = n + y \iff m = n$ (Precisely on $m < n; m = n; m > n$ assures precisely one possible condition for $m + y$ to $n + y$)
With that we can note that in Axiom 4, "given x and y there exists a z such that z + x = y" we can now know such a z is unique.
And thus $0_y = y - y$ is the unique element such that $0_y + y = y + 0_y = y$.
Okay.  So suppose $x + 0_y = z$.  Then $ \implies  x + 0_y + y = x + y = z + y \implies x = z \implies x + 0_y = x \implies 0_y = x - x = 0_x$.
Thus $0$ is unique.
I don't think you can prove $m + y = n + y \iff m = n$ without the order principle.  I could be wrong but I doubt it. ... Oh wait..
Suppose $m + y = n +y = z$.  If $v = (n -y) -m$ and $w = m -y$.  
With tedium we can show $v + w + y + y$ equals both $m$ and $n$ so $m = n$.
