# Thread: axiomatization of real numbers

1. ## axiomatization of real numbers

Hi guys,

Suppose following axiomatization of real numbers:
( $\exists !$ is syntactical sugar for uniqueness quantifier)

(+ 1) $\forall a \forall b~a+b = b+a$
(+ 2) $\forall a \forall b\forall c~ a+(b+c) = (a+b)+c$
(+ 3) $\forall a \forall b \exists ! x~a+x = b$

(. 1) $\forall a \forall b~ab = ba$
(. 2) $\forall a \forall b \forall c~a(bc) = (ab)c$
(. 3) $\forall a \forall b~(a \neq 0 \rightarrow \exists ! x~ax = b)$

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

(< 1) forall $a$ forall $b$, one of the following holds: $a < b$, $a = b$, $b < a$
(< 2) $\forall a \forall b \forall c~a
(+ <) $\forall a \forall b \forall c~a
(. <) $\forall a \forall b~0 < a \wedge 0 < b \rightarrow 0

(sup) Let $A$ be non-empty set, s.t. it has upper bound. Then $\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 $0$), which is solution of equation $\forall a~ a+x = a$.
Proof: Assume some fixed $b$. Let the only solution of $b+x = b$ be denoted by symbol $0$. So $b+0=b$ holds.

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

any ideas why is that correct? thanks

2. ## Re: axiomatization of real numbers

I am not sure I fully understand the question, but there is a theorem allowing the introduction of new functional symbols. Namely, let T be the original theory. We proved $\exists! x\forall a\,a+x=a$. Let T' be T with a new constant 0 and a new axiom $\forall a\,a+0 = a$. We can define a natural translation from formulas of T' to formulas of T: e.g.,

$\forall b\exists c\,b + c = 0$

is translated into

$\forall b\exists c\,(\forall x\,((\forall a\,a+x=a)\to b+c=x))$

If $A$ is a formula in T', let $A^*$ denote the translation of A, which is a formula in T. Then $T'\vdash A$ iff $T\vdash A^*$, and for all formulas $A$ in the language of T, $T'\vdash A$ iff $T\vdash A$.