Thread: axiomatization of real numbers

Hi guys,

Suppose following axiomatization of real numbers:
( is syntactical sugar for uniqueness quantifier)

(+ 1)
(+ 2)
(+ 3)

(. 1)
(. 2)
(. 3)

(+ .)


(< 1) forall forall , one of the following holds: , ,
(< 2)
(+ <)
(. <)

(sup) Let be non-empty set, s.t. it has upper bound. Then

Now following theorem holds: There is precisely one element (which will be denoted ), which is solution of equation .
Proof: Assume some fixed . Let the only solution of be denoted by symbol . So holds.

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

any ideas why is that correct? thanks

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 . Let T' be T with a new constant 0 and a new axiom . We can define a natural translation from formulas of T' to formulas of T: e.g.,



is translated into



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