(* master file for Joanna Guild's potential project *) (* version information: this is version of Dec. 27 with corrected axiom SUP1 (the condition that the set be nonempty was not included) Note also new lemma NOTBOTH3 for order contradictions (variant of NOTBOTH2 for when the equation is in other order) *) (* Joanna, look for comments marked with COMMENT: *) (* warning: this version of the file requires marcelsequent version of Nov. 21 or later *) (* early parts use the legacy oldrwl, oldcrwl commands but later parts use new version. The new ThmCut command is demonstrated in the last proof (along with SetUnknown (su) an old but so far unadvertised command) *) (* test what I can do and what upgrades are needed *) (* clearly for analysis or arithmetic the infix function upgrade is a requirement. This will need special identifiers, followed by infix binary functions with precedence. This is the last major upgrade envisaged for this term. *) (* consider a second-order logic restriction (two type stratification -- is it that simple?) *) (* it might be a good time to implement the fairly simple set/class version. The set/class version might be fine in place of stratified SOL; axioms that say that only real numbers are elements are not problematic. The further advantage is that one could then explore axiomatic set theory. *) (* another idea: could I build in typed variables -- use other series of variables like r1, r2... as variables of a declared type, with modifications obvious for restricted quantification, assertions that r1 belongs to the appopriate type, etc.? *) (* clearly some kind of improved equational reasoning will be needed; rewriting with universally quantified premises or with theorems? *) (* axioms should be checked for declarations, just like definitions *) (* numerals as names would be convenient at this point *) (* problem with usefulness of rewrite left commands: not enough freedom to reorder propositions on the left. Solution: supply an argument for the equation to rewrite the first proposition on left with? No, fixed this by supplying additional commands for moving formulas to second position. *) (* of course only the right rule is actually needed in theory *) (* create declaration and definition commands with no visible types *) (* description and axiom of choice *) (* COMMENT: (Dec 26) The operator An allows you to choose an element from any nonempty set; the axiom AN is a version of the Axiom of Choice *) DefineTerm "An(x1)" "An(x1)" [0,1]; Axiom "AN" ["a2 E a1"] ["An(a1) E a1"]; (* declarations and axioms for an ordered field *) (* primitive notions *) DefineProp "Real(x1)" "Real(x1)" [0]; DefineTerm "Zero" "Zero" [0]; DefineTerm "One" "One" [0]; DefineTerm "+(x1,x2)" "+(x1,x2)" [0,0,0]; DefineTerm "*(x1,x2)" "*(x1,x2)" [0,0,0]; setprecrightabove "*" "+"; DefineProp "<(x1,x2)" "<(x1,x2)" [0,0]; DefineTerm "Minus(x1)" "Minus(x1)" [0,0]; DefineTerm "Inv(x1)" "Inv(x1)" [0,0]; DefineTerm "Sup(x1)" "Sup(x1)" [0,1]; (* axioms *) (* outputs of all our operations are real *) Axiom "RPLUS" nil ["Real(+(a1,a2))"]; Axiom "RTIMES" nil ["Real(*(a1,a2))"]; Axiom "RMINUS" nil ["Real(Minus(a1))"]; Axiom "RINV" nil ["Real(Inv(a1))"]; Axiom "RSUP" nil ["Real(Sup(a1))"]; (* commutative laws *) Axiom "CPLUS" nil ["+(a1,a2)=+(a2,a1)"]; Axiom "CTIMES" nil ["*(a1,a2)= *(a2,a1)"]; (* associative laws *) Axiom "APLUS" nil ["+(+(a1,a2),a3)=+(a1,+(a2,a3))"]; Axiom "ATIMES" nil ["*(*(a1,a2),a3)= *(a1, *(a2,a3))"]; (* distributive law *) Axiom "DIST" nil ["a1*[a2+a3]=a1*a2+a1*a3"]; (* identity laws -- these do not take quite the expected form due to the coercion of arbitrary arguments to real numbers *) Axiom "IPLUS" nil ["Real(a1)-> +(a1,Zero)=a1"]; Axiom "ITIMES" nil ["Real(a1)-> *(a1,One)=a1"]; (* defines the relation "coerced to the same real" *) DefineProp "Equal(x1,x2)" "+(x1,Zero)=+(x2,Zero)" [0,0]; (* inverse laws *) Axiom "MINUS" nil ["+(a1,Minus(a1))=Zero"]; Axiom "INV" nil ["Equal(a1,Zero) v *(a1,Inv(a1))=One"]; (* otherwise we could have a model with one inhabitant, Zero *) Axiom "NONTRIV" nil ["~Equal(Zero,One)"]; (* basic properties of strict linear order *) Axiom "IRR" nil ["~<(a1,a1)"]; Axiom "TRI" nil ["Equal(a1,a2) v <(a1,a2) v <(a2,a1)"]; Axiom "TRANS" nil ["a1 < a2 & a2 < a3 -> a1 < a3"]; (* monotonicity properties of order *) Axiom "MPLUS0" nil ["<(a1,a2)==<(+(a1,a3),+(a2,a3))"]; s "a1 a1+a3 <(*(a1,a3), *(a2,a3))"]; (* define less than or equal to *) DefineProp "<=(x1,x2)" "Equal(x1,x2) v <(x1,x2)" [0,0]; (* the least upper bound property in two parts *) (* COMMENT: Dec 27 corrected error in statement of SUP1 -- the set a1 needs to be nonempty! *) Axiom "SUP1" nil ["(Ex1.x1Ea1)&(Ax1.x1Ea1->x1 <= a2)-> Sup(a1) <= a2"]; Axiom "SUP2" nil ["(Ax1.x1Ea1->x1 <= a2) -> (Ax1.x1Ea1->x1 <= Sup(a1))"]; (* I already have a couple of comments: note that this uses strict less than instead of less than or equal to, except in the supremum axioms. The forms of these axioms do not take advantage of the freedom to give complex sequents as axioms; I should fix this. *) (* also these axioms are wrong unless I restrict the logic, because they don't include needed hypotheses that objects are reals FIXED The way to understand the restrictions is to think of every argument of one of our operations (except the set argument in Sup) as being coerced to a real, while of course all operations give real output. Then everything should make sense (this minimizes the need to mention reals in algebraic laws to just a mention in the identity laws). The relation Equal holds between two objects iff they are coerced to the same real; this way of expressing the axioms minimizes assumptions about how the coercion works. The reason that all this is needed is that the underlying logic of the prover is strong enough to show that the universe is larger than the set of all reals. *) (* log file of a sample proof inserted *) (* commented out because didn't have domain restrictions in axioms (* 1 *) Start "+(a1,a2)=a2 == a1=Zero"; (* 2 *) r(); r(); r(); Cut "+(+(a1,a2),Minus(a2))=+(a2,Minus(a2))"; (* 6 *) Cut "+(a2,Minus(a2))=Zero"; (* 7 *) gl 2; gl2 3; oldrwl ~1; crwr ~1; (* 12 *) Cut "+(+(a1,a2),Minus(a2))=+(a1,+(a2,Minus(a2)))"; (* 13 *) rwr ~1; gl 3; rwr ~1; Cut "+(a1,Zero)=a1"; (* 17 *) rwr ~1; Reflexiveeq(); (* 19 *) UseThm "IPLUS" [] [1]; (* 20 *) UseThm "APLUS" [] [1]; (* 21 *) UseThm "MINUS" [] [1]; (* 22 *) rwr ~1; Reflexiveeq(); (* 24 *) r(); rwr ~1; Cut "+(Zero,a2)=+(a2,Zero)"; (* 27 *) rwr ~1; UseThm "IPLUS" [] [1]; (* 29 *) UseThm "CPLUS" [] [1]; (* 30 *) *) (* (* dud theorem -- domain conditions not enough (* 1 *) Start "; (* 2 *) r(); r(); r(); r(); Cut2 "Real(+(a1,a2))"; UseThm "RPLUS" [] [1]; (* 8 *) coldrwl ~1; Undo(); oldrwl ~1; Done(); (* 12 *) Cut2 "+(+(a1,a2),Minus(a1))=+(a1,Minus(a1))"; rwr ~1; Reflexiveeq(); (* 15 *) Cut "+(a1,Minus(a1))=Zero"; (* 16 *) gl 2; gl2 3; oldrwl ~1; Cut2 "+(a1,a2)=+(a2,a1)"; UseThm "CPLUS" [] [1]; (* 21 *) gl 2; gl2 4; oldrwl ~1; Cut2 "+(+(a2,a1),Minus(a1))=+(a2,+(a1,Minus(a1)))"; UseThm "APLUS" [] [1]; (* 26 *) gl 2; gl2 5; oldrwl ~1; gl2 4; oldrwl ~1; r(); *) startlogging "guildtest"; Start "Real(a1)&Real(a2)->(+(a1,a2)=a1==a2=Zero)"; *) (* Here is the proof that works with the theorem stated correctly *) (* 1 *) Start "Real(a1)&Real(a2)->(+(a1,a2)=a1==a2=Zero)"; (* 2 *) r(); l(); r(); r(); r(); Cut2 "+(+(a1,a2),Minus(a1))=+(a1,Minus(a1))"; rwr ~1; Reflexiveeq(); (* 10 *) Cut2 "+(a1,Minus(a1))=Zero"; UseThm "MINUS" [] [1]; (* 12 *) gl 2; gl2 5; oldrwl ~1; Cut "+(+(a1,a2),Minus(a1))=a2"; (* 16 *) gl 2; gl2 6; oldrwl ~1; Done(); (* 20 *) Cut2 "+(a1,a2)=+(a2,a1)"; UseThm "CPLUS" [] [1]; (* 22 *) gl 2; gl2 6; oldrwl ~1; Cut2 "+(+(a2,a1),Minus(a1))=+(a2,+(a1,Minus(a1)))"; UseThm "APLUS" [] [1]; (* 27 *) gl2 4; oldrwl ~1; Cut2 "Real(a2)->+(a2,Zero)=a2"; UseThm "IPLUS" [] [1]; (* 31 *) l(); gl 5; gr 1; Done(); (* 35 *) gl 2; gl2 8; rwr ~1; oldrwl ~1; gl 8; rwr ~1; gl 8; gr 1; (* 44 *) gl 3; gr 1; Done(); (* 47 *) r(); rwr ~1; Cut2 "Real(a1)->+(a1,Zero)=a1"; r(); Undo(); UseThm "IPLUS" [] [1]; (* 53 *) l(); gl 2; gr 1; Done(); (* 57 *) Done(); (* 58 *) NameSequent 3 "NULLADD"; (* demo with ThmCut *) (* create the "sequent" form of IPLUS *) s "Real(a1)->+(a1,Zero)=a1"; r(); ThmCut "IPLUS";l(); (* su 2 "a1"; *) Done();Done(); NameSequent 2 "IPLUSa"; (* now reprove the theorem above *) (* startlogging "newtest"; Start "Real(a1)&Real(a2)->(+(a1,a2)=a1==a2=Zero)"; r();l();r();r();r(); Cut2 "+(+(a1,a2),Minus(a1))=+(a1,Minus(a1))"; rwr ~1; re(); ThmCut "MINUS"; (* su 3 "a1"; *) (* this is where the mystery match error showed up *) rwl ~1; ThmCut "CPLUS"; (* su 4 "a1"; su 5 "a2"; *) gl2 3; rwl 2; (*change this to 2 from ~1 with automatic unknowns *) ThmCut "APLUS"; (* su 6 "a2"; su 7 "a1"; su 8 "Minus(a1)"; *) gl2 3; rwl ~1; gl 6; gl2 4; rwl ~1; ThmCut "IPLUSa"; (* su 9 "a2"; *) gl2 3; rwl ~1; Triv 2 1; Triv 5 1; r(); rwr ~1; UseThm "IPLUSa" [2] [1]; stoplogging(); *) (* a trivial lemma (smilie) *) s "a1=a1"; re(); NameSequent 1 "TRIV"; (* (* commented out proof above and replaced with its log: *) startlogging "test"; (* 1 *) Start "Real(a1)&Real(a2)->(+(a1,a2)=a1==a2=Zero)"; (* 2 *) r(); l(); r(); r(); r(); ThmCut "TRIV"; su 3 "+(a1,Minus(a1))"; gl 2; gl2 4; crwl 1; (* 10 *) ThmCut "MINUS"; (* 11 *) (*SetUnknown 4 "a1";*) gl2 3;rwl ~1; ThmCut "CPLUS"; (* 14 *) (*SetUnknown 5 "a1"; SetUnknown 6 "a2";*) gl2 3; rwl 2; ThmCut "APLUS"; (* 19 *) (*SetUnknown 7 "a2"; SetUnknown 8 "a1"; SetUnknown 9 "Minus(a1)";*) gl2 3; rwl ~1; gl 6; gl2 4; rwl ~1; ThmCut "IPLUSa"; (* 28 *) (*SetUnknown 10 "a2";*) gl2 3; rwl ~1; gl 2; gr 1; Done(); (* 34 *) gl 4; gr 1; Done(); (* 37 *) r(); rwr ~1; UseThm "IPLUSa" [2] [1]; (* 40 *) stoplogging(); *) (* 1 *) Start "Real(a1)&Real(a2)->(+(a1,a2)=a1==a2=Zero)"; (* 2 *) r(); l(); r(); r(); r(); ThmCut "TRIV"; (* note the sneaky way I avoided typing out the whole first cut formula using TRIV *) (* the command crwl 1 does converse left rewrite in the first position where the right side of the equation appears, only *) (* 8 *) su 3 "+(a1,Minus(a1))"; gl 2; gl2 4; crwl 1; ThmCut "MINUS"; (* 13 *) (* su 4 "a1"; *) gl2 3; rwl 2; ThmCut "CPLUS"; (* 17 *) (* su 5 "a1"; su 6 "a2"; *) gl2 3; rwl 2; ThmCut "APLUS"; (* 22 *) (* su 7 "a2"; su 8 "a1"; su 9 "Minus(a1)"; *) gl2 3; rwl ~1; gl 6; gl2 4; rwl ~1; ThmCut "IPLUSa"; (* 31 *) (* su 10 "a2"; *) gl2 3; rwl 1; gl 2; gr 1; Done(); (* 37 *) gl 4; gr 1; Done(); (* 40 *) r(); rwr ~1; UseThm "IPLUSa" [2] [1]; (* 43 *) (* work on x^2 >= 0 *) (* proof plan: x>0 or x=0 or x <0 (TRI). if x>0 this is easy (MTIMES) if x=0 prove x^2=0 -- use x*0 = 0 if x<0 use reversed form of MTIMES *) ss ["P1","P1->P2"] ["P2"]; Gl 2; Done(); Done(); NameSequent 1 "MP"; s "Real(Zero)"; ThmCut "MINUS"; crwr ~1; UseThm "RPLUS" nil [1]; NameSequent 1 "RZERO"; s "a1*Zero = Zero"; Cut "a1*Zero+a1*Zero=a1*Zero"; ThmCut "NULLADD"; (* su 2 "a1*Zero"; su 3 "a1*Zero"; *) l();l(); UseThm "MP" [1,3][1]; UseThm "RTIMES" nil [1]; UseThm "RTIMES" nil [1]; ThmCut "DIST"; (* su 4 "a1"; su 5 "Zero"; su 6 "Zero"; *) crwr ~1; ThmCut "IPLUS"; l(); (* su 7 "Zero"; *) (* omitting this su causes program to hang *) (* the version with automatic subs hangs on this matching if I don't use su here -- why? *) UseThm "RZERO" nil [1]; rwr ~1; re(); NameSequent 1 "MZERO"; (* at this point I saw that i neededto prove 0 real (appears above)*) s "Real(a2)&a1 + a2 = Zero -> a2 = Minus(a1)"; ThmCut "CPLUS"; su 3 "a1"; su 4 "a2"; rwr ~1; r(); l(); ThmCut "TRIV"; su 5 "[a2 + a1]+Minus(a1)"; gl 3;gl2 3; rwl 2; ThmCut "CPLUS"; su 6 "Zero"; su 7 "Minus(a1)"; ThmCut "IPLUS"; su 8 "Minus(a1)"; l(); UseThm "RMINUS" nil [1]; rwl ~1; gl 2; gl2 3; rwl ~1; ThmCut "APLUS"; su 9 "a2"; su 10 "a1"; su 11 "Minus(a1)"; gl2 3; rwl ~1; ThmCut "MINUS"; su 12 "a1"; gl2 3; rwl ~1; ThmCut "IPLUS"; su 13 "a2"; l(); Triv 3 1; gl2 3; rwl ~1; Triv 2 1; (* this isn't the ideal form but the way I did the proof didn't serve up the form I wanted *) NameSequent 1 "UNIQUEINV"; ss ["Real(a2)","a1+a2=Zero"] ["a2=Minus(a1)"]; ThmCut "UNIQUEINV";su 3 "a1"; su 4 "a2"; l();r();Done(); Triv 2 1; Done(); NameSequent 1 "UINV"; s "Real(a1)->Zero+a1=a1"; r(); ThmCut "CPLUS"; su 2 "Zero"; su 3 "a1"; rwr ~1; ThmCut "NULLADD"; su 4 "a1"; su 5 "Zero"; l();l(); Cut2 "Zero=Zero"; re(); UseThm "MP" [3,1] [1]; Triv 2 1; UseThm "RZERO" nil [1]; NameSequent 2 "IPLUSb"; s "Minus(a1)+a1=Zero"; ThmCut "CPLUS"; su 2 "Minus(a1)"; su 3 "a1"; rwr ~1; UseThm "MINUS" nil [1]; NameSequent 1 "MINUS2"; s "a1 < a2 == Minus(a2) < Minus(a1)"; r();r(); ThmCut "MPLUS"; su 3 "a1"; su 4 "a2"; su 5 "Minus(a1)+Minus(a2)"; r();Gl 2; Done(); ThmCut "APLUS"; su 6 "a1"; su 7 "Minus(a1)"; su 8 "Minus(a2)";crwl ~1; ThmCut "MINUS"; su 9 "a1"; gl2 3; rwl ~1; ThmCut "IPLUSb"; su 10 "Minus(a2)"; gl2 3; rwl ~1; gl 2; ThmCut "CPLUS"; su 11 "Minus(a1)"; su 12 "Minus(a2)"; rwl ~1; ThmCut "APLUS"; su 13 "a2"; su 14 "Minus(a2)"; su 15 "Minus(a1)"; gl2 3; crwl ~1; ThmCut "MINUS"; su 16 "a2"; gl2 3; rwl ~1; ThmCut "IPLUSb"; su 17 "Minus(a1)"; gl2 3; rwl ~1; Triv 2 1; UseThm "RMINUS" nil [1]; UseThm "RMINUS" nil [1]; r();ThmCut "MPLUS"; su 18 "Minus(a2)"; su 19 "Minus(a1)"; su 20 "a1+a2";l();Done(); Cut "Minus(a2)+a1+a2=a1+Zero"; rwl ~1; gl 2;Cut "Minus(a1)+a1+a2=a2+Zero"; rwl ~1; ThmCut "MPLUS0"; su 21 "a1"; su 22 "a2"; su 23 "Zero"; l();l(); UseThm "MP" [2,4] [1]; ThmCut "APLUS"; su 24 "Minus(a1)"; su 25 "a1"; su 26 "a2"; crwr ~1; ThmCut "MINUS2"; su 27 "a1"; rwr ~1; UseThm "CPLUS" nil [1]; ThmCut "CPLUS"; su 28 "Minus(a2)"; su 29 "a1+a2"; rwr ~1; ThmCut "APLUS"; su 30 "a1"; su 31 "a2"; su 32 "Minus(a2)"; rwr ~1; ThmCut "MINUS"; su 33 "a2"; rwr ~1; re(); NameSequent 1 "MINUSLESS"; (* Guild proofs begin here *) (* Equality *) (* 1 *) Start "Real(a1)&Real(a2)& Equal(a1,a2) -> a1 =a2"; (* 2 *) r(); l(); gl 2; l(); gl 2; l(); ThmCut "IPLUS"; (* 9 *) su 3 "a1"; l(); gl 2; Done(); (* 13 *) rwl ~1; ThmCut "IPLUS"; (* 15 *) su 4 "a2"; l(); gl 4; Done(); (* 19 *) gl2 3; rwl ~1; gl 2; Done(); (* 23 *) (* 22 EQUALITY: 1: a1 Equal a2 2: Real(a1) 3: Real(a2) |- 1: a1 = a2 *) NameSequent 4 "EQUALITY"; (* 24 *) (* If number neg, opp is pos*) (* 1 *) Start "Real(a1) & a1 < Zero -> Zero < Minus(a1)"; (* 2 *) r(); l(); ThmCut "MINUS"; (* 5 *) su 2 "a1"; Cut "a1 + Minus(a1) < [a1 + Minus(a1)] + Minus(a1)"; (* 7 *) gl 2; gl2 4; rwl ~1; ThmCut "CPLUS"; (* 11 *) su 3 "Zero"; su 4 "Minus(a1)"; gl2 3; rwl ~1; ThmCut "IPLUSa"; (* 16 *) su 5 "Minus(a1)"; gl2 3; rwl ~1; gl 2; Done(); (* 21 *) UseThm "RMINUS" [] [1]; (* 22 *) ThmCut "MPLUS"; (* 23 *) su 6 "a1"; su 7 "a1+Minus(a1)"; su 8 "Minus(a1)"; l(); rwr ~1; gl 3; Done(); (* 30 *) Done(); (* 31 *) (* 30 NEGINEQ: 1: a1 < Zero |- 1: Zero < Minus(a1) *) NameSequent 3 "NEGINEQ"; (* 32 *) (* This shows x(-y) = -(xy)*) (* 1 *) Start "Real(a1)&Real(a2) ->a1 * Minus(a2)=Minus(a1*a2)"; (* 2 *) l(); r(); l(); Cut "a1*a2+a1*Minus(a2)=Zero"; (* 6 *) ThmCut "DIST"; (* 7 *) su 3 "a1"; su 4 "a2"; su 5 "Minus(a2)"; rwl ~1; Undo(); crwl ~1; ThmCut "MINUS"; (* 14 *) su 6 "a2"; rwl 1; ThmCut "MZERO"; (* 17 *) su 7 "a1"; gl2 3; rwl ~1; ThmCut "UINV"; (* 21 *) su 9 "a1*Minus(a2)"; su 8 "a1*a2"; Done(); (* 24 *) UseThm "RTIMES" [] [1]; (* 25 *) gl 2; rwr ~1; Reflexiveeq(); (* 28 *) ThmCut "DIST"; (* 29 *) su 10 "a1"; su 11 "a2"; su 12 "Minus(a2)"; crwr ~1; ThmCut "MINUS"; (* 34 *) su 13 "a2"; rwr ~1; ThmCut "MZERO"; (* 37 *) su 14 "a1"; Done(); (* 39 *) (* 38 NEGCOMM: |- 1: a1 * Minus(a2) = Minus(a1 * a2) *) NameSequent 3 "NEGCOMM"; (* 40 *) (*This shows -(-x) = x *) (* 1 *) Start "Real(a1)->Minus(Minus(a1))=a1"; (* 2 *) r(); ThmCut "MINUS"; (* 4 *) su 2 "a1"; ThmCut "CPLUS"; (* 6 *) su 3 "a1"; su 4 "Minus(a1)"; rwl ~1; ThmCut "UINV"; (* 10 *) su 6 "a1"; su 5 "Minus(a1)"; crwr ~1; Reflexiveeq(); (* 14 *) gl 3; Done(); (* 16 *) gl 2; Done(); (* 18 *) (* 17 DOUBLENEG: 1: Real(a1) |- 1: Minus(Minus(a1)) = a1 *) NameSequent 2 "DOUBLENEG"; (* 19 *) (* This shows (-x)(-y) = xy *) (* 1 *) Start "Minus(a1)*Minus(a2)=a1*a2"; (* 2 *) ThmCut "NEGCOMM"; (* 3 *) su 3 "Minus(a1)"; su 4 "a2"; rwr ~1; ThmCut "CTIMES"; (* 7 *) su 5 "Minus(a1)"; su 6 "a2"; rwr ~1; ThmCut "NEGCOMM"; (* 11 *) su 7 "a2"; su 8 "a1"; rwr ~1; ThmCut "CTIMES"; (* 15 *) su 9 "a2"; su 10 "a1"; rwr ~1; ThmCut "DOUBLENEG"; (* 19 *) su 11 "a1*a2"; Done(); (* 21 *) UseThm "RTIMES" [] [1]; (* 22 *) (* 21 TIMESDOUBNEG: |- 1: Minus(a1) * Minus(a2) = a1 * a2 *) NameSequent 1 "TIMESDOUBNEG"; (* 23 *) (* This shows if z<0, x a2*a3 < a1*a3"; (* 2 *) r(); l(); ThmCut "NEGINEQ"; (* 5 *) su 4 "a3"; ThmCut "MINUSLESS"; (* 7 *) su 5 "a1"; su 6 "a2"; l(); l(); l(); l(); gr 2; gl 3; Done(); (* 16 *) Done(); (* 17 *) gl 2; l(); gl 4; Done(); (* 21 *) ThmCut "MTIMES"; (* 22 *) su 9 "Minus(a3)"; su 7 "Minus(a2)"; su 8 "Minus(a1)"; l(); r(); gl 2; Done(); (* 29 *) gl 5; Done(); (* 31 *) ThmCut "TIMESDOUBNEG"; (* 32 *) su 10 "a2"; su 11 "a3"; rwl ~1; ThmCut "TIMESDOUBNEG"; (* 36 *) su 12 "a1"; su 13 "a3"; gl2 3; rwl ~1; gl 2; Done(); (* 46 *) Done(); (* 47 *) (* 46 MTIMESNEG: 1: a3 < Zero 2: a1 < a2 |- 1: a2 * a3 < a1 * a3 *) NameSequent 3 "MTIMESNEG"; (* 48 *) (* s "a1*Minus(a2)=Minus(a1*a2)"; s "Real(a1)->Minus(Minus(a1))=a1"; s "a3 < Zero & a1 a1*a3 < a2*a3"; *) (* Joanna Guild proofs *) (* This shows that the square of a number is non-negative *) (* 1 *) Start "Real(a1) -> Zero <= a1*a1"; (* 2 *) r(); l(); r(); r(); ThmCut "TRI"; (* 7 *) su 2 "a1"; su 3 "Zero"; l(); ThmCut "EQUALITY"; (* 11 *) su 4 "a1"; su 5 "Zero"; rwr ~1; ThmCut "MZERO"; (* 15 *) su 6 "Zero"; rwr ~1; gl 2; rwl ~1; gl 2; Done(); (* 21 *) Done(); (* 22 *) gl 2; Done(); (* 24 *) UseThm "RZERO" [] [1]; (* 25 *) l(); ThmCut "MTIMESNEG"; (* 27 *) su 8 "Zero"; su 9 "a1"; su 7 "a1"; ThmCut "MZERO"; (* 31 *) su 10 "a1"; ThmCut "CTIMES"; (* 33 *) su 11 "a1"; su 12 "Zero"; rwl ~1; gl 2; rwl ~1; gl 2; gr 2; Done(); (* 41 *) Done(); (* 42 *) Done(); (* 43 *) ThmCut "MTIMES"; (* 44 *) su 15 "a1"; su 13 "Zero"; su 14 "a1"; l(); r(); Done(); (* 50 *) Done(); (* 51 *) ThmCut "MZERO"; (* 52 *) su 16 "a1"; ThmCut "CTIMES"; (* 54 *) su 17 "a1"; su 18 "Zero"; rwl ~1; gl 2; rwl ~1; gl 2; gr 2; Done(); (* 62 *) (* 61 SQUARENONNEG: 1: Real(a1) |- 1: Zero <= a1 * a1 *) NameSequent 2 "SQUARENONNEG"; (* Holmes attempt on the square root problem *) s "Zero*a1=Zero"; ThmCut "CTIMES"; rwr ~1; UseThm "MZERO" nil [1]; NameSequent 1 "MZERO2"; s "a1 Equal a2 -> a2 Equal a1"; r();r();l();rwr ~1; re(); NameSequent 2 "EqualSymm"; s "Real(One)"; ThmCut "INV"; ThmCut "NONTRIV"; l();l();UseThm "EqualSymm" [1] [1]; gr 2; crwr ~1; UseThm "RTIMES" nil [1]; NameSequent 1 "REALONE"; s "a1 ~a2 ~a1 ~a2 Zero (a1 x3+One E x2) -> x1 E x2)}" nil; (* 1 *) Start "Zero E Nat"; (* 2 *) r(); r(); r(); l(); Done(); (* 7 *) (* 6 ZeroNat: |- 1: Zero E Nat *) NameSequent 1 "ZeroNat"; (* 8 *) (* 8 *) Start "a1 E Nat -> a1 + One E Nat"; (* 9 *) r(); l(); r(); r(); w "a2"; (* 14 *) r(); gl 2; l(); gl 2; gr 1; Done(); (* 20 *) gl 3; l(); gl 2; (* w "a2"; (* 24 *) Undo(); *) w "a1"; (* 26 *) l(); gl 2; gr 1; Done(); (* 30 *) Done(); (* 31 *) NameSequent 2 "NatClosed"; (* 31 *) Start "a1 E Nat -> Real(a1)"; (* 32 *) r(); l(); w "{x1|Real(x1)}"; (* 35 *) l(); r(); r(); UseThm "RZERO" [] [1]; (* 39 *) r(); r(); l(); r(); UseThm "RPLUS" [] [1]; (* 44 *) l(); Done(); (* 46 *) NameSequent 2 "NatReal"; (* COMMENT: Dec 26 I still need to look at these *) (* Joanna's proofs *) (* 1 *) Start "Zero E Nat"; (* 2 *) r(); r(); r(); l(); Done(); (* 7 *) (* 1 *) Start "a1 E Nat -> a1 + One E Nat"; (* 2 *) r(); l(); r(); r(); r(); l(); gl 3; w "a2"; (* 10 *) l(); r(); gl 2; gr 1; Done(); (* 15 *) gl 3; gr 1; Done(); (* 18 *) gl 4; w "a1"; (* 20 *) l(); gl 2; gr 1; Done(); (* 24 *) Done(); (* 25 *) (* 1 *) Start "a1 E Nat -> Real(a1)"; (* 2 *) r(); l(); w "{x1 | Real(x1)}"; (* 5 *) l(); r(); r(); ThmCut "RZERO"; (* 9 *) Done(); (* 10 *) r(); r(); l(); r(); ThmCut "RPLUS"; (* 15 *) gl 1; gr 1; Done(); (* 18 *) l(); Done(); (* 20 *) (* COMMENT: Dec 26 Notice these definitions *) (* COMMENT: Dec 26 The built in ordered pair appears here ([x,y] is the pair of x and y; p1([x,y]) = x; p2([x,y]) = y). The pair and its projection operators p1 and p2 have special support in the prover which we will need to discuss. (and of course the pair and its projections, which we haven't used much, may have destructive interactions with recent updates; there may be bugs. I already had to redo the notation for the pair (originally ) to allow us to use < and > as predicates! *) (* the notion of a function defined *) DefineProp "Function(x1,x2)" "(Ax3.x3 E x1 -> p1(x3) E p1(x2) & p2(x3) E p2(x2)) & (Ax3.(Ax4.(Ax5.[x3,x5]Ex1&[x4,x5]Ex1->x3=x4)))" nil; (* the set of all reals *) DefineTerm "Reals" "{x1|Real(x1)}" nil; (* a sequence is a function from the natural numbers to the reals *) DefineProp "Sequence(x1)" "Function(x1,[Nat,Reals])" nil; (* a closure operation; we will use this to develop iterative and recursive definitions of sequences *) DefineTerm "Closure(x1,x2)" "{x3 | (Ax4.x1 E x4 &(Ax5.p1(x5)Ex4 & x5 E x2->p2(x5)Ex4)->x3 E x4)}" nil; (* COMMENT: Dec 26 here I have inserted the set examples file: some more set operations will probably need to be added as we go on *) (* set examples file inserted *) (* this file contains elementary set theory examples *) s "a1 E {x1 | x1=a1}"; r(); (* applying r() (or l()) to a membership statement in an explicitly defined set just makes the obvious substitution *) re(); (* along the same lines *) (* 1 *) Start "a2 E {x1|x1=a1}==a2=a1"; (* 2 *) r(); r(); r(); l(); (* 8 *) Done(); (* 9 *) r(); r(); Done(); (* 12 *) DefineTerm "Union(x1,x2)" "{x3|x3 E x1 v x3 E x2}" nil; s "a1 Union a2 = a2 Union a1"; de(); (* notice that this expands definitions on both sides *) SetEquals(); (* the strategy for proving equality of sets is just what we expect: show that they have the same members *) r();r();r();r();r();l();gr 2; d();d(); (* d() is our old friend Done() *) AutoPrune(); NameSequent 6 "Symmetric"; UseThm "Symmetric" nil [1]; (* the point is that the previous proved sequent 6 (line number found using showall()) matches this sequent; why prove it over again? *) (* note the use of de() and SetEquals() (which can be abbreviated se()); avoid using l() or r() on equations, as always (it does something, but you don't want to mess with it) *) (* the main tools we will use with sets are l() and r() on membership statements with set notation on the right (which just expands out the membership statement in the obvious way) and the SetEquals (se) command to show that sets are equal *) (* the singleton set *) DefineTerm "Sing(x1)" "{x2|x2=x1}" nil; (* the unordered pair *) (* notice that the default use of infix notation has an odd effect here *) DefineTerm "Couple(x1,x2)" "{x3|x3=x1 v x3=x2}" nil; (* the usual definition of the ordered pair; it is not the same as the built-in pair of the logic of the prover *) (* again the infix notation has an odd effect *) DefineTerm "Kpair(x1,x2)" "Couple(Sing(x1),Couple(x1,x2))" nil; (* Here is an exercise: prove the usual theorem about the ordered pair *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* You wrote to me that it was unclear what to do without applying l() and indeed you are right. Here's the way I would usually prove it: the difficulty is that it uses sets like {x1 | a1 E x1} which do not exist in standard set theory (as we showed in one of the problems on the set theory exam *) (* Here is the first part of my proof (showing that a1=a3 follows from Kpair(a1,a2)=Kpair(a3,a4)) *) (* this is still the "old-style" proof -- I fixed it by removing a redundant se() which did nothing in the previous version of the prover but now breaks the proof *) (* I think the solution might be to expand the current SetEquals command to work on the left as well as the right, which is sound and allows one to avoid these odd effects... *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) r(); r(); r(); r(); DefEquals(); DefEquals(); (* SetEquals(); *) l(); w "{x1|Sing(a1) E x1}"; (* 11 *) l(); l(); l(); r(); r(); r(); Reflexiveeq(); (* 18 *) l(); l(); l(); DefEquals(); l(); w "{x1|a1 E x1}"; (* 24 *) l(); l(); l(); r(); r(); Reflexiveeq(); (* 30 *) l(); l(); Done(); (* 33 *) DefEquals(); l(); w "{x1|a3 E x1}"; (* 36 *) l(); l(); gl 2; l(); r(); r(); r(); Reflexiveeq(); (* 45 *) l(); l(); rwr ~1; Reflexiveeq(); (* 49 *) (* the new style proof *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) r(); r(); r(); r(); DefEquals(); DefEquals(); SetEquals(); w "Sing(a1)"; (* 10 *) l(); l(); l(); r(); Reflexiveeq(); (* 15 *) l(); DefEquals(); SetEquals(); w "a1"; (* 19 *) l(); l(); l(); Reflexiveeq(); (* 23 *) Done(); (* 24 *) DefEquals(); SetEquals(); w "a3"; (* 27 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 33 *) rwr ~1; Reflexiveeq(); (* 35 *) (* actually, these (partial) proofs are in overall style quite similar; the only issue is the different handling of equality. *) (* intersection of all elements of x1 *) DefineTerm "Si(x1)" "{x2|(Ax3.x3 E x1 -> x2 E x3)}" nil; (* 1 *) Start "Si(Kpair(a1,a2))=Sing(a1)"; (* 2 *) DefEquals(); SetEquals(); r(); r(); r(); r(); w "Sing(a1)"; (* 9 *) l(); r(); r(); Reflexiveeq(); (* 13 *) l(); Done(); (* 15 *) r(); r(); r(); l(); l(); rwr ~1; r(); gl 2; gr 1; Done(); (* 25 *) l(); Undo(); DefEquals(); rwr ~1; r(); r(); gl 2; gr 1; Done(); (* 34 *) NameSequent 1 "PROJ1"; (* the set of all things which belong to exactly one element of x1 *) DefineTerm "Projtwo(x1)" "{x2|(Ex3.x2 E x3 & x3 E x1)&(Ax3.(Ax4.x2Ex3 & x2Ex4 & x3Ex1 & x4 E x1->x3=x4))}" nil; (* second projection lemma underway *) (* 1 *) Start "Projtwo(Kpair(a1,a2))=Sing(a2)"; (* 2 *) DefEquals(); SetEquals(); r(); r(); r(); r(); l(); l(); l(); gl 2; l(); l(); l(); Undo(); gl2 3; rwl ~1; gl 2; l(); gl 2; w "Sing(a1)"; (* 22 *) w "Couple(a1,a2)"; (* 23 *) l(); r(); r(); gl 4; gr 1; Done(); (* 29 *) r(); r(); r(); gl 4; gr 1; Done(); (* 35 *) r(); DefEquals(); r(); r(); Reflexiveeq(); (* 40 *) r(); r(); gr 2; Reflexiveeq(); (* 44 *) DefEquals(); SetEquals(); w "a2"; (* 47 *) l(); l(); gl 2; r(); Undo(); l(); r(); gr 2; Reflexiveeq(); (* 56 *) rwr ~1; gl 6; gr 1; Done(); (* 60 *) l(); Undo(); gl2 3; rwl ~1; gl 2; l(); l(); gl 2; w "Sing(a1)"; (* 69 *) w "Couple(a1,a2)"; (* 70 *) l(); r(); r(); gl 4; gr 1; Done(); (* 76 *) r(); r(); r(); gl 4; gr 1; Done(); (* 82 *) r(); r(); r(); Reflexiveeq(); (* 86 *) r(); r(); gr 2; Reflexiveeq(); (* 90 *) DefEquals(); SetEquals(); w "a2"; (* 93 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 100 *) rwr ~1; gl 6; gr 1; Done(); (* 104 *) Done(); (* 105 *) r(); rwr ~1; w "Couple(x1,x2)"; (* 108 *) r(); w "Couple(a1,a2)"; (* 110 *) r(); r(); r(); gr 2; Reflexiveeq(); (* 115 *) r(); r(); gr 2; Reflexiveeq(); (* 119 *) r(); r(); r(); l(); gl 2; l(); gl 2; l(); l(); l(); l(); Undo(); gl2 4; rwl ~1; gl 2; l(); gl 5; rwr ~1; gl 4; l(); l(); rwr ~1; Reflexiveeq(); (* 8 *) rwr ~1; DefEquals(); SetEquals(); r(); gl 4; rwr ~1; r(); r(); r(); r(); Done(); (* 19 *) r(); l(); Done(); (* 22 *) Done(); (* 23 *) rwr ~1; gl 2; l(); l(); gl2 4; rwl ~1; gl 2; gl 5; gl 2; l(); gl 5; rwr ~1; DefEquals(); SetEquals(); r(); gl 2; rwr ~1; r(); r(); r(); l(); Done(); (* 45 *) Done(); (* 46 *) r(); r(); Done(); (* 49 *) rwr ~1; Reflexiveeq(); (* 51 *) NameSequent 1 "PROJ2"; (* here is my favorite proof of the main pair theorem *) (* 334 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 335 *) r(); r(); r(); r(); ThmCut "PROJ1"; (* 340 *) su 5 "a1"; su 6 "a2"; gl 2; rwl ~1; ThmCut "PROJ1"; (* 345 *) su 7 "a3"; su 8 "a4"; gl2 3; rwl ~1; gl 2; DefEquals(); SetEquals(); w "a1"; (* 353 *) l(); l(); gl 2; l(); Reflexiveeq(); (* 358 *) Done(); (* 359 *) ThmCut "PROJ2"; (* 360 *) su 9 "a1"; su 10 "a2"; gl 2; rwl ~1; ThmCut "PROJ2"; (* 365 *) su 11 "a3"; su 12 "a4"; gl2 3; rwl ~1; gl 2; DefEquals(); SetEquals(); w "a2"; (* 373 *) l(); l(); gl 2; l(); Reflexiveeq(); (* 378 *) Done(); (* 379 *) l(); r(); l(); rwr ~1; gl 2; rwr ~1; Reflexiveeq(); (* 386 *) (* 385 KPAIR: |- 1: a1 Kpair a2 = a3 Kpair a4 == a1 = a3 & a2 = a4 *) NameSequent 1 "KPAIR"; (* 387 *) (* Joanna's attempted proof *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) r(); r(); r(); r(); DefEquals(); DefEquals(); SetEquals(); w "Sing(a1)"; (* 10 *) l(); l(); l(); r(); Reflexiveeq(); (* 15 *) l(); DefEquals(); SetEquals(); w "a1"; (* 19 *) l(); l(); l(); Reflexiveeq(); (* 23 *) Done(); (* 24 *) DefEquals(); SetEquals(); w "a3"; (* 27 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 33 *) rwr ~1; Reflexiveeq(); (* 35 *) DefEquals(); DefEquals(); SetEquals(); w "a1 Couple a2"; (* 39 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 45 *) l(); DefEquals(); SetEquals(); (* a theorem about equality of unordered pairs *) (* 1 *) Start "Couple(a1,a2)=Couple(a3,a4)==(a1=a3&a2=a4v a1=a4&a2=a3)"; (* 2 *) r(); r(); r(); DefEquals(); SetEquals(); w "a1"; (* 8 *) l(); l(); l(); r(); Reflexiveeq(); (* 13 *) l(); gl 3; w "a2"; (* 16 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 22 *) l(); gl 3; w "a4"; (* 25 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 32 *) l(); rwr ~1; r(); r(); gl 3; gr 1; Done(); (* 39 *) gl 3; rwr ~1; gl 3; gr 1; Done(); (* 44 *) rwr ~1; r(); r(); gl 3; gr 1; Done(); (* 50 *) Reflexiveeq(); (* 51 *) r(); r(); gl 4; gr 1; Done(); (* 56 *) Done(); (* 57 *) gl 3; w "a2"; (* 59 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 65 *) l(); r(); gr 2; r(); gl 4; gr 1; Done(); (* 72 *) Done(); (* 73 *) gl 3; w "a3"; (* 75 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 81 *) l(); rwr ~1; gl 3; rwr ~1; r(); r(); Reflexiveeq(); (* 88 *) gl 3; gr 1; Done(); (* 91 *) rwr ~1; r(); gr 2; r(); gl 3; gr 1; Done(); (* 98 *) Reflexiveeq(); (* 99 *) r(); l(); l(); rwr ~1; gl 2; rwr ~1; Reflexiveeq(); (* 106 *) l(); rwr ~1; gl 2; rwr ~1; DefEquals(); SetEquals(); r(); r(); r(); r(); r(); l(); gl 1; gr 2; Done(); (* 121 *) Done(); (* 122 *) r(); r(); l(); gl 1; gr 2; Done(); (* 128 *) Done(); (* 129 *) (* 128 CoupleEq: |- 1: a1 Couple a2 = a3 Couple a4 == a1 = a3 & a2 = a4 v a1 = a4 & a2 = a3 *) NameSequent 1 "CoupleEq"; (* 130 *) (* see if this can be used to prove Kpair property *) (* I need lemmas *) (* 1 *) Start "Sing(a1)=Couple(a2,a3)->a1=a2 & a1=a3"; (* 2 *) r(); r(); l(); Undo(); DefEquals(); SetEquals(); w "a2"; (* 9 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 15 *) rwr ~1; Reflexiveeq(); (* 17 *) DefEquals(); SetEquals(); w "a3"; (* 20 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 27 *) rwr ~1; Reflexiveeq(); (* 29 *) (* 28 SCLEMMA2: 1: Sing(a1) = a2 Couple a3 |- 1: a1 = a3 *) NameSequent 4 "SCLEMMA2"; (* 30 *) (* 29 SCLEMMA1: 1: Sing(a1) = a2 Couple a3 |- 1: a1 = a2 *) NameSequent 3 "SCLEMMA1"; (* 31 *) (* 1 *) Start "Couple(a1,a2)=Couple(a2,a1)"; (* 2 *) DefEquals(); SetEquals(); r(); r(); r(); r(); r(); l(); gl 1; gr 2; Done(); (* 13 *) Done(); (* 14 *) r(); r(); l(); gl 1; gr 2; Done(); (* 20 *) Done(); (* 21 *) (* 20 CoupleComm: |- 1: a1 Couple a2 = a2 Couple a1 *) NameSequent 1 "CoupleComm"; (* 22 *) (* 1 *) Start "Sing(a1)=Couple(a2,a3)->a2=a3"; (* 2 *) r(); ThmCut "SCLEMMA1"; (* 4 *) NextGoal(); (* 5 *) Done(); (* 6 *) ThmCut "SCLEMMA2"; (* 7 *) NextGoal(); (* 8 *) gl 2; gr 1; Done(); (* 11 *) crwr ~1; gl 2; rwr ~1; Reflexiveeq(); (* 15 *) NameSequent 2 "SCLEMMA3"; (* proof of Kpair basic result using the couple equality result, underway *) (* this is quite an elegant proof -- but it was crucial for sanity to prove lemmas above *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) l(); r(); r(); r(); DefEquals(); ThmCut "CoupleEq"; (* 10 *) su 5 "Sing(a1)"; su 6 "a1 Couple a2"; su 7 "Sing(a3)"; su 8 "Couple(a3,a4)"; l(); l(); l(); gl 2; gr 1; Done(); (* 20 *) l(); l(); DefEquals(); SetEquals(); w "a1"; (* 25 *) l(); l(); l(); Reflexiveeq(); (* 29 *) r(); Done(); (* 31 *) ThmCut "CoupleEq"; (* 32 *) su 9 "a1"; su 10 "a2"; su 11 "a3"; su 12 "a4"; l(); l(); l(); gl 5; gr 1; Done(); (* 44 *) l(); l(); gl 2; gr 1; Done(); (* 49 *) l(); crwr ~1; gl 2; rwr ~1; gl 3; rwr ~1; Reflexiveeq(); (* 56 *) l(); r(); UseThm "SCLEMMA1" [1] [1]; (* 59 *) ThmCut "SCLEMMA3"; (* 60 *) NextGoal(); (* 61 *) NextGoal(); (* 62 *) Done(); (* 63 *) Cut2 "Sing(a3)=Couple(a1,a2)"; (* 64 *) gl 2; gr 1; (* 67 *) gl 2; rwr ~1; Reflexiveeq(); (* 70 *) ThmCut "SCLEMMA2"; (* 71 *) NextGoal(); (* 72 *) NextGoal(); (* 73 *) Done(); (* 74 *) crwr ~1; gl 3; Done(); (* 77 *) r(); l(); rwr ~1; gl 2; rwr ~1; Reflexiveeq(); (* 83 *) (* the painful naive proof of the Kpair result *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) r(); r(); r(); DefEquals(); DefEquals(); SetEquals(); r(); w "Sing(a1)"; (* 10 *) l(); l(); l(); r(); Reflexiveeq(); (* 15 *) l(); DefEquals(); SetEquals(); w "a1"; (* 19 *) l(); l(); l(); Reflexiveeq(); (* 23 *) Done(); (* 24 *) DefEquals(); SetEquals(); w "a3"; (* 27 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 33 *) rwr ~1; Reflexiveeq(); (* not finished yet *) (* COMMENT: Dec 26 I must check this *) (* Joanna's hopefully complete version of the naive proof *) (* 1 *) Start "Kpair(a1,a2)=Kpair(a3,a4)==a1=a3&a2=a4"; (* 2 *) r(); r(); r(); r(); DefEquals(); DefEquals(); SetEquals(); w "Sing(a1)"; (* 10 *) l(); l(); l(); r(); Reflexiveeq(); (* 15 *) l(); DefEquals(); SetEquals(); w "a1"; (* 19 *) l(); l(); l(); Reflexiveeq(); (* 23 *) Done(); (* 24 *) DefEquals(); SetEquals(); w "a3"; (* 27 *) l(); l(); gl 2; l(); r(); Reflexiveeq(); (* 33 *) rwr ~1; Reflexiveeq(); (* 35 *) (* 34 COORDONE: 1: (Ax4. x4 = Sing(a1) v x4 = a1 Couple a2 == x4 = Sing(a3) v x4 = a3 Couple a4) |- 1: a1 = a3 *) (* Sequent snapshot: 1: a1 Kpair a2 = a3 Kpair a4 |- 1: a2 = a4 *) NameSequent 10 "COORDONE"; (* 36 *) DefEquals(); DefEquals(); SetEquals(); w "a1 Couple a2"; (* 40 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 46 *) l(); DefEquals(); SetEquals(); w "a2"; (* 50 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 56 *) gl 5; w "a3 Couple a4"; (* 58 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 65 *) l(); DefEquals(); SetEquals(); w "a4"; (* 69 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 75 *) rwr ~1; gl 5; rwr ~1; ThmCut "COORDONE"; (* 79 *) NextGoal(); (* 80 *) NextGoal(); (* 81 *) NextGoal(); (* 82 *) NextGoal(); (* 83 *) NextGoal(); (* 84 *) NextGoal(); (* 85 *) NextGoal(); (* 86 *) NextGoal(); (* 87 *) gl 9; gr 1; Done(); (* 90 *) rwr ~1; Reflexiveeq(); (* 92 *) DefEquals(); SetEquals(); w "a2"; (* 95 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 102 *) l(); gl 2; w "a4"; (* 105 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 111 *) l(); rwr ~1; gl 11; rwr ~1; ThmCut "COORDONE"; (* 116 *) NextGoal(); (* 117 *) NextGoal(); (* 118 *) NextGoal(); (* 119 *) NextGoal(); (* 120 *) NextGoal(); (* 121 *) NextGoal(); (* 122 *) NextGoal(); (* 123 *) NextGoal(); (* 124 *) NextGoal(); (* 125 *) NextGoal(); (* 126 *) NextGoal(); (* 127 *) NextGoal(); (* 128 *) NextGoal(); (* 129 *) NextGoal(); (* 130 *) NextGoal(); (* 131 *) NextGoal(); (* 132 *) gl 5; gr 1; Done(); (* 135 *) rwr ~1; Reflexiveeq(); (* 137 *) rwr ~1; Reflexiveeq(); (* 139 *) Done(); (* 140 *) DefEquals(); SetEquals(); w "a2"; (* 143 *) l(); l(); l(); r(); gr 2; Reflexiveeq(); (* 149 *) l(); gl 3; w "a4"; (* 152 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 159 *) l(); rwr ~1; gl 5; rwr ~1; ThmCut "COORDONE"; (* 164 *) NextGoal(); (* 165 *) NextGoal(); (* 166 *) NextGoal(); (* 167 *) NextGoal(); (* 168 *) NextGoal(); (* 169 *) NextGoal(); (* 170 *) NextGoal(); (* 171 *) NextGoal(); (* 172 *) gl 7; gr 1; Done(); (* 175 *) rwr ~1; Reflexiveeq(); (* 177 *) rwr ~1; Reflexiveeq(); (* 179 *) Done(); (* 180 *) r(); l(); rwr ~1; gl 2; rwr ~1; Reflexiveeq(); (* 186 *) (* COMMENT: Dec 26 Here's the "description" use of An *) (* the point is that sometimes we can prove that a set has one element; the choice operator gives us a way to write a name for that one element *) s "An(Sing(a1))=a1"; ThmCut "AN"; su 2 "Sing(a1)"; l(); d(); su 3 "a1"; r(); re(); NameSequent 1 "THE"; (* COMMENT: Dec 26 Here's a tool for dealing with the difficulty I ran into which we need to discuss *) s "a1+Zero < a2 + Zero -> a1a1a1 < a2"; (* 2 *) r(); ThmCut "MPLUS"; (* 4 *) l(); Done(); (* 6 *) su 6 "Minus(a3)"; ThmCut "APLUS"; (* 8 *) rwl ~1; ThmCut "APLUS"; (* 10 *) gl2 3; rwl ~1; ThmCut "MINUS"; (* 15 *) gl2 3; rwl 1; ThmCut "MINUS"; (* 18 *) gl2 3; rwl 1; ThmCut "LESSTYPEa"; (* 21 *) Done(); (* 22 *) gl 2; gr 1; Done(); (* 25 *) NameSequent 2 "MPLUSCONV"; (* COMMENT: Dec 27 you can compare my proof of MPLUSCONV: s "a1+a3a1 Zero a1 < a2"; (* you should try to prove this yourself *) s "a1 + Minus(One) < a1"; (* COMMENT: prove this *) (* 1 *) Start "a1 + Minus(One) < a1"; (* 2 *) ThmCut "ZEROLESSONE"; (* 3 *) ThmCut "MPLUS"; (* 4 *) l(); Done(); (* 6 *) su 4 "a1 + Minus(One)"; ThmCut "CPLUS"; (* 8 *) rwl 8; ThmCut "APLUS"; (* 10 *) gl2 3; crwl 2; ThmCut "MINUS"; (* 13 *) gl2 3; rwl 1; ThmCut "CPLUS"; (* 16 *) gl2 3; rwl 1; ThmCut "CPLUS"; (* 19 *) gl2 3; rwl 4; ThmCut "LESSTYPEa"; (* 22 *) Done(); (* 23 *) gl 2; gr 1; Done(); (* 26 *) NameSequent 1 "SomethingLess"; (* appallingly slow proof recording here - why? -- fixed as noted above*) s "Zero (Ex1.x1*x10 there is y such that y*y = x Proof: Let y = sup{z|z*z(Ex2.x2*x2 = x1))"; r(); r(); w "Sup({x3|x3*x3