Is my proof of $-(-a)=a$ correct? I'm trying to prove theorem $1.4$ with the following:



$$a=a$$
$$a-a=\stackrel{0}{\overline{a-a}}\tag{Ax.5}$$
$$a-a=0\tag{Inverse def.}$$
$$a+(-a)=0\tag{Thm 1.3}$$
Here I thought about packing the $a$ with a minus sign and then it would yield a new minus sign on Its inverse due to the inverse definition.
$$(-a)+(-(-a))=0$$
Adding $a$ to both sides.
$$\stackrel{0}{\overline{a+(-a)}}+(-(-a))=a$$
$$-(-a)=a$$
Is my proof correct?
 A: Better wording:
By theorem 1.2.  For every a there is a unique -a such that a + (-a) = 0.  Likewise for (-a) there is a unique -(-a) such that (-a) + (-(-a)) = 0.
Therefore:
(-a) + (-(-a)) = 0
a + (-a) + (-(-a)) = a+ 0 = a
By associativity:
[a + (-a)] + (-(-a))  = a so
0 + (-(-a)) = (-(-a)) = a.
A: Your proof is correct, but it looks like you're trying to be as precise as possible, so I'll write out a proof you might find helpful. Let $a$ be a real number. By axiom $5$, we there exists a real number $b$, satisfying $a+b=0$.  
Since $b$ is a real number, it also has an inverse, which we may call $c$. The aim is to show $c=a$. Since $a+b=0$, we have $$(a+b)+c=0+c=c$$
And then by axiom $2$ (associativity) we deduce that $$a+(b+c)=c$$
But since $c$ was the inverse of $b$, $b+c=0$, so $a+0=c \implies a=c$. Hopefully that's helpful.
A: What is "packing with a minus sign"? This step seems a little obscure. You are acting like there is an operation which is "putting minus in front", even though (in this stage of axioms) $-a$ is a symbol in itself.
For proving $-(-a)=a$, we have to prove (by definition) that $-a+a=0$. But this is trivial due to commutativity and the characterization of $-a$.
Also, more leisurely:
Proof: We have that $a+(-a)=0$. Now look again. $\blacksquare$
A: The proof uses a bunch of manipulations that are generally legitimate for
later proofs--but notice that in this particular axiomatization of algebra,
the subtraction operation and negative sign are not introduced until
Theorem 1.2. If you look closely at Theorem 1.2, you may notice that it
provides a definition of $-a$ that is, in essence,
$$a + (-a) = 0.$$
That is, Theorem 1.2 is actually the source of the statement you justified
by Theorem 1.3, and it supports that statement directly.
The rest of the proof looks OK. I'm not sure what "packing" means, but
since the statement $a + (-a) = 0$ is true for any real number $a$,
it is certainly true for $-a$, which also is a real number,
and you can write $-a$ instead of $a$ to obtain $(-a) + (-(-a)) = 0.$
A: I'm not exactly clear on how you go from $a+(-a)=0$ to $(-a)+(-(-a))=0$ via "packing". But starting with  $$(-a)+(-(-a)) = 0$$ Then by theorem $1.2$ you have $(-a(a)) = x$ as the unique element such that $c+x = b$ where $b=0$ and $c = (-a).$ However you can just as well satisfy the same values of $c,b$ if $x = a$. Hence by uniqueness $a = -(-a)$.
