Hi guys,

Suppose following axiomatization of real numbers:

($\displaystyle \exists !$ is syntactical sugar for uniqueness quantifier)

(+ 1) $\displaystyle \forall a \forall b~a+b = b+a$

(+ 2) $\displaystyle \forall a \forall b\forall c~ a+(b+c) = (a+b)+c$

(+ 3) $\displaystyle \forall a \forall b \exists ! x~a+x = b$

(. 1) $\displaystyle \forall a \forall b~ab = ba$

(. 2) $\displaystyle \forall a \forall b \forall c~a(bc) = (ab)c$

(. 3) $\displaystyle \forall a \forall b~(a \neq 0 \rightarrow \exists ! x~ax = b)$

(+ .) $\displaystyle \forall a \forall b \forall c~(a+b)c = ac + bc$

(< 1) forall $\displaystyle a$ forall $\displaystyle b$, one of the following holds: $\displaystyle a < b$, $\displaystyle a = b$, $\displaystyle b < a$

(< 2) $\displaystyle \forall a \forall b \forall c~a<b \wedge b < c \rightarrow a < c $

(+ <) $\displaystyle \forall a \forall b \forall c~a<b \rightarrow a+c < b+c$

(. <) $\displaystyle \forall a \forall b~0 < a \wedge 0 < b \rightarrow 0 <ab$

(sup) Let $\displaystyle A$ be non-empty set, s.t. it has upper bound. Then $\displaystyle \exists \alpha (\forall x~x \leq \alpha~\wedge~\forall \beta ~ \beta < \alpha \rightarrow ~ \exists a~ \beta < a)$

Now following theorem holds: There is precisely one element (which will be denoted $\displaystyle 0$), which is solution of equation $\displaystyle \forall a~ a+x = a$.

Proof: Assume some fixed $\displaystyle b$. Let the only solution of $\displaystyle b+x = b$ be denoted by symbol $\displaystyle 0$. So $\displaystyle b+0=b$ holds.

Now proof is straightforward and I will not finish it. My problem is that $\displaystyle 0$ is formal symbol of our first-order theory (i.e. it is non-logical constant) and no axiom define any property that should $\displaystyle 0$ obbey. However the first step of the theorem says something like $\displaystyle \exists b~b+0 =b$. My question is why is this correct? I don't see any inference rule which interlinks $\displaystyle 0$ and axiom (+ 3).

any ideas why is that correct? thanks