(* 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)=