How to prove that $(-a)$ is real number if $a$ is real number using additive inverse axiom? That is: $ \forall a[a \in \mathbb{R} \implies(-a) \in \mathbb{R}]$ is implied by $\forall_{a \in \mathbb{R}} \exists_{(-a) \in \mathbb{R}}[a+(-a)=0]$ ?
As far I have got is that $\forall_{a \in \mathbb{R}} \exists_{(-a) \in \mathbb{R}}[a+(-a)=0]$ implies $ \forall a[a \in \mathbb{R} \implies \exists(-a) \in \mathbb{R}]$.
P.S. I have 5 A4x48 pages notebooks filled with solved logical problems, I have masters degree at chemistry. I have tried to solve this problem for several days. It is not obvious for me.
It would be nice to receive answer in terms of natural deduction, preferably in Fitch notation.
This is not well formed in first-order logic. The axiom is $$\forall a \exists b ((a+b)=0)$$ You have symbols for
There is no unary function symbol $(-a)$. If you had such a unary function symbol in the language, the axiom would say $$\forall a ((a+(-a)) = 0)$$
Your sentence $\forall a[a \in \mathbb{R} \implies(-a) \in \mathbb{R}]$ is not in the language. There is no binary relation symbol $\in$ and no constant $\mathbb{R}$. If it's a claim about a model of the axioms then it's "a tautology", because any element in the range of an interpretation of a function symbol is in the model, and any element asserted to exist by an axiom is in the model.