(* In this file we once again develop Landau's analysis book, using the latest version of the prover, and using an axiomatic approach (we do not prove the axioms from set theory; we may come back and do that again later *) (* from August 10 on I'm maintaining dated version notes here *) (* August 13: Almost to the end of chapter I! Theorems after Satz32 up to the end of the chapter are stated but not yet proved. *) (* August 11: I must fix the back function so that it works correctly with usubs. It is useless for backing through algebraic calculations as it is. How about a version of rewrites which uses a matching term as an argument? *) (* August 10, posted again: Completed proof of Satz 29, commutativity of multiplication. Note the blowup of type checking obligations in the proof of the lemma LeftTimesSucc. I think that automatic recognition of Triv's would help, combined with automatic theorem matching and a list of theorems to be automatically applied (in type checking, perhaps automatic theorem cuts as well?) *) (* August 10: just finished Satz 27, the well-ordering principle, and am about to start proving theorems about multiplication. The proof of Satz 27 is in some sense a direct induction proof *) (* comments calling for some action later: it would be useful to get the prover to say something like when it is pausing. It might be possible to automate proofs that objects are of appropriate types? It is clear that it would be useful to automate proof of anything immediately trivial after a certain level; this would eliminate a lot of explicit type proofs, for example. The more complicated type proofs are also automatable though. If we see a conclusion of the form X+Y E Nat we could look for hypotheses X E Nat and Y E Nat and auto-prove if they are found. Automatic search for appropriate hyps and conclusions for UseThm is eventually a must. A formal implementation of "exactly one of the following n statements is true" and of "respectively" would be useful. It might be manageable with some set theory? If the bookmark command actually copied the current sequent one level higher in proof tree and moved to it, then automatic reordering and elimination of redundant hypotheses would not generate surprises in the forms of theorems. Just a thought. *) (* Theory of the natural numbers *) (* For Landau version we want to start with 1, not 0 *) (* we use more standard axioms for addition and multiplication, rather than Landau's second-order definition of + and *; we also use x+1 instead of x'. This does not seem to affect the Landau development beyond a certain point, but we will see. *) (* definite description operator *) (* this enables us to introduce operations which pick out any uniquely definable object *) DeclareFunction "The" [0,1]; (* if the object to be described is a set, this is definable *) (* Theset(a1) is the unique element of a1 if this is a set, otherwise it is the empty set *) DefineFunction 1 "Theset" "Theset(x1)" "{x2|(Ax3.(Ax4.x3Ex1&x4Ex1->x3=x4))&(Ex3.x3Ex1&x2Ex3)}"; Axiom "THE" [] ["The({x2|x2=a1})=a1"]; (* the basic property of The *) Start "(Ax1.(Ax2.x1Ea1&x2Ea1->x1=x2))&a2Ea1->a2=The(a1)"; r();l(); bookmark "THE2"; Cut "a1 = {x1|x1=a2}"; r(); Triv 2 1; r(); r(); r(); Gl 2; l(); l(); r(); Triv 4 1; Triv 3 1; Done(); l(); rwr nil; Triv 3 1; rwr nil; ThmCut "THE"; rwr nil; r(); ProveMarked "THE2" "THE2"; (* Theset has a similar basic theorem *) (* declarations *) DeclareFunction "Nat" [0]; DeclareFunction "+" [0,0,0]; DeclareFunction "*" [0,0,0]; (* order of operations *) Spra "*" "+"; (* axioms *) Axiom "OneNat" nil ["1ENat"]; (* the next axiom looks different because I write successor as x+1 (not as a separate operation) so closure under successor is a special case of closure under addition *) Axiom "SumNat" ["a1ENat","a2ENat"] ["a1+a2ENat"]; (* I prove the expected axiom as a theorem *) Start "a1ENat -> a1+1ENat"; r(); ThmCut "SumNat"; Done(); UseThm "OneNat" nil [1]; Done(); Prove 2 "SuccNat"; Axiom "OneNotSucc" ["a1ENat","a1+1=1"] nil; Axiom "SameSucc" ["a1ENat","a2ENat","a1+1=a2+1"] ["a1=a2"]; (* notice use of a restricted quantifier *) Axiom "Induction" ["1Ea1","(Ax1:Nat.x1Ea1->x1+1Ea1)","a2ENat"] ["a2Ea1"]; (* additional axioms to handle recursive definition of addition and multiplication *) Axiom "PlusSucc" ["a1ENat","a2ENat"] ["a1+[a2+1]=[a1+a2]+1"]; Axiom "TimesOne" ["a1ENat"] ["a1*1=a1"]; Axiom "TimesSucc" ["a1ENat","a2ENat"] ["a1*[a2+1]=a1*a2+a1"]; (* a very easy theorem *) (* an odd feature of this theorem is that the ind hyp is never used *) Start "a1ENat -> a1=1 v (Ex1:Nat.x1+1=a1)"; ThmCut "Induction"; su 2 "{x1:Nat|x1=1v(Ex2:Nat.x2+1=x1)}"; r();(* r(); *) UseThm "OneNat" nil [1]; r();r(); (* proof of induction step starts *) r();r();r();(* r(); *) ThmCut "OneNat"; UseThm "SumNat" [3,1] [1]; r(); gr 2; r(); Triv 2 1; r(); (* from here on seems to be tidying up ThmCut *) su 3 "a1"; Gr 2; Triv 1 2; l(); (* rf(); *) r(); Triv 3 1; Prove 1 "OneOrSucc"; (* here starts the proposition by proposition implementation of Landau *) DefinePredicate 2 "neq" "x1 neq x2" "~x1=x2"; Start "a1ENat & a2ENat & a1 neq a2 -> a1+1 neq a2+1"; r();l();Gl 2; Gl 2; l(); Gr 2; r(); UseThm "SameSucc" [2,3,1] [1]; NameSequent 4 "Satz1"; Start "a1ENat -> a1 neq a1+1"; r();r();r(); ThmCut "Induction"; su 2 "{x1:Nat|x1 neq x1+1}"; r(); UseThm "OneNat" nil [1]; r();r(); ThmCut "OneNotSucc"; UseThm "OneNat" nil [1]; crwr nil; r(); r();r();l();r(); UseThm "SuccNat" [1] [1]; ThmCut "Satz1"; Triv 2 1; Done();UseThm "SuccNat" [1] [1]; Done(); Triv 2 1; l(); Gl 2; l(); Done(); Prove 2 "Satz2"; Start "a1ENat & a1 neq 1 -> (Ex1:Nat.x1+1=a1)"; r(); l(); bookmark "Satz3"; ThmCut "Induction"; su 2 "{x1:Nat|x1=1v(Ex2:Nat.x2+1=x1)}"; r(); UseThm "OneNat" nil [1]; r();r(); r();r();r(); UseThm "SuccNat" [2] [1]; r(); Gr 2; Triv 2 1; r(); Done(); l(); Gl 2; Gl 3; l(); Triv 2 1; Done(); ProveMarked "Satz3" "Satz3"; (* Satz4 is an axiom in our scheme *) (* though it might be interesting to try to prove it *) Start "a1ENat&a2ENat&a3ENat->[a1+a2]+a3=a1+a2+a3"; r(); l(); Gl 2; gl 3; bookmark "Satz5"; ThmCut "Induction"; su 4 "{x1:Nat|[a1+a2]+x1=a1+a2+x1}"; r(); UseThm "OneNat" nil [1]; ThmCut "PlusSucc"; sg(); sg(); crwr [1]; r(); Done(); Triv 2 1; r();r();l();r(); UseThm "SuccNat" [1][1]; ThmCut "PlusSucc"; sg(); sg(); rwr [1]; ThmCut "PlusSucc"; sg(); sg(); rwr [1]; ThmCut "PlusSucc"; sg(); sg(); rwr [1]; gl 5; rwr [1];r(); Triv 6 1; UseThm "SumNat" [7,5] [1]; Triv 6 1; Triv 4 1; UseThm "SumNat" [4,5] [1]; Done(); Triv 3 1; l(); Triv 2 1; ProveMarked "Satz5" "Satz5"; Start "a1ENat->1+a1=a1+1"; r(); bookmark "OneComm"; ThmCut "Induction"; su 2 "{x1:Nat|1+x1=x1+1}"; r(); UseThm "OneNat" nil [1]; r(); r();r();l();r(); UseThm "SuccNat" [1] [1]; gl 2; crwr [2]; ThmCut2 "Satz5"; crwr [1]; r(); UseThm "OneNat" nil [1]; Triv 2 1;UseThm "OneNat" nil [1]; Done(); l(); Triv 2 1; (* two lemmas needed for Satz 6 *) ProveMarked "OneComm" "OneComm"; Start "a1ENat&a2ENat->[a1+1]+a2=[a1+a2]+1"; r();l(); bookmark "LeftPlusSucc"; ThmCut "Induction"; su 3 "{x1:Nat|[a1+1]+x1=[a1+x1]+1}"; r(); UseThm "OneNat" nil [1]; r(); r();r();l();r(); UseThm "SuccNat" [1][1]; ThmCut2 "PlusSucc"; rwr [1]; gl 3; rwr [1]; ThmCut2 "PlusSucc"; rwr [1]; r(); Triv 3 1; Triv 6 1; UseThm "SuccNat" [4] [1]; Triv 3 1; sg();l(); Triv 2 1; Triv 2 1; ProveMarked "LeftPlusSucc" "LeftPlusSucc"; Start "a1ENat & a2ENat -> a1+a2=a2+a1"; r();l(); bookmark "Satz6"; ThmCut "Induction"; su 3 "{x1:Nat|a1+x1=x1+a1}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "OneComm"; rwr [1]; r(); Done(); r();r();l();r(); UseThm "SuccNat" [1][1]; gl 2; ThmCut2 "LeftPlusSucc"; rwr [1]; ThmCut2 "PlusSucc"; rwr [1]; gl 3; rwr [1]; r(); Triv 4 1; Triv 3 1; Triv 5 1; Triv 3 1; sg();l(); Triv 2 1; Triv 2 1; ProveMarked "Satz6" "Satz6"; Start "a1ENat&a2ENat->a2 neq a1 + a2"; r();l(); bookmark "Satz7"; ThmCut "Induction"; su 3 "{x1:Nat|x1 neq a1+x1}"; r(); UseThm "OneNat" nil [1]; r(); r(); ThmCut "OneNotSucc"; Triv 2 1; crwr [1]; r(); r();r();l();r(); UseThm "SuccNat" [1][1]; Gl 2;l();Gr 2;r(); ThmCut2 "PlusSucc"; rwl [1]; ThmCut2 "SameSucc"; Triv 1 2; Triv 6 1; UseThm "SumNat" [4,3] [1]; Triv 2 1; Triv 3 1; Triv 2 1; sg();l(); Triv 2 1; Triv 2 1; ProveMarked "Satz7" "Satz7"; (* a technical variation of Satz7 *) Start "a1ENat&a2ENat->a1 neq a1+a2"; r();l(); bookmark "Satz7b"; ThmCut2 "Satz6"; rwr nil; UseThm "Satz7" [3,2] [1]; Done(); Triv 2 1; ProveMarked "Satz7b" "Satz7b"; (* start proof of Satz 8 *) Start "a1ENat&a2ENat&a3ENat->a2neq a3 ->a1+a2 neq a1+a3"; r();l();Gl 2;gl 3; r(); bookmark "Satz8"; ThmCut2 "Induction"; (* using ThmCut2 seems to be an improvement *) su 5 "a1"; su 4 "{x1:Nat|x1+a2 neq x1+a3}"; l(); Triv 2 1; r(); UseThm "OneNat" nil [1]; l();l(); Gr 2; r(); ThmCut "OneComm"; sg(); rwl nil; ThmCut "OneComm"; sg(); gl2 3; rwl nil; UseThm "SameSucc" [4,5,2] [2]; Triv 5 1; Triv 3 1; r();r();l();r(); UseThm "SuccNat" [1][1]; Gl 2;l();Gr 2;r(); ThmCut2 "LeftPlusSucc"; rwl nil; pl 1; ThmCut2 "LeftPlusSucc"; rwl nil; pl 1; ThmCut2 "SameSucc"; Triv 1 2; UseThm "SumNat" [7,5] [1]; UseThm "SumNat" [7,6] [1]; Done(); Triv 7 1; Triv 6 1; Triv 7 1; Triv 5 1; Triv 2 1; ProveMarked "Satz8" "Satz8"; (* start proof of Satz 9 *) (* it is divided into two parts, one asserting the disjunction of the three alternatives and one excluding the possibility that the second and third alternatives both hold *) (* the first alternative is shown to be incompatible with the other two by an earlier theorem (Satz 7) *) (* this should be called Satz9B *) Start "a1ENat&a2ENat->a1=a2v(Ex1:Nat.a1=a2+x1)v(Ex1:Nat.a2=a1+x1)"; r();l(); bookmark "Satz9B"; ThmCut2 "Induction"; su 4 "a2"; su 3 "{x1:Nat|a1=x1v(Ex2:Nat.a1=x1+x2)v(Ex2:Nat.x1=a1+x2)}"; l(); Triv 2 1; r(); UseThm "OneNat" nil [1]; r(); Gr 2; ThmCut "Satz3"; su 3 "a1"; Done(); (* Satz3 needed to be reproved! *) r();r(); Triv 1 4; (* this should be called Satz9A *) Start "a1ENat&a2ENat&a3ENat&a4ENat->a1=a2+a3->a2 neq a1+a4"; r(); l(); Gl 2; Gl 2; gl 3; r(); bookmark "Satz9A"; rwr nil; ThmCut2 "Satz5"; rwr nil; ThmCut2 "Satz7b"; Done(); Triv 4 1; UseThm "SumNat" [5,6] [1]; Triv 3 1; Triv 4 1; Triv 5 1; ProveMarked "Satz9A" "Satz9A"; (* Satz9b *) Start "a1ENat&a2ENat->a1=a2v(Ex1:Nat.a1=a2+x1)v(Ex1:Nat.a2=a1+x1)"; r();l();r();Gr 2; bookmark "Satz9b"; ThmCut2 "Induction"; su 4 "a2"; su 3 "{x1:Nat | a1=x1 v (Ex2:Nat.a1=x1+x2)v(Ex2:Nat.x1=a1+x2)}"; l(); Gl 2; Triv 1 3; l(); Done(); Triv 1 2; r(); UseThm "OneNat" nil [1]; ThmCut2 "Satz3"; l(); su 3 "a1"; r(); Gr 2; r(); sg(); gl 2; crwr [1]; ThmCut2 "Satz6"; Done(); Triv 4 1; UseThm "OneNat" nil [1]; Done(); Done(); r(); r(); r(); Done(); (* survived basis step! *) r();r();r(); UseThm "SuccNat" [2] [1]; l();r(); Gl 2; Gr 2; Gr 2; sg(); rwr [1]; r(); UseThm "OneNat" nil [1]; l(); l(); ThmCut "OneOrSucc"; l(); Done(); l(); gl2 3; rwl nil; Triv 2 1; l(); gl 2; gl2 3; crwl nil; Gr 2; ThmCut2 "PlusSucc"; gl2 3; rwl nil; ThmCut2 "LeftPlusSucc"; gl2 3; crwl nil; crwl nil; r(); sg(); Triv 2 1; Triv 7 1; Triv 3 1; Triv 7 1; Triv 3 1; Triv 7 1; l(); Gr 2; Gr 2; sg(); su 9 "a8+1"; gl 2; rwr nil; ThmCut2 "PlusSucc"; rwr [1]; r(); Triv 3 1; Triv 6 1; UseThm "SuccNat" [1] [1]; Triv 2 1; ProveMarked "Satz9b" "Satz9B"; DefinePredicate 2 ">" "x1>x2" "(Ex3:Nat.x1=x2+x3)"; DefinePredicate 2 "<" "x1=" "x1>=x2" "x1>x2vx1=x2"; DefinePredicate 2 "<=" "x1<=x2" "x1~a1~a1>a1"; r();r(); bookmark "Satz10B"; l();l(); ThmCut2 "Satz7"; l();l(); ThmCut2 "Satz6"; gl2 3; rwl nil; Triv 2 1; Triv 3 1; Done(); Done(); Triv 3 1; ProveMarked "Satz10B" "Satz10B"; Start "a1ENat&a2ENat->~(a1~(a1a2)"; r();r();l();Gl 3; bookmark "Satz10D"; Cut "a2a1=a2va1>a2va1a2>a1"; r(); bookmark "Satz12"; l();r();Done(); ProveMarked "Satz12" "Satz12"; Start "a1>a2->a2a2==a2=a2->a2<=a1"; r(); bookmark "Satz13"; l();r();r(); l(); UseThm "Satz11" [1] [1]; gr 2; rwr nil; r(); ProveMarked "Satz13" "Satz13"; Start "a1<=a2->a2>=a1"; r(); bookmark "Satz14"; l();r();r(); l(); UseThm "Satz12" [1] [1]; gr 2; rwr nil; r(); ProveMarked "Satz14" "Satz14"; Start "a1>=a2==a2<=a1"; r(); UseThm "Satz13" [1][1]; UseThm "Satz14" [1][1]; Prove 1 "OrderRewrite2"; Start "a1ENat&a2ENat&a3ENat->a1a1a1>a2&a2>a3->a1>a3"; r();r();l(); bookmark "Satz15B"; ThmCut "OrderRewrite"; rwl nil; pl 1; gl 2;ThmCut "OrderRewrite"; rwl nil; pl 1; ThmCut "OrderRewrite"; rwr nil; pl 1; UseThm "Satz15" [1,3,2] [1]; ProveMarked "Satz15B" "Satz15B"; (* notice use of biconditionals to rewrite in previous proof! *) (* notice also that Landau's remarks on _not_ proving something like Satz15B bring up exactly the issue of rewriting inequalities which we here implement formally *) (* Satz16A *) Start "a1ENat->a1<=a2&a2a1a1a1a1<=a2&a2<=a3->a1<=a3"; r();r();l(); bookmark "Satz17"; (* define predecessor *) DefineFunction 1 "Pred" "Pred(x1)" "The({x2 : Nat|(x1=1->x2=1)&(x1 neq 1 ->x2+1=x1)})"; (* prove basic properties of Pred *) Start "a1 E Nat & a1 neq 1 -> Pred(a1)+1 = a1"; r(); l(); bookmark "PREDTHM"; ThmCut "Satz3"; Done(); Triv 2 1; l(); Cut "a2=Pred(a1)";r();(* pr 1;pr 1; *) ThmCut "THE2"; su 3 "{x3:Nat|(a1=1->x3=1)&(a1 neq 1 -> x3+1=a1)}"; r();r();r();l();l();Gl 2;Gl 3;Gl 2; Gl 2;Triv 4 1;Gl 8;Triv 7 1; gl 4;gl2 8;crwl nil; UseThm "SameSucc" [9,3,2] [1]; r();Done(); r();r();gl 5;l();l();Done(); r();Triv 3 1;Done(); gl2 3; rwl nil; Triv 2 1; ProveMarked "PREDTHM" "PREDTHM"; (* another theorem about The *) Start "(Ax1.x1Ea1 == x1=a2) -> a2=The(a1)"; r(); bookmark "THE3"; Cut "a1={x2|x2=a2}"; r(); Gr 2; r(); r();l(); su 5 "a4"; r();r();Gl 2;l();Triv 3 1;Done(); l();Gl 2;Gl 2;Triv 2 1;Done(); rwr nil; ThmCut "THE"; rwr nil; r(); ProveMarked "THE3" "THE3"; (* back to the main line of Landau development *) Start "a1ENat&a1<=a2&a2<=a3->a1<=a3"; r();l();Gl 2; bookmark "Satz17"; l();l();r();r();UseThm "Satz16B" [2,3,1] [1]; rwr nil;Triv 2 1; ProveMarked "Satz17" "Satz17"; Start "a1ENat&a2ENat->a1+a2>a1"; r();l(); bookmark "Satz18"; r();r();sg();r();Triv 2 1; ProveMarked "Satz18" "Satz18"; (* note just above that hypotheses about a1 being in Nat turn out not to be needed *) Start "a1ENat&a2ENat&a3ENat&a1>a2->a1+a3>a2+a3"; r();l();Gl 2;Gl 2; bookmark "Satz19A"; Gl 2;l(); r();r();sg(); su 5 "a4"; gl 2; rwr nil; ThmCut2 "Satz6"; rwr [2]; ThmCut2 "Satz6"; rwr [3]; ThmCut2 "Satz5"; rwr nil; r(); Triv 7 1;Triv 5 1;Triv 6 1; UseThm "SumNat" [4,5] [1]; Triv 6 1;Triv 3 1;Triv 5 1;Done(); ProveMarked "Satz19A" "Satz19A"; Start "a1ENat&a2ENat&a3ENat&a1a1+a3a2+a3->a1>a2"; r();l();Gl 2;Gl 2; bookmark "Satz20A"; ThmCut "Satz10E"; sg(); sg(); Done(); Cut "a1+a3a1=a2"; r();l();Gl 2;Gl 2; bookmark "Satz20B"; ThmCut "Satz10E"; sg();sg();sg();sg();Done(); Triv 3 1;Triv 4 1; ThmCut2 "Satz19A"; su 4 "a1"; su 5 "a2"; su 6 "a3"; gl 4; gl2 4; rwl nil; ThmCut "Satz10B"; Triv 2 1; UseThm "SumNat" [6,4][1];Done();Triv 5 1;Triv 2 1; ThmCut2 "Satz19B"; su 7 "a1"; su 8 "a2"; su 6 "a3"; gl 4; gl2 4; rwl nil; ThmCut "Satz10A"; Triv 2 1; UseThm "SumNat" [6,4] [1];Triv 2 1;Done();Triv 4 1; ProveMarked "Satz20B" "Satz20B"; Start "a1ENat&a2ENat&a3ENat&a1+a3a1a2&a3>a4->a1+a3>a2+a4"; r();l();Gl 2;Gl 2;Gl 2; Gl 2; bookmark "Satz21"; ThmCut "Satz19A"; Done(); Triv 4 1; sg(); su 7 "a3"; ThmCut "Satz19A"; Triv 3 1; Triv 7 1; sg(); su 9 "a2"; ThmCut2 "Satz6"; rwl nil; pl 1; ThmCut2 "Satz6"; rwl [2]; ThmCut2 "Satz15B"; Done(); Triv 3 1; Triv 2 1; UseThm "SumNat" [7,9][1]; Triv 8 1; Triv 6 1; Triv 7 1; Triv 6 1; Triv 5 1;Triv 5 1; ProveMarked "Satz21" "Satz21"; (* Satz22A *) Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>=a2&a3>a4->a1+a3>a2+a4"; r();l();Gl 2;Gl 2;Gl 2;Gl 2; bookmark "Satz22A"; l();l();ThmCut "Satz21";Done();Triv 2 1; Triv 4 1;Triv 5 1;Triv 6 1;Done(); rwr nil; ThmCut "Satz19A"; Triv 2 1; Triv 6 1; sg(); ThmCut2 "Satz6"; rwr [1]; ThmCut2 "Satz6"; rwr [2]; Triv 3 1; Triv 6 1; Triv 8 1; Triv 5 1; Triv 6 1; Triv 4 1; ProveMarked "Satz22A" "Satz22A"; (* Satz22B *) Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>a2&a3>=a4->a1+a3>a2+a4"; r();l();Gl 2;Gl 2;Gl 2;Gl 2; bookmark "Satz22B"; ThmCut2 "Satz6"; rwr [1]; ThmCut2 "Satz6"; rwr [2]; ThmCut "Satz22A"; Triv 4 1; Triv 3 1; Triv 8 1;Triv 5 1;Triv 6 1;Done(); Triv 5 1;Triv 7 1;Triv 3 1;Triv 5 1; ProveMarked "Satz22B" "Satz22B"; (* Satz23 *) Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>=a2&a3>=a4->a1+a3>=a2+a4"; r();l();Gl 2;Gl 2;Gl 2;Gl 2; bookmark "Satz23"; l();l();r();r(); UseThm "Satz22B" [1,2,3,4,5,6] [1]; rwr nil;r();r();Gl 2;l(); ThmCut2 "Satz6"; rwr [1]; ThmCut2 "Satz6"; rwr [2]; UseThm "Satz19A" [3,7,5] [1]; Triv 4 1;Triv 6 1;Triv 3 1;Triv 4 1; gr 2; rwr nil; r(); ProveMarked "Satz23" "Satz23"; (* notice in the last couple of theorems contrast between a style using ThmCut and a style using UseThm *) (* Satz24 *) (* Aug. 9, number 1 *) Start "a1ENat->a1>=1"; r(); bookmark "Satz24"; r();r();r();ThmCut "OneOrSucc"; l();Done();l();Triv 1 2; l();r();Done();gl 2; crwr nil; ThmCut2 "Satz6"; Done(); Triv 3 1; UseThm "OneNat" nil [1]; ProveMarked "Satz24" "Satz24"; (* Satz24B *) Start "~(a1ENat&a1<1)"; r();l(); bookmark "Satz24B"; ThmCut "Satz24"; Done(); l();l(); ThmCut "Satz10C"; Triv 3 1; UseThm "Satz11" [1][1]; UseThm "OneNat" nil [1]; gl2 3; rwl nil; ThmCut "Satz10A"; Triv 2 1;UseThm "OneNat" nil [1]; ProveMarked "Satz24B" "Satz24B"; (* Satz25 *) (* Aug. 9, number 2 *) Start "a1ENat&a2ENat&a1>a2->a1>=a2+1"; r();l();Gl 2; l(); bookmark "Satz25"; Gl 2;l();gl 2; rwr nil; ThmCut2 "Satz23"; Done(); r();r();Gr 2; ThmCut2 "Satz24"; Done(); Triv 4 1; Triv 3 1; Triv 3 1; Triv 4 1; UseThm "OneNat" nil [1]; ProveMarked "Satz25" "Satz25"; (* Satz26 *) (* Aug. 9, number 3 *) Start "a1ENat&a2ENat&a2a2<=a1"; r();l();Gl 2; bookmark "Satz26"; Gl 2;l(); Cut "a2<=a1va2>a1"; r();r();r();Gr 4; r(); ThmCut2 "Satz10E"; Triv 1 5; Done(); Triv 1 2; Triv 4 1; Triv 3 1; l(); Done(); Cut "a2+a3>a1+1"; ThmCut2 "Satz22B"; Done(); Done(); UseThm "Satz24" [2][1]; Triv 5 1; Triv 4 1; Triv 2 1; UseThm "OneNat" nil [1]; gl 4; gl2 4; rwl nil; ThmCut "Satz10B"; Triv 2 1; UseThm "SumNat" [6,4] [1]; ProveMarked "Satz26" "Satz26"; (* Satz27 *) (* the well-ordering principle... *) Start "a1ENat&a1Ea2->(Ex1:Nat.x1Ea2&(Ax2:Nat.x2Ea2->x2>=x1))"; r();l(); bookmark "Satz27"; ThmCut "Induction"; su 3 "{x1:Nat|(Ax2:Nat.x2<=x1->~x2Ea2)v(Ex2:Nat.x2<=x1&x2Ea2&(Ax3:Nat.x3Ea2->x3>=x2))}"; r(); UseThm "OneNat" nil [1]; r(); r(); r(); r(); Gl 2; l(); UseThm "Satz24B" [2,1] nil; gl2 5; rwl nil; Gr 2; UseThm "OneNat" nil [1]; r(); Triv 2 1; r(); r(); UseThm "Satz24" [2] [1]; r();r();l(); r(); UseThm "SuccNat" [1][1]; r(); r(); r(); r(); Gl 5; Gl 6; l(); ThmCut "Satz26"; Done(); Triv 5 1; Triv 2 1; Gl 5; Triv 8 1; l(); Triv 6 1; l(); Triv 5 1; Gr 2; Triv 2 1; r(); Triv 8 1; r(); r(); Gl 6; Triv 7 1; l(); gl 8; gr 2; rwr nil; ThmCut2 "Satz10E"; su 10 "a9"; su 11 "a7"; ThmCut2 "Satz25"; Done(); Done(); Triv 6 1; Gr 4; r(); Done(); Gr 4; r(); Triv 1 2; Triv 10 1; Triv 3 1; l(); Triv 6 1; (* Done(); *) l(); r(); Done(); r(); Gl 2; Cut "a7 <= a7+1"; r();r();r();r();sg();r();UseThm "OneNat" nil [1]; ThmCut2 "Satz17"; Done(); Triv 2 1; Done(); Triv 11 1; Gl 2; Triv 2 1; Done(); l(); Gl 2; l(); sg(); l(); r(); r(); Gr 2; l(); Triv 3 1; Triv 4 1; (* Done(); *) l(); r(); sg(); r(); Gl 2; Gl 2; Done(); Gl 2; Gl 2; Triv 2 1; Done(); ProveMarked "Satz27" "Satz27"; (* the axioms for multiplication appear above *) (* two lemmas implicit in Landau's Satz 28 are needed *) (* lemma on left multiplication by one *) Start "a1ENat->1*a1=a1"; r(); bookmark "OneTimesComm"; ThmCut "Induction"; su 2 "{x1:Nat|1*x1=x1}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "TimesOne"; Done(); UseThm "OneNat" nil [1]; r(); r(); l(); r(); UseThm "SuccNat" [1][1]; ThmCut2 "TimesSucc"; rwr nil; gl 3; rwr nil; r(); UseThm "OneNat" nil [1]; Done();Done();l();Triv 2 1; ProveMarked "OneTimesComm" "OneTimesComm"; (* closure property of multiplication, not given as an axiom but is provable *) Start "a1ENat&a2ENat->a1*a2ENat"; r();l(); bookmark "TimesNat"; ThmCut "Induction"; su 3 "{x1:Nat|a1*x1ENat}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "TimesOne"; rwr nil; Triv 2 1; Done(); r(); r(); l(); r(); UseThm "SuccNat" [1][1]; ThmCut2 "TimesSucc"; rwr nil; ThmCut2 "SumNat"; Done(); Triv 3 1;Triv 5 1;Triv 4 1;Done(); Triv 2 1;l();Triv 2 1; ProveMarked "TimesNat" "TimesNat"; (* lemma on left multiplication by a successor *) Start "a1ENat&a2ENat->[a1+1]*a2=a1*a2+a2"; r();l(); bookmark "LeftTimesSucc"; ThmCut "Induction"; su 3 "{x1:Nat|[a1+1]*x1=a1*x1+x1}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "TimesOne"; rwr nil; ThmCut2 "TimesOne"; rwr nil; r(); Triv 2 1;UseThm "SuccNat" [1][1]; r();r();l();r();UseThm "SuccNat" [1][1]; ThmCut2 "TimesSucc"; rwr nil; ThmCut2 "TimesSucc"; rwr nil; gl 4; rwr nil; ThmCut2 "Satz5"; rwr nil; ThmCut2 "Satz5"; crwr [2]; ThmCut2 "Satz6"; rwr [3]; ThmCut2 "Satz5"; rwr nil;ThmCut2 "Satz5"; rwr nil;r(); ThmCut2 "TimesNat"; Done(); Triv 7 1; Triv 11 1; Triv 7 1; UseThm "SuccNat" [11][1]; Triv 6 1; Triv 10 1; UseThm "OneNat" nil [1]; Triv 9 1;Triv 5 1;Triv 8 1;Triv 4 1;UseThm "OneNat" nil [1]; ThmCut2 "TimesNat"; Done();Triv 3 1;Triv 7 1;Triv 7 1; UseThm "SuccNat" [3] [1];Triv 5 1;Triv 4 1;UseThm "SuccNat" [4] [1]; Done(); Triv 2 1; l(); Triv 2 1;Done(); ProveMarked "LeftTimesSucc" "LeftTimesSucc"; (* Satz 29 *) Start "a1ENat&a2ENat->a1*a2=a2*a1"; r();l(); bookmark "Satz29"; ThmCut "Induction"; su 3 "{x1:Nat|x1*a2=a2*x1}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "TimesOne"; rwr nil; ThmCut2 "OneTimesComm"; rwr nil; r(); Triv 3 1; Triv 2 1; r();r();r(); UseThm "SuccNat" [2][1]; l(); ThmCut2 "TimesSucc"; rwr nil; ThmCut2 "LeftTimesSucc"; rwr nil; gl 4; rwr nil; r(); Triv 4 1;Triv 6 1;Triv 5 1;Done();Done();l();Triv 2 1; ProveMarked "Satz29" "Satz29"; (* Satz 30 *) s "a1ENat&a2ENat&a3ENat->a1*[a2+a3]=a1*a2+a1*a3"; r();l();Gl 2; bookmark "Satz30"; ThmCut "Induction"; su 4 "{x1:Nat|x1*[a2+a3]=x1*a2+x1*a3}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "OneTimesComm"; rwr nil; ThmCut2 "OneTimesComm"; rwr nil; ThmCut2 "OneTimesComm"; rwr nil; r(); Triv 4 1;Triv 2 1; UseThm "SumNat" [1,2] [1]; r();r();l();r(); UseThm "SuccNat" [1] [1]; ThmCut2 "LeftTimesSucc"; rwr nil; ThmCut2 "LeftTimesSucc"; rwr nil; ThmCut2 "LeftTimesSucc"; rwr nil; gl 5; rwr nil; (* from this point it is algebraic calculation, which is irritating *) ThmCut2 "Satz5"; rwr nil; ThmCut2 "Satz5"; crwr [2]; ThmCut2 "Satz6"; rwr [3]; ThmCut2 "Satz5"; rwr nil; ThmCut2 "Satz5"; rwr nil;r(); (* now comes a block of type checking -- this needs to be automated *) UseThm "TimesNat" [13,7] [1]; Triv 7 1; ThmCut2 "SumNat"; Done(); UseThm "TimesNat" [13,8] [1]; Triv 8 1; Triv 6 1; UseThm "TimesNat" [12,7] [1]; Triv 7 1; UseThm "TimesNat" [11,6] [1]; Triv 5 1; UseThm "TimesNat" [10,5] [1]; Triv 4 1; Triv 5 1; UseThm "TimesNat" [9,3] [1]; UseThm "TimesNat" [9,4] [1]; UseThm "SumNat" [3,4] [1]; Triv 5 1; Triv 7 1; Triv 4 1; Triv 5 1; Done(); UseThm "SumNat" [4,5] [1]; Triv 3 1;l();Triv 2 1; ProveMarked "Satz30" "Satz30"; (* Satz30B -- left distributivity *) s "a1ENat&a2ENat&a3ENat->[a1+a2]*a3=a1*a3+a2*a3"; r();l();Gl 2; bookmark "Satz30B"; ThmCut2 "Satz29";rwr nil; ThmCut2 "Satz30";rwr nil; ThmCut2 "Satz29";rwr nil; ThmCut2 "Satz29";rwr [2];r(); Triv 5 1;Triv 4 1;Triv 4 1;Triv 5 1;Triv 4 1;Triv 2 1;Triv 3 1; UseThm "SumNat" [3,1] [1];Triv 2 1; ProveMarked "Satz30B" "Satz30B"; (* Satz31: associativity of multiplication *) s "a1ENat&a2ENat&a3ENat->[a1*a2]*a3=a1*a2*a3"; r();l();Gl 2; bookmark "Satz31"; ThmCut "Induction"; su 4 "{x1:Nat|[a1*a2]*x1=a1*a2*x1}"; r(); UseThm "OneNat" nil [1]; ThmCut2 "TimesOne"; rwr nil; ThmCut2 "TimesOne"; rwr nil;r(); Triv 2 1; UseThm "TimesNat" [3,1] [1]; r();r();r();l(); UseThm "SuccNat" [1] [1]; l(); ThmCut2 "TimesSucc"; rwr nil; ThmCut2 "TimesSucc"; rwr nil; gl 4; rwr nil; ThmCut2 "Satz30"; rwr nil;r(); UseThm "TimesNat" [3,8] [1]; Triv 3 1;Triv 5 1;Triv 5 1;Triv 4 1; UseThm "TimesNat" [6,4] [1]; Triv 3 1; Triv 2 1;l();Triv 2 1; ProveMarked "Satz31" "Satz31"; (* Satz32 -- three versions *) s "a1ENat&a2ENat&a3ENat->a1>a2->a1*a3>a2*a3"; r();l();Gl 2;r(); bookmark "Satz32A"; l();l();gl 2;rwr nil; ThmCut2 "Satz30B"; rwr nil; r();r();sg();r(); UseThm "TimesNat" [6,4] [1]; Triv 5 1;Triv 3 1;Triv 2 1; ProveMarked "Satz32A" "Satz32A"; s "a1ENat&a2ENat&a3ENat->a1=a2->a1*a3=a2*a3"; r();l();Gl 2;r(); bookmark "Satz32B"; rwr nil; r(); ProveMarked "Satz32B" "Satz32B"; (* this is trivial of course *) s "a1ENat&a2ENat&a3ENat->a1a1*a3a1*a3>a2*a3->a1>a2"; r();l();Gl 2;r(); bookmark "Satz33A"; s "a1ENat&a2ENat&a3ENat->a1*a3=a2*a3->a1=a2"; r();l();Gl 2;r(); bookmark "Satz33B"; s "a1ENat&a2ENat&a3ENat->a1*a3a1a1>a2&a3>a4->a1*a3>a2*a4"; (* Satz 34B *) s "a1ENat&a2ENat&a3ENat&a4ENat->a1a1*a3a1>=a2&a3>a4->a1*a3>a2*a4"; (* Satz35B *) s "a1ENat&a2ENat&a3ENat&a4ENat->a1>a2&a3>=a4->a1*a3>a2*a4"; (* Satz35C *) s "a1ENat&a2ENat&a3ENat&a4ENat->a1<=a2&a3a1*a3a1a1*a3a1>=a2&a3>=a4->a1*a3>=a2*a4"; (* Satz 36B *) s "a1ENat&a2ENat&a3ENat&a4ENat->a1<=a2&a3<=a4->a1*a3<=a2*a4"; (* this completes Landau Chapter I *)