(* master file for Joanna Guild's potential project *) (* Idea: rewrite this into new version as debugging cruise *) (* Joanna, look for comments marked with COMMENT: *) (* Dec 27 SUP1 corrected -- private version *) (* 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 *) DeclareFunction "An" [0,1]; Axiom "AN" ["a2 E a1"] ["An(a1) E a1"]; (* declarations and axioms for an ordered field *) (* primitive notions *) DeclarePredicate "Real" [0]; (* note that numerals are now legal terms! *) (* DeclareFunction "0" [0]; DeclareFunction "1" [0]; *) DeclareFunction "+" [0,0,0]; DeclareFunction "*" [0,0,0]; setprecrightabove "*" "+"; DeclarePredicate "<" [0,0]; DeclareFunction "Minus" [0,0]; DeclareFunction "Inv" [0,0]; DeclareFunction "Sup" [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+0=a1"]; Axiom "ITIMES" nil ["Real(a1)-> a1*1=a1"]; (* defines the relation "coerced to the same real" *) DefinePredicate 2 "Equal" "x1 Equal x2" "x1+0=x2+0"; (* inverse laws *) Axiom "MINUS" nil ["a1+Minus(a1)=0"]; Axiom "INV" nil ["a1 Equal 0 v a1*Inv(a1)=1"]; (* otherwise we could have a model with one inhabitant, Zero *) Axiom "NONTRIV" nil ["~0 Equal 1"]; (* basic properties of strict linear order *) Axiom "IRR" nil ["~a1 < a1"]; Axiom "TRI" nil ["a1 Equal a2 v a1 < a2 v a2 a1 < a3"]; (* monotonicity properties of order *) Axiom "MPLUS0" nil ["a1 a1+a3 a1*a3x1 <= 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. *) (* begin new prover version of NULLADD *) (* startlogging "nulladd"; *) (* 1 *) StartSequent [] ["Real(a1)&Real(a2)->(a1+a2=a1==a2=0)"]; (* 2 *) r(); r(); Cutr "[a1+a2]+Minus(a1)=a1+Minus(a1)"; (* 5 *) gl 2; l(); gl 3; rwr [1]; r(); ThmCut "CPLUS"; (* 11 *) rwl [2]; (*rwl [1];*) gl 4; l(); gl 4; ThmCut "APLUS"; (* 17 *) rwl [1]; ThmCut "MINUS"; (* 19 *) gl2 3; rwl nil; ThmCut "IPLUS"; (* 22 *) l(); gl 5; gr 1; Done(); (* 26 *) gl2 3; rwl [1]; gl 2; gr 1; Done(); (* 31 *) rwr [1]; gl 2; l(); ThmCut "IPLUS"; (* 36 *) l(); Done(); Done(); NameSequent 1 "NULLADD"; (* stoplogging(); *) (* end new prover version of NULLADD *) (* create the "sequent" form of IPLUS *) (* 1 *) StartSequent ["Real(a1)"] ["a1+0=a1"]; (* 2 *) ThmCut "IPLUS"; (* 3 *) l(); Done(); (* 5 *) Done(); (* 6 *) (* 5 -------------------- Proved ---------------------- Line 1: 1: Real(a1) |- 1: a1 + 0 = a1 By 3, 2*) (* 5 -------------------- Proved ---------------------- Line 3: 1: Real(a1) -> a1 + 0 = a1 2: Real(a1) |- 1: a1 + 0 = a1 By 5, 4*) (* 5 -------------------- Trivial --------------------- Line 5: 1: a1 + 0 = a1 2: Real(a1) |- 1: a1 + 0 = a1 *) (* 5 -------------------- Trivial --------------------- Line 4: 1: Real(a1) |- 1: Real(a1) 2: a1 + 0 = a1 *) (* 5 -------------------- Proved ---------------------- Line 2: |- 1: Real(a1) -> a1 + 0 = a1 By IPLUS*) (* 5 Proof of IPLUS begins *) (* 5 -------------------- Proved ---------------------- Line 12.1: |- 1: Real(a1) -> a1 + 0 = a1 By IPLUS.*) (* 5 is an axiom*) (* 5 Proof of IPLUS ends*) NameSequent 1 "IPLUSa"; (* 7 *) (* 6 IPLUSa: 1: Real(a1) |- 1: a1 + 0 = a1 *) (* a trivial lemma (smilie) *) s "a1=a1"; r(); NameSequent 1 "TRIV"; (* 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 *) (* 1 *) StartSequent ["P1","P1->P2"] ["P2"]; (* 2 *) gl 2; l(); Done(); (* 5 *) Done(); (* 6 *) NameSequent 1 "MP"; (* 7 *) (* 6 MP: 1: P1 -> P2 2: P1 |- 1: P2 *) (* 7 *) StartSequent [] ["Real(0)"]; (* 8 *) ThmCut "MINUS"; (* 9 *) crwr [1]; UseThm "RPLUS" [] [1]; (* 12 *) NameSequent 1 "RZERO"; (* BEGIN UNCORRECTED 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 nil; 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 nil; re(); NameSequent 1 "MZERO"; END UNCORRECTED *) (* 1 *) StartSequent [] ["a1*0=0"]; (* 2 *) Cut "a1*0+a1*0 = a1*0"; (* 3 *) ThmCut "DIST"; (* 4 *) crwr [1]; ThmCut "IPLUSa"; (* 6 *) NextGoal(); (* 7 *) NextGoal(); (* 8 *) rwr [1]; r(); UseThm "RZERO" [] [1]; (* 11 *) ThmCut "NULLADD"; (* 12 *) (* l(); r(); UseThm "RZERO" [] [1]; (* 15 *) UseThm "RZERO" [] [1]; (* 16 *) undo(); undo(); undo(); undo(); undo(); undo(); *) l(); NextGoal(); (* 24 *) l(); l(); gl 2; gr 1; Done(); (* 29 *) Done(); (* 30 *) r(); UseThm "RTIMES" [] [1]; (* 32 *) UseThm "RTIMES" [] [1]; (* 33 *) Prove 1 "MZERO"; (* BEGIN UNCORRECTED (* 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 nil; 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 nil; gl 2; gl2 3; rwl nil; ThmCut "APLUS"; su 9 "a2"; su 10 "a1"; su 11 "Minus(a1)"; gl2 3; rwl nil; ThmCut "MINUS"; su 12 "a1"; gl2 3; rwl nil; ThmCut "IPLUS"; su 13 "a2"; l(); Triv 3 1; gl2 3; rwl nil; 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"; END UNCORRECTED *) (* trivial as a theorem but valuable as a tool with ThmCut *) ss ["a1=a2"] ["a1+a3=a2+a3"]; rwr [1]; r(); Prove 1 "BOTHSIDESPLUS"; (* uniqueness of additive inverse *) ss ["Real(a2)","a1+a2=0"] ["a2=Minus(a1)"]; ThmCut "BOTHSIDESPLUS"; (* note that I implemented "add to both sides" neatly *) Triv 2 1; w 1 "Minus(a1)"; ThmCut "CPLUS"; rwl [2]; ThmCut "APLUS"; gl2 3; rwl [1]; ThmCut "MINUS"; gl2 3; rwl [1]; ThmCut "CPLUS"; gl2 3; rwl [2]; ThmCut "IPLUSa"; Triv 3 1; gl2 3; rwl [1]; ThmCut "IPLUSa"; ng(); gl2 3; rwl [1]; Triv 2 1; UseThm "RMINUS" nil [1]; Prove 1 "UINV"; (* BEGIN UNCORRECTED s "Real(a1)->Zero+a1=a1"; r(); ThmCut "CPLUS"; su 2 "Zero"; su 3 "a1"; rwr nil; 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"; END UNCORRECTED *) (* 1 *) StartSequent ["Real(a1)"] ["0+a1=a1"]; (* 2 *) ThmCut "IPLUSa"; (* 3 *) Done(); (* 4 *) crwr [2]; UseThm "CPLUS" [] [1]; (* 12 *) NameSequent 1 "IPLUSb"; (* 13 *) (* 12 IPLUSb: 1: Real(a1) |- 1: 0 + a1 = a1 *) (* BEGIN UNCORRECTED s "Minus(a1)+a1=Zero"; ThmCut "CPLUS"; su 2 "Minus(a1)"; su 3 "a1"; rwr nil; UseThm "MINUS" nil [1]; NameSequent 1 "MINUS2"; END UNCORRECTED *) (* 1 *) StartSequent [] ["Minus(a1)+a1=0"]; (* 2 *) ThmCut "CPLUS"; (* 3 *) rwr [1]; UseThm "MINUS" [] [1]; (* 5 *) Prove 1 "MINUS2"; (* Begin UNCORRECTED 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 nil; ThmCut "MINUS"; su 9 "a1"; gl2 3; rwl nil; ThmCut "IPLUSb"; su 10 "Minus(a2)"; gl2 3; rwl nil; gl 2; ThmCut "CPLUS"; su 11 "Minus(a1)"; su 12 "Minus(a2)"; rwl nil; ThmCut "APLUS"; su 13 "a2"; su 14 "Minus(a2)"; su 15 "Minus(a1)"; gl2 3; crwl nil; ThmCut "MINUS"; su 16 "a2"; gl2 3; rwl nil; ThmCut "IPLUSb"; su 17 "Minus(a1)"; gl2 3; rwl nil; 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 nil; gl 2;Cut "Minus(a1)+a1+a2=a2+Zero"; rwl nil; 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 nil; ThmCut "MINUS2"; su 27 "a1"; rwr nil; UseThm "CPLUS" nil [1]; ThmCut "CPLUS"; su 28 "Minus(a2)"; su 29 "a1+a2"; rwr nil; ThmCut "APLUS"; su 30 "a1"; su 31 "a2"; su 32 "Minus(a2)"; rwr nil; ThmCut "MINUS"; su 33 "a2"; rwr nil; re(); NameSequent 1 "MINUSLESS"; end UNCORRECTED *) (* 1 *) StartSequent [] ["a1 < a2 == Minus(a2) < Minus(a1)"]; (* 2 *) r(); ThmCut "MPLUS"; (* 4 *) l(); Done(); (* 6 *) w 1 "Minus(a1)+Minus(a2)"; (* 7 *) ThmCut "APLUS"; (* 8 *) crwl [1]; gl 2; ThmCut "MINUS"; (* 11 *) rwl [1]; ThmCut "IPLUSb"; (* 13 *) w 1 "Minus(a2)"; (* 14 *) UseThm "RMINUS" [] [1]; (* 15 *) gl2 3; rwl [1]; ThmCut "CPLUS"; (* 18 *) gl2 3; rwl [1]; ThmCut "APLUS"; (* 21 *) gl2 3; rwl [1]; ThmCut "MINUS2"; (* 24 *) gl2 3; rwl [1]; ThmCut "IPLUSa"; (* 27 *) w 1 "Minus(a1)"; (* 28 *) UseThm "RMINUS" [] [1]; (* 29 *) gl2 3; rwl [1]; gl 2; gr 1; Done(); (* 34 *) ThmCut "MPLUS"; (* 35 *) l(); Done(); (* 37 *) w 1 "a1+a2"; (* 38 *) ThmCut "CPLUS"; (* 39 *) rwl [1]; undo(); undo(); undo(); rwl [2]; undo(); undo(); rwl [1]; undo(); undo(); undo(); undo(); rwl [3]; undo(); undo(); undo(); rwl [1]; gl 2; ThmCut "APLUS"; (* 58 *) rwl [1]; ThmCut "MINUS"; (* 60 *) gl2 3; rwl [1]; ThmCut "APLUS"; (* 63 *) crwl [1]; undo(); gl2 3; crwl [1]; ThmCut "MINUS2"; (* 68 *) gl2 3; rwl [1]; (* 69 MPLUS: |- 1: a1 < a2 -> a1 + a3 < a2 + a3 *) (* Sequent snapshot: 1: Minus(a1) + a1 = 0 2: a1 + 0 < 0 + a2 3: Minus(a2) < Minus(a1) 4: Minus(a2) + a1 + a2 = [a1 + a2] + Minus(a2) 5: [a1 + a2] + Minus(a2) = a1 + a2 + Minus(a2) 6: a2 + Minus(a2) = 0 7: [Minus(a1) + a1] + a2 = Minus(a1) + a1 + a2 |- 1: a1 < a2 *) (* 69 MPLUS0: |- 1: a1 < a2 == a1 + a3 < a2 + a3 *) (* Sequent snapshot: 1: Minus(a1) + a1 = 0 2: a1 + 0 < 0 + a2 3: Minus(a2) < Minus(a1) 4: Minus(a2) + a1 + a2 = [a1 + a2] + Minus(a2) 5: [a1 + a2] + Minus(a2) = a1 + a2 + Minus(a2) 6: a2 + Minus(a2) = 0 7: [Minus(a1) + a1] + a2 = Minus(a1) + a1 + a2 |- 1: a1 < a2 *) ThmCut "CPLUS"; (* 71 *) gl2 3; rwl [2]; ThmCut "MPLUS0"; (* 74 *) l(); gl 2; l(); gl 2; gr 1; Done(); (* 80 *) Done(); (* 81 *) NameSequent 1 "MINUSLESS"; (* 82 *) (* 81 MINUSLESS: |- 1: a1 < a2 == Minus(a2) < Minus(a1) *) (* BEGIN UNCORRECTED (* 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 nil; ThmCut "IPLUS"; (* 15 *) su 4 "a2"; l(); gl 4; Done(); (* 19 *) gl2 3; rwl nil; gl 2; Done(); (* 23 *) (* 22 EQUALITY: 1: a1 Equal a2 2: Real(a1) 3: Real(a2) |- 1: a1 = a2 *) NameSequent 4 "EQUALITY"; (* 24 *) END UNCORRECTED *) (* 1 *) StartSequent ["a1 Equal a2","Real(a1)","Real(a2)"] ["a1=a2"]; (* 2 *) l(); ThmCut "IPLUSa"; (* 4 *) gl 2; gr 1; Done(); (* 7 *) rwl [1]; gl 2; ThmCut "IPLUSa"; (* 10 *) gl 3; gr 1; Done(); (* 13 *) rwl [1]; gl 2; gr 1; Done(); (* 17 *) NameSequent 1 "EQUALITY"; (* 18 *) (* 17 EQUALITY: 1: a1 Equal a2 2: Real(a1) 3: Real(a2) |- 1: a1 = a2 *) (* BEGIN UNCORRECTED (* 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 nil; ThmCut "CPLUS"; (* 11 *) su 3 "Zero"; su 4 "Minus(a1)"; gl2 3; rwl nil; ThmCut "IPLUSa"; (* 16 *) su 5 "Minus(a1)"; gl2 3; rwl nil; 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 nil; gl 3; Done(); (* 30 *) Done(); (* 31 *) (* 30 NEGINEQ: 1: a1 < Zero |- 1: Zero < Minus(a1) *) END UNCORRECTED *) (* 1 *) StartSequent ["a1<0"] ["0a1 * 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 nil; Undo(); crwl nil; ThmCut "MINUS"; (* 14 *) su 6 "a2"; rwl [1]; ThmCut "MZERO"; (* 17 *) su 7 "a1"; gl2 3; rwl nil; ThmCut "UINV"; (* 21 *) su 9 "a1*Minus(a2)"; su 8 "a1*a2"; Done(); (* 24 *) UseThm "RTIMES" [] [1]; (* 25 *) gl 2; rwr nil; Reflexiveeq(); (* 28 *) ThmCut "DIST"; (* 29 *) su 10 "a1"; su 11 "a2"; su 12 "Minus(a2)"; crwr nil; ThmCut "MINUS"; (* 34 *) su 13 "a2"; rwr nil; ThmCut "MZERO"; (* 37 *) su 14 "a1"; Done(); (* 39 *) (* 38 NEGCOMM: |- 1: a1 * Minus(a2) = Minus(a1 * a2) *) NameSequent 3 "NEGCOMM"; END UNCORRECTED *) (* 40 *) (* 1 *) StartSequent [] ["a1*Minus(a2)=Minus(a1*a2)"]; (* 2 *) ThmCut "TRIV"; (* 3 *) w 1 "a1*Minus(a2)"; (* 4 *) ThmCut "BOTHSIDESPLUS"; (* 5 *) Done(); (* 6 *) w 1 "a1*a2+Minus(a1*a2)"; (* 7 *) ThmCut "MINUS"; (* 8 *) rwl [1]; ThmCut "IPLUSa"; (* 10 *) w 1 "a1*Minus(a2)"; (* 11 *) UseThm "RTIMES" [] [1]; (* 12 *) gl2 3; rwl [1]; gl 2; (* ThmCut "DIST"; (* 16 *) crwl [1]; undo(); undo(); undo(); *) ThmCut "APLUS"; (* 21 *) crwl [1]; gl 2; ThmCut "DIST"; (* 24 *) crwl [1]; ThmCut "MINUS2"; (* 26 *) gl2 3; rwl [1]; ThmCut "MZERO"; (* 30 *) gl2 3; rwl [1]; gl 2; ThmCut "IPLUSb"; (* 34 *) w 1 "Minus(a1*a2)"; (* 35 *) UseThm "RMINUS" [] [1]; (* 36 *) rwl [1]; gl 2; gr 1; Done(); (* 40 *) NameSequent 1 "NEGCOMM"; (* 41 *) (* 40 NEGCOMM: |- 1: a1 * Minus(a2) = Minus(a1 * a2) *) (* BEGIN UNCORRECTED (*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 nil; ThmCut "UINV"; (* 10 *) su 6 "a1"; su 5 "Minus(a1)"; crwr nil; Reflexiveeq(); (* 14 *) gl 3; Done(); (* 16 *) gl 2; Done(); (* 18 *) (* 17 DOUBLENEG: 1: Real(a1) |- 1: Minus(Minus(a1)) = a1 *) NameSequent 2 "DOUBLENEG"; (* 19 *) END UNCORRECTED *) (* this proof is somewhat mischievous *) (* 1 *) StartSequent ["Real(a1)"] ["Minus(Minus(a1))=a1"]; (* 2 *) ThmCut "UINV"; (* 3 *) Done(); (* 4 *) UseThm "MINUS2" [] [1]; (* 5 *) rwr [2]; r(); NameSequent 1 "DOUBLENEG"; (* 8 *) (* 7 DOUBLENEG: 1: Real(a1) |- 1: Minus(Minus(a1)) = a1 *) (* BEGIN UNCORRECTED (* 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 nil; ThmCut "CTIMES"; (* 7 *) su 5 "Minus(a1)"; su 6 "a2"; rwr nil; ThmCut "NEGCOMM"; (* 11 *) su 7 "a2"; su 8 "a1"; rwr nil; ThmCut "CTIMES"; (* 15 *) su 9 "a2"; su 10 "a1"; rwr nil; 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 *) END UNCORRECTED *) (* 1 *) StartSequent [] ["Minus(a1)*Minus(a2)=a1*a2"]; (* 2 *) ThmCut "NEGCOMM"; (* 3 *) rwr [1]; ThmCut "NEGCOMM"; (* 5 *) ThmCut "CTIMES"; (* 6 *) rwr [1]; ThmCut "NEGCOMM"; (* 8 *) rwr [1]; ThmCut "NEGCOMM"; (* 10 *) undo(); undo(); ThmCut "DOUBLENEG"; (* 13 *) NextGoal(); ThmCut "CTIMES"; (* 16 *) rwr [1]; gl 2; Done(); (* 20 *) UseThm "RTIMES" [] [1]; (* 21 *) Prove 1 "TIMESDOUBNEG"; (* Begin UNCORRECTED (* 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 nil; ThmCut "TIMESDOUBNEG"; (* 36 *) su 12 "a1"; su 13 "a3"; gl2 3; rwl nil; gl 2; Done(); (* 46 *) Done(); (* 47 *) (* 46 MTIMESNEG: 1: a3 < Zero 2: a1 < a2 |- 1: a2 * a3 < a1 * a3 *) NameSequent 3 "MTIMESNEG"; (* 48 *) END UNCORRECTED *) (* 1 *) StartSequent [] ["a3 < 0 & a1 a2*a3 < a1*a3"]; (* 2 *) r(); l(); ThmCut "NEGINEQ"; (* 7 *) w 1 "a3"; (* 8 *) ThmCut "MINUSLESS"; (* 9 *) w 2 "a1"; (* 10 *) w 1 "a2"; (* 11 *) l(); l(); gl 3; gr 1; Done(); (* 16 *) gl 3; gr 1; Done(); (* 19 *) ThmCut "MTIMES"; (* 20 *) w 3 "Minus(a3)"; (* 21 *) w 2 "Minus(a2)"; (* 22 *) w 1 "Minus(a1)"; (* 23 *) l(); r(); Done(); (* 26 *) (* 25 MINUSLESS: |- 1: a1 < a2 == Minus(a2) < Minus(a1) *) (* Sequent snapshot: 1: 0 < Minus(a3) 2: a3 < 0 3: a1 < a2 |- 1: Minus(a2) < Minus(a1) 2: a2 * a3 < a1 * a3 *) ThmCut "MINUSLESS"; (* 27 *) l(); l(); gl 4; gr 1; Done(); (* 32 *) Done(); (* 33 *) ThmCut "TIMESDOUBNEG"; (* 34 *) rwl [1]; gl 2; ThmCut "TIMESDOUBNEG"; (* 37 *) rwl [1]; gl 2; Done(); (* 40 *) (* 39 -------------------- Proved ---------------------- Line 1: |- 1: a3 < 0 & a1 < a2 -> a2 * a3 < a1 * a3 By 2*) (* 39 -------------------- Proved ---------------------- Line 2: 1: a3 < 0 & a1 < a2 |- 1: a2 * a3 < a1 * a3 By 3*) (* 39 -------------------- Proved ---------------------- Line 3: 1: a3 < 0 2: a1 < a2 |- 1: a2 * a3 < a1 * a3 By 6, 4, 5*) NameSequent 3 "MTIMESNEG"; (* 41 *) (* 40 MTIMESNEG: 1: a3 < 0 2: a1 < a2 |- 1: a2 * a3 < a1 * a3 *) (*BEGIN UNCORRECTED (* 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 nil; ThmCut "MZERO"; (* 15 *) su 6 "Zero"; rwr nil; gl 2; rwl nil; 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 nil; gl 2; rwl nil; 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 nil; gl 2; rwl nil; gl 2; gr 2; Done(); (* 62 *) (* 61 SQUARENONNEG: 1: Real(a1) |- 1: Zero <= a1 * a1 *) NameSequent 2 "SQUARENONNEG"; END UNCORRECTED *) (* 1 *) StartSequent ["Real(a1)"] ["0<=a1*a1"]; (* 2 *) ThmCut "TRI"; (* 3 *) l(); w 2 "a1"; (* 5 *) w 1 "0"; (* 6 *) Cut "a1=0"; (* 7 *) Cut "Real(0)"; (* 8 *) UseThm "RZERO" [] [1]; (* 9 *) UseThm "EQUALITY" [2,3,1] [1]; (* 10 *) rwr nil; ThmCut "MZERO"; (* 12 *) rwr [1]; r(); r(); r(); r(); l(); ThmCut "MTIMES"; (* 19 *) undo(); undo(); ThmCut "MTIMESNEG"; (* 22 *) Done(); (* 23 *) Done(); (* 24 *) ThmCut "CTIMES"; (* 25 *) rwl [1]; gl 2; ThmCut "MZERO"; (* 28 *) rwl [1]; gl 2; gr 1; (* Done(); *) (* 32 *) (* 31 Not done!*) (* Sequent snapshot: 1: 0 < a1 * a1 2: a1 < 0 3: Real(a1) 4: 0 * a1 = a1 * 0 5: a1 * 0 = 0 |- 1: 0 <= a1 * a1 *) r(); r(); gl 1; gr 2; Done(); (* 37 *) ThmCut "MTIMES"; (* 38 *) l(); r(); Done(); (* 41 *) Done(); (* 42 *) ThmCut "CTIMES"; (* 43 *) rwl [1]; gl 2; ThmCut "MZERO"; (* 46 *) rwl [1]; gl 2; r(); r(); (* Done(); *) (* 51 *) (* 50 Not done!*) (* Sequent snapshot: 1: 0 < a1 * a1 2: 0 < a1 3: Real(a1) 4: 0 * a1 = a1 * 0 5: a1 * 0 = 0 |- 1: 0 Equal a1 * a1 2: 0 < a1 * a1 *) gl 1; gr 2; Done(); (* 54 *) NameSequent 1 "SQUARENONNEG"; (* 55 *) (* 54 SQUARENONNEG: 1: Real(a1) |- 1: 0 <= a1 * a1 *) (* BEGIN UNCORRECTED TAIL (* Holmes attempt on the square root problem *) s "Zero*a1=Zero"; ThmCut "CTIMES"; rwr nil; UseThm "MZERO" nil [1]; NameSequent 1 "MZERO2"; s "a1 Equal a2 -> a2 Equal a1"; r();r();l();rwr nil; re(); NameSequent 2 "EqualSymm"; s "Real(One)"; ThmCut "INV"; ThmCut "NONTRIV"; l();l();UseThm "EqualSymm" [1] [1]; gr 2; crwr nil; 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; *) (* new prover version of definition *) DefineFunction 2 "Union" "x1 Union x2" "{x3|x3 E x1 v x3 E x2}"; 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; *) DefineFunction 1 "Sing" "Sing(x1)" "{x2|x2=x1}"; (* 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; *) DefineFunction 2 "Couple" "x1 Couple x2" "{x3|x3=x1 v x3=x2}"; (* 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; *) DefineFunction 2 "Kpair" "x1 Kpair x2" "Sing(x1) Couple [x1 Couple x2]"; (* 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 nil; 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 nil; 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 nil; r(); gl 2; gr 1; Done(); (* 25 *) l(); Undo(); DefEquals(); rwr nil; 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 nil; 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 nil; gl 6; gr 1; Done(); (* 60 *) l(); Undo(); gl2 3; rwl nil; 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 nil; gl 6; gr 1; Done(); (* 104 *) Done(); (* 105 *) r(); rwr nil; 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 nil; gl 2; l(); gl 5; rwr nil; gl 4; l(); l(); rwr nil; Reflexiveeq(); (* 8 *) rwr nil; DefEquals(); SetEquals(); r(); gl 4; rwr nil; r(); r(); r(); r(); Done(); (* 19 *) r(); l(); Done(); (* 22 *) Done(); (* 23 *) rwr nil; gl 2; l(); l(); gl2 4; rwl nil; gl 2; gl 5; gl 2; l(); gl 5; rwr nil; DefEquals(); SetEquals(); r(); gl 2; rwr nil; r(); r(); r(); l(); Done(); (* 45 *) Done(); (* 46 *) r(); r(); Done(); (* 49 *) rwr nil; 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 nil; ThmCut "PROJ1"; (* 345 *) su 7 "a3"; su 8 "a4"; gl2 3; rwl nil; 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 nil; ThmCut "PROJ2"; (* 365 *) su 11 "a3"; su 12 "a4"; gl2 3; rwl nil; gl 2; DefEquals(); SetEquals(); w "a2"; (* 373 *) l(); l(); gl 2; l(); Reflexiveeq(); (* 378 *) Done(); (* 379 *) l(); r(); l(); rwr nil; gl 2; rwr nil; 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 nil; 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 nil; r(); r(); gl 3; gr 1; Done(); (* 39 *) gl 3; rwr nil; gl 3; gr 1; Done(); (* 44 *) rwr nil; 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 nil; gl 3; rwr nil; r(); r(); Reflexiveeq(); (* 88 *) gl 3; gr 1; Done(); (* 91 *) rwr nil; r(); gr 2; r(); gl 3; gr 1; Done(); (* 98 *) Reflexiveeq(); (* 99 *) r(); l(); l(); rwr nil; gl 2; rwr nil; Reflexiveeq(); (* 106 *) l(); rwr nil; gl 2; rwr nil; 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 nil; Reflexiveeq(); (* 17 *) DefEquals(); SetEquals(); w "a3"; (* 20 *) l(); l(); gl 2; l(); r(); gr 2; Reflexiveeq(); (* 27 *) rwr nil; 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 nil; gl 2; rwr nil; 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 nil; gl 2; rwr nil; gl 3; rwr nil; 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 nil; Reflexiveeq(); (* 70 *) ThmCut "SCLEMMA2"; (* 71 *) NextGoal(); (* 72 *) NextGoal(); (* 73 *) Done(); (* 74 *) crwr nil; gl 3; Done(); (* 77 *) r(); l(); rwr nil; gl 2; rwr nil; 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 nil; 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 nil; 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 nil; gl 5; rwr nil; 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 nil; 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 nil; gl 11; rwr nil; 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 nil; Reflexiveeq(); (* 137 *) rwr nil; 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 nil; gl 5; rwr nil; 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 nil; Reflexiveeq(); (* 177 *) rwr nil; Reflexiveeq(); (* 179 *) Done(); (* 180 *) r(); l(); rwr nil; gl 2; rwr nil; 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 -> a1a1 Zero a1 < a2"; r();l(); ThmCut "MTIMES"; l(); r(); UseThm "POSINV" [1] [1]; Triv 2 1; ThmCut "ATIMES"; rwl [1]; pl 1; ThmCut "ATIMES"; rwl [1]; pl 1; ThmCut "INV"; l(); UseThm "NOTBOTH3" [3,1] nil; rwl nil; pl 1; ThmCut "TYPECONVERT"; rwl [1]; pl 1; ThmCut "TYPECONVERT"; rwl [1]; pl 1; UseThm "LESSTYPEa" [1] [1]; NameSequent 3 "MTIMESCONV"; (* definitely taking too long to store -- solved by locking ZEROLESSONE *) s "a1 + Minus(One) < a1"; (* COMMENT: prove this *) (* 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