(* started August 25, 1997 *) (* modified May 29, 1998 for installation in algebra2.mk2 *) (* purpose: develop the theory of order for real numbers *) (* this theory of order for the reals takes the common approach of defining the notion of "less than" for real numbers in terms of the notion of "positive" real number; the axioms for "positive" are somewhat simpler than the axioms of order *) (* two theorems are provided in comments which were added to older theories in the course of development of this file; if you are running an old version of the web page files, you may need one or both of these theorems (ZERONOTONE and SIGNPULL) *) (* script "algebra2"; *) (* this is how this will link in when it is complete *) (* this theorem has been added to naturals.mk2; it is provided here in case you are running this file with an older version of naturals *) (* (* ZERONOTONE: 0 = 1 = false *) s "0=1"; ri "(LEFT@ZERONAT)**RIGHT@ONENAT"; rri "EVALEQ"; ex(); p "ZERONOTONE"; *) (* (* this theorem is found in the newest version of algebra2.mk2 but reproduced here in case you are using an old version *) (* SIGNPULL: ?x * -?y = -?x * ?y ["BUILTIN","CASEINTRO","DIST","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TIMESCOMM","TIMESTYPE","TYPES"] *) s "?x* -?y"; ri "TADDTOP@TIMESTYPE"; ex(); rri "PLUSID"; ex(); left(); initializecounter(); ri "REALZERO"; rri "PLUSMINUS"; ex(); assign "?y_2" "?x*?y"; top(); ri "PLUSASSOC"; ex(); right(); rri "DIST"; ex(); right(); ri "PLUSCOMM**PLUSMINUS** \$REALZERO"; ex(); up(); ri "TIMESCOMM**TIMESZERO"; ex(); up(); ri "COMMPLUSID**TREMTOP@MINUSTYPE"; ex(); prove "SIGNPULL"; *) declareconstant "Positive"; (* predicate true of positive real numbers *) axiom "POSTYPE" "Positive@?x" "bool:Positive@Real:?x"; axiom "POSPLUS" "(Positive@?x)&Positive@?y" "(Positive@?x+?y)&(Positive@?x)&(Positive@?y)"; axiom "POSTIMES" "(Positive@?x)&Positive@?y" "(Positive@?x*?y)&(Positive@?x)&(Positive@?y)"; axiom "TRICHOTOMY" "(Positive@?x)|(Positive@ -?x)" "~0=Real:?x"; axiom "REAL_LESS_DEF" "?x?y" "?y=?y" "((Real:?x)=(Real:?y))|?x>?y"; defineinfix "NOT_EQ" "?x~=?y" "~?x=?y"; s "Positive@?x"; ri "POSTYPE"; ex(); right();right(); initializecounter(); rri "PLUSMINUS"; ex(); assign "?y_1" "0"; ri "PLUSCOMM**PLUSID"; ex(); top(); rri "POSTYPE"; rri "REAL_LESS_DEF"; ex(); p "ALT_POS_DEF"; (* POSASSERT: Positive @ ?x = |-Positive @ ?x ["ASSERT","POSTYPE","TYPES"] *) s "Positive@?x"; ri "POSTYPE"; rri "TYPES"; ri "RIGHT@ \$POSTYPE"; ri "ASSERT2"; ex(); prove "POSASSERT"; (* ZERONOTPOS: Positive @ 0 = false ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"] *) s "Positive@0"; ri "POSASSERT** \$DIDEM"; ex(); right();right(); rri "MINUSZERO"; ex(); top(); ri "TRICHOTOMY"; ex(); right();right(); rri "REALZERO"; ex(); up(); ri "REFLEX"; ex(); up(); rri "FDEF";ex(); p "ZERONOTPOS"; (* NOTBOTHPOS: (Positive @ ?x) & Positive @ -?x = false ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"] *) s "(Positive@?x)&Positive@ -?x"; ri "POSPLUS"; ex(); left();right(); ri "PLUSCOMM**PLUSMINUS"; ex(); up(); ri "POSTYPE**(EVERYWHERE@TYPES)** \$POSTYPE"; ex(); ri "ZERONOTPOS"; ex(); up(); ri "CSYM**CZER"; ex(); p "NOTBOTHPOS"; s "(0=Real:?x)|Positive@?x*?x"; ri "MAKE_CASE"; ex(); ri "OR_EXP"; ex(); rri "NOT_EXP"; ex(); left(); rri "TRICHOTOMY"; ex(); top(); ri "OR_EXP"; ex(); ri "EVERYWHERE2@ODDCHOICE"; ex(); downtoleft "false"; ri "FDEF"; ex(); right(); ri "(\$AT)** \$CIDEM"; ex(); ri "RL@0|-|1"; ex(); ri "POSTIMES"; ex(); left(); ri "POSASSERT** \$ASSERT_UNEXP"; ex(); ri "ODDCHOICE**1|-|2"; ex(); up();up(); ri "NEWTAUT"; ex(); up();up();up(); downtoright "false"; ri "FDEF"; ex(); right(); ri "(\$AT)** \$CIDEM"; ex(); ri "RL@0|-|2"; ex(); ri "POSTIMES"; ex(); left();right(); ri "SIGNPULL**RIGHT@TIMESCOMM**SIGNPULL"; ex(); ri "MINUSMINUS"; ex(); up(); ri "POSTYPE**(EVERYWHERE@TYPES)** \$POSTYPE"; ex(); ri "POSASSERT** \$ASSERT_UNEXP"; ex(); ri "ODDCHOICE**1|-|3"; ex(); up();up(); ri "NEWTAUT"; ex(); top(); ri "EVERYWHERE@ \$CASEINTRO"; ex(); prove "SQUARE_POS"; (* POS_ONE: Positive @ 1 = true ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","DIST","EQUATION","EVALEQ","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTIMES","POSTYPE","REFLEX","TIMESCOMM","TIMESID","TIMESTYPE","TRICHOTOMY","TYPES","XOR"] *) s "Positive@1"; ri "POSTYPE"; ex(); ri "EVERYWHERE@ \$TIMESID"; ex(); ri "ASSERT2"; ex(); ri "(\$DID)**DSYM"; ex(); left(); rri "ZERONOTONE"; ex(); right(); ri "ONENAT**REALNAT**RIGHT@ \$BUILTIN"; ex(); top(); ri "SQUARE_POS"; ex(); p "POS_ONE"; (* POS_ZERO: Positive @ 0 = false ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSTYPE","REFLEX","TRICHOTOMY","TYPES","XOR"] *) s "Positive@0"; ri "POSASSERT"; ex(); rri "DIDEM"; ex(); right();right(); rri "MINUSZERO"; ex(); up();up(); ri "TRICHOTOMY"; ex(); right();left(); ri "REALZERO"; ex(); up(); ri "REFLEX"; ex(); top(); ri "NEWTAUT"; ex(); p "POS_ZERO"; (* REAL_LESS_TRANS: (?x < ?y) & ?y < ?z = (?x < ?z) & (?x < ?y) & ?y < ?z ["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","POSPLUS","REAL_LESS_DEF","REFLEX","TYPES"] *) s "(?x=Nat:?y"; ri "GREATER_EQ_REAL"; ex(); ri "EVERYWHERE@ \$REALNAT"; ex(); ri "DSYM"; ex(); p "GREATER_OR_EQ"; s "(Nat:?x)=