(theory Reals :aliases {Real Closed Fields} :written_by {Cesare Tinelli} :date {08/04/05} :updated {30/01/09} :history { 30/01/09 removed erroneous :assoc attribute for binary minus } :references { 1) W. Hodges. Model theory. Cambridge University Press, 1993. 2) PlanetMath, http://planetmath.org/encyclopedia/RealClosedFields.html } :sorts (Real) :notes "The (unsupported) annotations of the function/predicate symbols have the following meaning: attribute | possible value | meaning ------------------------------------------------------- :assoc // the symbol is associative :comm // the symbol is commutative :unit a constant c c is the symbol's left and right unit :trans // the symbol is transitive :refl // the symbol is reflexive :irref // the symbol is irreflexive :antisym // the symbol is antisymmetric " :funs ((0 Real) (1 Real) (~ Real Real) ; unary minus (- Real Real Real) ; binary minus (+ Real Real Real :assoc :comm :unit {0}) (* Real Real Real :assoc :comm :unit {1}) ) :preds ((<= Real Real :refl :trans :antisym) (< Real Real :trans :irref) (>= Real Real :refl :trans :antisym) (> Real Real :trans :irref) ) :definition "The standard first-order theory of real numbers, but with no overloading of the minus symbols. This is the set of all the first-order sentences over the given signature that are true in the structure of the real numbers that interprets the signature's symbols in the obvious way. This theory coincides with the theory of real closed fields, axiomatized by the sentences in the :axioms field, plus the two axioms schemas also listed, but in comments, in the same field. " :axioms ( ; associativity of + (forall (?x Real) (?y Real) (?z Real) (= (+ (+ ?x ?y) ?z) (+ ?x (+ ?y ?z)))) ; commutativity of + (forall (?x Real) (?y Real) (= (* ?x ?y) (* ?y ?x))) ; 0 is the right (and by commutativity, left) unit of + (forall (?x Real) (= (+ ?x 0) ?x)) ; right (and left) inverse wrt + (forall (?x Real) (= (+ ?x (~ ?x)) 0)) ; associativity of * (forall (?x Real) (?y Real) (?z Real) (= (* (* ?x ?y) ?z) (* ?x (* ?y ?z)))) ; commutativity of * (forall (?x Real) (?y Real) (= (* ?x ?y) (* ?y ?x))) ; 1 is the right (and by commutativity, left) unit of * (forall (?x Real) (= (* ?x 1) ?x)) ; existence of right (and left) inverse wrt * (forall (?x Real) (or (= ?x 0) (exists (?y Real) (= (* ?x ?y) 1)))) ; left distributivity of * over + (forall (?x Real) (?y Real) (?z Real) (= (* ?x (+ ?y ?z)) (+ (* ?x ?y) (* ?x ?z)))) ; right distributivity of * over + (forall (?x Real) (?y Real) (?z Real) (= (* (+ ?x ?y) ?z) (+ (* ?x ?z) (* ?y ?z)))) ; non-triviality (distinct 0 1) ; all positive elements have a square root (forall (?x Real) (exists (?y Real) (or (= ?x (* ?y ?y)) (= (~ ?x) (* ?y ?y))))) ; axiom schemas for all n > 0 ; (forall (?x_1 Real) ... (?x_n Real) ; (distinct (+ (* ?x_1 ?x_1) (+ ... (* ?x_n ?x_n))) ; (~ 1))) ; axiom schemas for all odd n > 0 where ; (^ y n) abbreviates the n-fold product of y with itself ; (forall (?x_1 Real) ... (?x_n Real) ; (exists (?y Real) ; (= 0 ; (+ (^ ?y n) (+ (* ?x_1 (^ ?y n-1)) (+ ... (+ (* ?x_{n-1} ?y) ?x_n))))))) ; reflexivity of <= (forall (?x Real) (<= ?x ?x)) ; antisymmetry of <= (forall (?x Real) (?y Real) (implies (and (<= ?x ?y) (<= ?y ?x)) (= ?x ?y))) ; transitivity of <= (forall (?x Real) (?y Real) (?z Real) (implies (and (<= ?x ?y) (<= ?y ?z)) (<= ?x ?z))) ; totality of <= (forall (?x Real) (?y Real) (or (<= ?x ?y) (<= ?y ?x))) ; monotonicity of <= wrt + (forall (?x Real) (?y Real) (?z Real) (implies (<= ?x ?y) (<= (+ ?x ?z) (+ ?y ?z)))) ; monotonicity of <= wrt * (forall (?x Real) (?y Real) (?z Real) (implies (and (<= ?x ?y) (<= 0 ?z)) (<= (* ?z ?x) (* ?z ?y)))) ; definition of binary minus (forall (?x Real) (?y Real) (= (- ?x ?y) (+ ?x (~ ?y)))) ; definition of < (forall (?x Real) (?y Real) (iff (< ?x ?y) (and (<= ?x ?y) (distinct ?x ?y))) ) ; definition of >= (forall (?x Real) (?y Real) (iff (>= ?x ?y) (<= ?y ?x)) ) ; definition of > (forall (?x Real) (?y Real) (iff (> ?x ?y) (< ?y ?x)) ) ) )