Adding "-" as a binary function to the language of rings and the sentence $∀x(x+(−x)=0)∀x(x+(−x)=0)$ to the set of axioms proves existence of additive inverses. But I can't see how Professor Marker's way adding the "$-$" to the language as a binary function and the axiom $∀x∀y∀z(x−y=z⟷x=y+z)$ to the set of axioms of rings is really proving the existence of the additive inverse! and he also says: This axiom is only necessary because we include "$−$" in the language. (this will be useful later); and I don't see how? Is it by deducing from the second axiom that: $∀x(x−x=0⟷x=x+0)$; is it right to say so? even if it is the case again does it prove it's existence?
Would be pleased if you could clarify.
Let me write $-^1$ for (unary) negation and $-^2$ for (binary) subtraction. The issue is really just about the additive groups of the rings. If you axiomatize abelian groups over the signature $(0, +)$, then you need an AE formula such as $\forall x\exists y\,x + y = 0$ to ensure the existence of inverses. Adding negation or substraction to the signature lets you give a purely universal axiomatization. I believe this is what "will be useful later", e.g., when the theory of integral domains is shown to be axiomatized by the purely universal part of the theory of algebraic closed fields.
I don't think Marker is saying that subtraction has any technical advantage over negation: the two formulations are equivalent: using Marker's axioms for subtraction and $\forall x\,x + -^1x = 0$ for negation. To see this, your argument above and the axiom $\forall x\,x = x + 0$ give that with $-^1 x$ defined as $0 -^2 x$, we have $x + -^1 x = 0$; conversely with $x -^2 y$ defined as $x + -^1 y$, you can easily verify Marker's axioms for subtraction.