(* This is repaired to work with the June 22 upgrade, which reduces the aggressiveness of the right equality rule. *) (* 0 *) hardcomment "empty set"; (* 1 *) Definefunction 0 "Null" "Null" "{x1|~x1=x1}"; (* 2 *) (* 1 *) hardcomment "singleton set"; (* 2 *) Definefunction 1 "Sing" "Sing(x1)" "{x2|x2=x1}"; (* 3 *) (* 2 *) hardcomment "the Frege natural number zero"; (* 3 *) Definefunction 0 "Zero" "Zero" "Sing(Null)"; (* 4 *) (* 3 *) hardcomment "The universal set"; (* 4 *) Definefunction 0 "V" "V" "{x1|x1=x1}"; (* 5 *) (* 4 *) hardcomment "The sethood predicate"; (* 5 *) Definepredicate 1 "Set" "Set(x1)" "x1=Null v (Ex2.x2Ex1)"; (* 6 *) (* 5 *) hardcomment "The subset relation:"; (* 5 *) hardcomment "the sethood conditions are expensive"; (* 6 *) Definepredicate 2 "c" "x1 c x2" "Set(x1)&Set(x2)&(Ax3.x3Ex1->x3Ex2)"; (* 7 *) (* 6 *) hardcomment "The extension of an object (the set with the same elements)"; (* 7 *) Definefunction 1 "Ext" "Ext(x1)" "{x2|x2Ex1}"; (* 8 *) (* 7 *) hardcomment "The power set"; (* 8 *) Definefunction 1 "Sc" "Sc(x1)" "{x2|x2 c x1}"; (* 9 *) (* 8 *) hardcomment "The set of all one-element subsets"; (* 9 *) Definefunction 1 "Usc" "Usc(x1)" "{Sing(x2)|x2 E x1}"; (* 10 *) (* 9 *) hardcomment "x1 is a function from x2 to x3"; (* 10 *) Definepredicate 3 "Function" "Function(x1,x2,x3)" "Set(x1)&Set(x2)&Set(x3)&(Ax4:x2.(Ex5:x3.[x4,x5]Ex1))&(Ax6:x1.(Ax7:x1.p1(x6)=p1(x7)->x6=x7))"; (* 11 *) (* 10 *) hardcomment "The converse of a relation"; (* 11 *) Definefunction 1 "Converse" "Converse(x1)" "{[x3,x2]|[x2,x3]Ex1}"; (* 12 *) (* 11 *) hardcomment "x1 is a bijection from x2 to x3"; (* 12 *) Definepredicate 3 "Bijection" "Bijection(x1,x2,x3)" "Function(x1,x2,x3)&Function(Converse(x1),x3,x2)"; (* 13 *) (* 12 *) hardcomment "x1 and x2 are sets of the same size"; (* 13 *) Definepredicate 2 "sim" "x1 sim x2" "(Ex3.Bijection(x3,x1,x2))"; (* 14 *) (* 13 *) hardcomment "The relative product of two relations"; (* 14 *) Definefunction 2 "Relprod" "x1 Relprod x2" "{[x3,x4]|(Ex5.[x3,x5]Ex1&[x5,x4]Ex2)}"; (* 15 *) (* 14 *) hardcomment "The unordered pair"; (* 15 *) Definefunction 2 "Couple" "x1Couple x2" "{x3|x3=x1vx3=x2}"; (* 16 *) (* 15 *) hardcomment "The Kuratowski ordered pair"; (* 16 *) Definefunction 2 "Kpair" "x1 Kpair x2" "Sing(x1) Couple x1 Couple x2"; (* 17 *) (* 16 *) hardcomment "A theorem on equality of unordered pairs"; (* 17 *) StartSequent [] ["a1Couple a2 = a3Couple a4 -> a1=a3&a2=a4va1=a4&a2=a3"]; (* 18 *) r(); r(); r(); gr 2; r(); l(); l(); l(); l(); r(); r(); l(); gl 1; gr 2; Done(); (* 33 *) Done(); (* 34 *) l(); l(); l(); gl 2; l(); r(); r(); l(); gr 2; rwr [1]; r(); rwr [1]; r(); gr 2; r(); l(); l(); l(); gr 2; r(); undo(); gl 2; l(); r(); gr 2; r(); l(); gr 2; rwr [1]; r(); rwr [1]; r(); l(); l(); l(); l(); r(); gr 2; r(); l(); Done(); (* 75 *) gr 2; Done(); (* 77 *) NameSequent 2 "CoupleEq"; (* 78 *) (* 77 CoupleEq: 1: a1 Couple a2 = a3 Couple a4 |- 1: a1 = a3 & a2 = a4 v a1 = a4 & a2 = a3 *) (* 77 *) hardcomment "The main theorem about the usual ordered pair, only half proved"; (* 78 *) StartSequent [] ["a1Kpair a2 = a3Kpair a4 -> a1=a3&a2=a4"]; (* 79 *) r(); l(); l(); r(); l(); l(); l(); undo(); r(); su 5 "Sing(a3)"; (* 89 *) l(); r(); r(); l(); Done(); (* 94 *) gl 1; gr 2; Done(); (* 97 *) gl 2; l(); r(); r(); l(); l(); l(); l(); l(); r(); gl 2; l(); gl 6; gr 1; Done(); (* 112 *) gl 7; rwr [1]; r(); l(); l(); l(); l(); r(); l(); rwr [1]; r(); gl 2; l(); r(); gl 6; gr 2; Done(); (* 129 *) gl 2; l(); su 5 "a2"; (* 132 *) l(); gl 2; l(); r(); gr 2; r(); gl 9; l(); Done(); (* 141 *) l(); rwr [1]; crwr [1]; gl 2; gr 1; Done(); (* 147 *) gl 3; l(); su 5 "a2"; (* 150 *) l(); gl 2; l(); r(); gr 2; r(); gl 3; l(); l(); l(); gl 2; l(); l(); undo(); r(); r(); Done(); (* 167 *) (* 167 *) StartSequent [] ["~a1ENull"]; (* 168 *) r(); r(); l(); l(); r(); NameSequent 1 "NullIsEmpty"; (* 174 *) (* 173 NullIsEmpty: |- 1: ~a1 E Null *) (* 173 *) hardcomment "The empty set has no elements"; (* 174 *) StartSequent [] ["a1EV"]; (* 175 *) r(); r(); NameSequent 1 "VIsUniversal"; (* 178 *) (* 177 VIsUniversal: |- 1: a1 E V *) (* 177 *) hardcomment "The universal set contains everything"; (* 178 *) StartSequent [] ["Set(Ext(a1))"]; (* 179 *) r(); r(); r(); r(); r(); r(); gr 2; r(); r(); Done(); (* 190 *) l(); r(); NameSequent 1 "SetExt"; (* 193 *) (* 192 SetExt: |- 1: Set(Ext(a1)) *) (* 192 *) hardcomment "The extension of an object is a set"; (* 193 *) StartSequent [] ["a1 c a2 & a2 c a1 -> Ext(a1)=Ext(a2)"]; (* 194 *) r(); l(); r(); r(); l(); gl 2; l(); l(); gl 2; l(); gl 3; l(); gl 2; l(); r(); r(); r(); gl 3; l(); l(); gl 6; gr 1; Done(); (* 217 *) Done(); (* 218 *) gl 6; l(); l(); gl 3; gr 1; Done(); (* 224 *) Done(); (* 225 *) NameSequent 1 "SubAntiSymm"; (* 226 *) (* 225 SubAntiSymm: |- 1: a1 c a2 & a2 c a1 -> Ext(a1) = Ext(a2) *) (* 225 *) hardcomment "subset relation is antisymmetric in a weak sense"; (* 225 *) hardcomment "Inclusion is actually strictly antisymmetric, not just up to extension"; (* 226 *) StartSequent [] ["a1 c a2 & a2 c a1 -> a1=a2"]; (* 227 *) r(); l(); gl 1; l(); gl 2; l(); gl 1; l(); gl 3; l(); gl 2; l(); gl 4; l(); l(); l(); gl 4; l(); l(); rwr [1]; gl 4; gr 1; Done(); (* 250 *) l(); r(); gl 1; gr 2; Done(); (* 255 *) r(); r(); gl 3; l(); l(); gl 6; gr 1; Done(); (* 263 *) Done(); (* 264 *) gl 6; l(); l(); gl 3; gr 1; Done(); (* 270 *) Done(); (* 271 *) l(); r(); Done(); (* 274 *) r(); r(); gl 6; l(); l(); gl 3; gr 1; Done(); (* 282 *) Done(); (* 283 *) gl 3; l(); l(); gl 6; gr 1; Done(); (* 289 *) Done(); (* 290 *) NameSequent 1 "StrictSubAntiSymm"; (* 291 *) (* 290 StrictSubAntiSymm: |- 1: a1 c a2 & a2 c a1 -> a1 = a2 *) (* 290 *) hardcomment "Power sets are sets"; (* 291 *) StartSequent [] ["Set(Sc(a1))"]; (* 292 *) r(); r(); r(); r(); r(); r(); gr 2; r(); r(); Done(); (* 301 *) l(); r(); NameSequent 1 "SetSc"; (* 304 *) (* 303 SetSc: |- 1: Set(Sc(a1)) *) (* 303 *) hardcomment "The class of one-element subsets is a set"; (* 304 *) StartSequent [] ["Set(Usc(a1))"]; (* 305 *) r(); r(); r(); r(); r(); r(); l(); gr 2; r(); su 4 "a2"; (* 314 *) r(); Done(); (* 316 *) gl 2; gr 1; Done(); (* 319 *) l(); l(); r(); NameSequent 1 "SetUsc"; (* 323 *) (* 322 SetUsc: |- 1: Set(Usc(a1)) *) (* 322 *) hardcomment "The class of one element subsets is a subset of the power set"; (* 323 *) StartSequent [] ["Usc(a1) c Sc(a1)"]; (* 324 *) r(); r(); UseThm "SetUsc" [] [1]; (* 327 *) r(); UseThm "SetSc" [] [1]; (* 329 *) r(); r(); l(); r(); r(); r(); r(); r(); gr 2; r(); su 4 "a3"; (* 340 *) rwr [1]; r(); r(); r(); r(); r(); gr 2; r(); gl 2; gr 1; Done(); (* 351 *) r(); l(); undo(); r(); gl 2; rwl [1]; gl2 3; rwl [1]; gl 2; l(); rwl [1]; crwl [1]; gl 2; gr 1; Done(); (* 366 *) NameSequent 1 "UsccSc"; (* 367 *) (* 366 UsccSc: |- 1: Usc(a1) c Sc(a1) *) (* 366 *) hardcomment "Singleton sets are sets"; (* 367 *) StartSequent [] ["Set(Sing(a1))"]; (* 368 *) r(); r(); gr 2; r(); su 2 "a1"; (* 373 *) r(); r(); NameSequent 1 "SetSing"; (* 376 *) (* 375 SetSing: |- 1: Set(Sing(a1)) *) (* 375 *) hardcomment "Reflexivity of equinumerousness"; (* 376 *) StartSequent [] ["Set(a1)->a1 sim a1"]; (* 377 *) r(); r(); r(); w 1 "{[x1,x1]|x1Ea1}"; (* 381 *) r(); r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); gr 2; r(); r(); Done(); (* 395 *) gl 2; gr 1; Done(); (* 398 *) l(); l(); r(); r(); Done(); (* 403 *) r(); Done(); (* 405 *) r(); r(); r(); Done(); (* 409 *) r(); r(); Done(); (* 412 *) r(); l(); r(); l(); rwr []; gl 3; rwr []; r(); rwr []; r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); gl 2; l(); l(); gr 2; r(); r(); gl 5; gr 1; Done(); (* 439 *) r(); rwr [1]; gl 2; rwr [1]; r(); gl 3; gr 1; Done(); (* 447 *) l(); l(); r(); r(); Done(); (* 452 *) r(); Done(); (* 454 *) r(); r(); r(); Done(); (* 458 *) r(); r(); r(); r(); Done(); (* 463 *) r(); l(); r(); l(); rwr []; gl 3; rwr []; gl 2; l(); l(); rwr []; gl 2; rwr []; gl 4; rwr []; gl 2; l(); l(); rwr []; gl 2; rwr []; r(); rwr []; r(); NameSequent 1 "SimSelf"; (* 488 *) (* 487 SimSelf: |- 1: Set(a1) -> a1 sim a1 *) (* when I made the right equality rule less aggressive, I seemed to be forced to write a quite different proof here *) (* 488 *) StartSequent [] ["Set(a1)->a1=Converse(Converse(a1))"]; r();l();l(); rwr nil;r();r();r();r();l();l();r(); l();Gl 2;Gl 2;l(); r(); l();r();r();Done(); r();r();r();r();r();r();r();r();Done(); l();Gl 2;l();rf();rf();gl 3;rwr nil;Triv 2 1; (* (* 489 *) r(); r(); r(); r(); l(); l(); rwr []; r(); r(); r(); l(); l(); r(); l(); gl 2; l(); gl 2; l(); l(); r(); l(); r(); r(); Done(); (* 511 *) r(); r(); r(); NextGoal(); (* 515 *) NextGoal(); (* 516 *) su 12 "p2(a10)"; (* 517 *) su 11 "p1(a10)"; (* 518 *) r(); NextGoal(); (* 520 *) NextGoal(); (* 521 *) r(); NextGoal(); (* 523 *) l(); RewriteFree(); l(); l(); RewriteFree(); RewriteFree(); Done(); (* 530 *) r(); Done(); *) (* 532 *) NameSequent 2 "Converse2"; (* 533 *) (* 532 Converse2: 1: Set(a1) |- 1: a1 = Converse(Converse(a1)) *) (* 532 *) hardcomment "The converse of the converse is the relation itself"; (* 533 *) StartSequent [] ["a1 sim a2 -> a2 sim a1"]; (* 534 *) r(); l(); l(); r(); r(); su 4 "Converse(a3)"; (* 540 *) l(); l(); r(); r(); gl 2; gr 1; Done(); (* 547 *) ThmCut "Converse2"; (* 548 *) su 4 "a3"; (* 549 *) l(); l(); Done(); (* 552 *) rwr []; crwr []; crwr []; gl 2; gr 1; Done(); (* 558 *) NameSequent 1 "SimSymm"; (* 559 *) (* 558 SimSymm: |- 1: a1 sim a2 -> a2 sim a1 *) (* 558 *) hardcomment "Relative products of functions with appropriate domain and range are functions"; (* 559 *) StartSequent [] ["Function(a1,a3,a4)&Function(a2,a4,a5)->Function(a1 Relprod a2,a3,a5)"]; (* 560 *) r(); r(); r(); r(); r(); r(); r(); r(); r(); l(); RewriteFree(); gr 2; r(); su 9 "[a7,a8]"; (* 573 *) r(); r(); Done(); (* 576 *) l(); l(); r(); AutoPrune(); NameSequent 4 "RelProdSet"; (* 581 *) (* 580 RelProdSet: |- 1: Set(a1 Relprod a2) *) (* Sequent snapshot: 1: Function(a1,a3,a4) & Function(a2,a4,a5) |- 1: Set(a3) & Set(a5) & (A x5 : a3.(E x6 : a5.[x5,x6] E a1 Relprod a2)) & (A x7 : a1 Relprod a2.(A x8 : a1 Relprod a2.p1(x7) = p1(x8) -> x7 = x8)) *) (* 580 *) hardcomment "Relative products are sets"; (* Sequent snapshot: 1: Function(a1,a3,a4) & Function(a2,a4,a5) |- 1: Set(a3) & Set(a5) & (A x5 : a3.(E x6 : a5.[x5,x6] E a1 Relprod a2)) & (A x7 : a1 Relprod a2.(A x8 : a1 Relprod a2.p1(x7) = p1(x8) -> x7 = x8)) *) r(); l(); l(); l(); gl 2; l(); Done(); (* 588 *) r(); l(); gl 2; l(); l(); gl 2; l(); gl 2; l(); Done(); (* 598 *) r(); r(); gl 2; l(); l(); l(); pl 1; l(); pl 1; l(); pl 1; l(); l(); gl 4; gr 1; Done(); (* 614 *) l(); AutoPrune(); gl 5; l(); l(); pl 1; l(); pl 1; l(); pl 1; l(); l(); gl 4; gr 1; Done(); (* 629 *) l(); r(); Done(); (* 632 *) r(); r(); r(); r(); gl 7; gr 1; Done(); (* 639 *) gl 2; gr 1; Done(); (* 642 *) r(); r(); l(); RewriteFree(); gl 2; l(); RewriteFree(); r(); gl 2; l(); gl 3; l(); gl 2; RewriteFree(); l(); gl 4; l(); gl 5; l(); l(); gl 2; l(); pl 1; undo(); l(); pl 1; l(); pl 1; l(); pl 1; l(); pl 1; gl 6; l(); pl 1; l(); pl 1; l(); pl 1; l(); pl 1; l(); gl 3; gr 1; Done(); (* 687 *) l(); gl 6; gr 1; Done(); (* 691 *) l(); r(); l(); RewriteFree(); RewriteFree(); gl 3; l(); gl 3; gr 1; Done(); (* 701 *) l(); gl 6; gr 1; Done(); (* 705 *) l(); r(); l(); RewriteFree(); RewriteFree(); r(); NameSequent 1 "Comp"; (* 712 *) (* 711 Comp: |- 1: Function(a1,a3,a4) & Function(a2,a4,a5) -> Function(a1 Relprod a2,a3,a5) *)