Results 1 to 2 of 2

Thread: axiomatization of real numbers

  1. #1
    Jul 2011

    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<b \wedge b < c \rightarrow a < c
    (+ <) \forall a \forall b \forall c~a<b \rightarrow a+c < b+c
    (. <) \forall a \forall b~0 < a \wedge 0 < b \rightarrow 0 <ab

    (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
    Last edited by jozou; Sep 5th 2011 at 06:07 AM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Oct 2009

    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 1
    Last Post: Sep 27th 2010, 04:14 PM
  2. Real Numbers
    Posted in the Algebra Forum
    Replies: 6
    Last Post: Feb 21st 2010, 03:31 AM
  3. Real Numbers
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: Jan 20th 2009, 03:12 PM
  4. Real Numbers - Real Anaylsis
    Posted in the Calculus Forum
    Replies: 5
    Last Post: Sep 3rd 2008, 11:54 AM
  5. should I use real numbers ??
    Posted in the Advanced Algebra Forum
    Replies: 9
    Last Post: Sep 17th 2006, 12:16 PM

Search Tags

/mathhelpforum @mathhelpforum