>> Inspector Lestrade says: >> Welcome to the Lestrade Type Inspector, >> full solution to name collisions >> (renames identifiers in saved or imported moves). >> matching of lambda terms installed, not sure how to test it >> interface refinements >> disabled prop/type symmetry re rewrite feature >> version of 12/2/2016 >> 7 pm Boise time %% this is a development of pocket set theory, which is both a funny %% exercise in axiomatics and perhaps one of the smallest untyped set theories % which might be viewed as a foundation for mathematics. %% In the proof of the basic property of ordered pairs, I use a version of %% the substitution property of equality which exploits indifference as to the choice %% of evidence for a proposition. The property can be proved without this variation: % it would be more awkward, because we would be unable to use Lemma 3. % demonstration of the import feature. import discretemath % primitives are numbered declare p prop >> p: prop {move 1} declare q prop >> q: prop {move 1} % 1. implication construct -> p q : prop >> ->: [(p_1:prop),(q_1:prop) => (---:prop)] >> {move 0} declare pp that p >> pp: that p {move 1} define Fixfun p pp : pp >> Fixfun: [(p_1:prop),(pp_1:that p_1) => (pp_1: >> that p_1)] >> {move 0} declare rr that p -> q >> rr: that (p -> q) {move 1} % 2. the rule of modus ponens construct Mp pp rr that q >> Mp: [(.p_1:prop),(pp_1:that .p_1),(.q_1:prop), >> (rr_1:that (.p_1 -> .q_1)) => (---:that >> .q_1)] >> {move 0} open declare pp1 that p >> pp1: that p {move 2} construct ded pp1 : that q >> ded: [(pp1_1:that p) => (---:that q)] >> {move 1} close % 3. the deduction theorem (for us an axiom) construct Deduction ded : that p -> q >> Deduction: [(.p_1:prop),(.q_1:prop),(ded_1: >> [(pp1_2:that .p_1) => (---:that .q_1)]) >> => (---:that (.p_1 -> .q_1))] >> {move 0} % 4. a primitive false statement, the absurd construct ?? prop >> ??: prop {move 0} define ~ p : p -> ?? >> ~: [(p_1:prop) => ((p_1 -> ??):prop)] >> {move 0} declare maybe that ~ ~ p >> maybe: that ~(~(p)) {move 1} % 5. the double negation axiom construct Dneg maybe : that p >> Dneg: [(.p_1:prop),(maybe_1:that ~(~(.p_1))) >> => (---:that .p_1)] >> {move 0} % development of conjunction declare qq that q >> qq: that q {move 1} define & p q: ~(p -> ~q) >> &: [(p_1:prop),(q_1:prop) => (~((p_1 -> ~(q_1))): >> prop)] >> {move 0} open declare notandev that p -> ~q >> notandev: that (p -> ~(q)) {move 2} define andline1 notandev : Mp pp notandev >> andline1: [(notandev_1:that (p -> ~(q))) >> => ((pp Mp notandev_1):that ~(q))] >> {move 1} define andline2 notandev : Mp qq andline1 notandev >> andline2: [(notandev_1:that (p -> ~(q))) >> => ((qq Mp andline1(notandev_1)): >> that ??)] >> {move 1} close define Conj pp qq: Fixfun (p & q,Deduction andline2) >> Conj: [(.p_1:prop),(pp_1:that .p_1),(.q_1: >> prop),(qq_1:that .q_1) => (((.p_1 & >> .q_1) Fixfun Deduction([(notandev_2: >> that (.p_1 -> ~(.q_1))) => ((qq_1 >> Mp (pp_1 Mp notandev_2)):that ??)])) >> :that (.p_1 & .q_1))] >> {move 0} declare andev that p & q >> andev: that (p & q) {move 1} open declare notp that ~p >> notp: that ~(p) {move 2} open declare pp1 that p >> pp1: that p {move 3} open declare qq1 that q >> qq1: that q {move 4} define andline3 qq1 : Mp pp1 notp >> andline3: [(qq1_1:that q) >> => ((pp1 Mp notp):that >> ??)] >> {move 3} close define andline4 pp1 : Fixfun(~q,Deduction andline3) >> andline4: [(pp1_1:that p) => ((~(q) >> Fixfun Deduction([(qq1_2:that >> q) => ((pp1_1 Mp notp): >> that ??)])) >> :that ~(q))] >> {move 2} close define andline5 notp : Deduction andline4 >> andline5: [(notp_1:that ~(p)) => (Deduction([(pp1_2: >> that p) => ((~(q) Fixfun Deduction([(qq1_3: >> that q) => ((pp1_2 Mp >> notp_1):that ??)])) >> :that ~(q))]) >> :that (p -> ~(q)))] >> {move 1} define andline6 notp : Mp andline5 notp andev >> andline6: [(notp_1:that ~(p)) => ((andline5(notp_1) >> Mp andev):that ??)] >> {move 1} close define Simp1 andev : Dneg(Deduction andline6) >> Simp1: [(.p_1:prop),(.q_1:prop),(andev_1: >> that (.p_1 & .q_1)) => (Dneg(Deduction([(notp_2: >> that ~(.p_1)) => ((Deduction([(pp1_3: >> that .p_1) => ((~(.q_1) Fixfun >> Deduction([(qq1_4:that .q_1) >> => ((pp1_3 Mp notp_2): >> that ??)])) >> :that ~(.q_1))]) >> Mp andev_1):that ??)])) >> :that .p_1)] >> {move 0} open declare notq that ~q >> notq: that ~(q) {move 2} open declare pp1 that p >> pp1: that p {move 3} define andline7 pp1 : notq >> andline7: [(pp1_1:that p) => (notq: >> that ~(q))] >> {move 2} close define andline8 notq : Deduction andline7 >> andline8: [(notq_1:that ~(q)) => (Deduction([(pp1_2: >> that p) => (notq_1:that ~(q))]) >> :that (p -> ~(q)))] >> {move 1} define andline9 notq : Mp andline8 notq andev >> andline9: [(notq_1:that ~(q)) => ((andline8(notq_1) >> Mp andev):that ??)] >> {move 1} close define Simp2 andev : Dneg (Deduction andline9) >> Simp2: [(.p_1:prop),(.q_1:prop),(andev_1: >> that (.p_1 & .q_1)) => (Dneg(Deduction([(notq_2: >> that ~(.q_1)) => ((Deduction([(pp1_3: >> that .p_1) => (notq_2:that >> ~(.q_1))]) >> Mp andev_1):that ??)])) >> :that .q_1)] >> {move 0} %% demonstrate import feature: % the proof of the contrapositive rule imported from discretemath % and the rule of exportation imported from discretemath: much more elaborate. save current clearcurrent discretemath declare p prop >> p: prop {move 1:discretemath} declare q prop >> q: prop {move 1:discretemath} declare r prop >> r: prop {move 1:discretemath} declare indevx that (~\$q) ->\$ ~\$p >> indevx: that (~\$(q) ->\$ ~\$(p)) {move 1:discretemath} define Contra0 ->\$, Mp', Deduction', ??\$, Dneg', indevx : Contrapositive indevx >> Contra0: [(->\$_1:[(p_2:prop),(q_2:prop) => >> (---:prop)]), >> (Mp'_1:[(.p_3:prop),(pp_3:that .p_3), >> (.q_3:prop),(ss_3:that (.p_3 ->\$_1 >> .q_3)) => (---:that .q_3)]), >> (Deduction'_1:[(.p_4:prop),(.q_4:prop), >> (Ded_4:[(pp1_5:that .p_4) => (---: >> that .q_4)]) >> => (---:that (.p_4 ->\$_1 .q_4))]), >> (??\$_1:prop),(Dneg'_1:[(.p_6:prop),(maybe_6: >> that ((.p_6 ->\$_1 ??\$_1) ->\$_1 >> ??\$_1)) => (---:that .p_6)]), >> (.q_1:prop),(.p_1:prop),(indevx_1:that >> ((.q_1 ->\$_1 ??\$_1) ->\$_1 (.p_1 ->\$_1 >> ??\$_1))) => (Deduction'_1(.p_1,.q_1, >> [(pp1_7:that .p_1) => ((.q_1 Dneg'_1 >> Deduction'_1((.q_1 ->\$_1 ??\$_1), >> ??\$_1,[(notq_8:that (.q_1 ->\$_1 >> ??\$_1)) => (Mp'_1(.p_1,pp1_7, >> ??\$_1,Mp'_1((.q_1 ->\$_1 ??\$_1), >> notq_8,(.p_1 ->\$_1 ??\$_1), >> indevx_1)):that ??\$_1)])) >> :that .q_1)]) >> :that (.p_1 ->\$_1 .q_1))] >> {move 0} declare indev that (~q) -> ~p >> indev: that (~(q) -> ~(p)) {move 1:discretemath} define Contra indev : Contra0 ->, Mp, Deduction, ??, Dneg, indev >> Contra: [(.q_1:prop),(.p_1:prop),(indev_1: >> that (~(.q_1) -> ~(.p_1))) => (Contra0(->, >> Mp,Deduction,??,Dneg,indev_1):that (.p_1 >> -> .q_1))] >> {move 0} define Exprt0 &\$, Conjunction, Simplification1, Simplification2, ->\$, Mp', Deduction', ??\$, Dneg', p q r : Export p q r >> Exprt0: [(&\$_1:[(p_2:prop),(q_2:prop) => >> (---:prop)]), >> (Conjunction_1:[(.p_3:prop),(pp_3:that >> .p_3),(.q_3:prop),(qq_3:that .q_3) >> => (---:that (.p_3 &\$_1 .q_3))]), >> (Simplification1_1:[(.p_4:prop),(.q_4: >> prop),(rr_4:that (.p_4 &\$_1 .q_4)) >> => (---:that .p_4)]), >> (Simplification2_1:[(.p_5:prop),(.q_5: >> prop),(rr_5:that (.p_5 &\$_1 .q_5)) >> => (---:that .q_5)]), >> (->\$_1:[(p_6:prop),(q_6:prop) => (---: >> prop)]), >> (Mp'_1:[(.p_7:prop),(pp_7:that .p_7), >> (.q_7:prop),(ss_7:that (.p_7 ->\$_1 >> .q_7)) => (---:that .q_7)]), >> (Deduction'_1:[(.p_8:prop),(.q_8:prop), >> (Ded_8:[(pp1_9:that .p_8) => (---: >> that .q_8)]) >> => (---:that (.p_8 ->\$_1 .q_8))]), >> (??\$_1:prop),(Dneg'_1:[(.p_10:prop), >> (maybe_10:that ((.p_10 ->\$_1 ??\$_1) >> ->\$_1 ??\$_1)) => (---:that .p_10)]), >> (p_1:prop),(q_1:prop),(r_1:prop) => >> (Conjunction_1((((p_1 &\$_1 q_1) ->\$_1 >> r_1) ->\$_1 (p_1 ->\$_1 (q_1 ->\$_1 r_1))), >> Deduction'_1(((p_1 &\$_1 q_1) ->\$_1 r_1), >> (p_1 ->\$_1 (q_1 ->\$_1 r_1)),[(line1_11: >> that ((p_1 &\$_1 q_1) ->\$_1 r_1)) >> => (Deduction'_1(p_1,(q_1 ->\$_1 >> r_1),[(line2_12:that p_1) => (Deduction'_1(q_1, >> r_1,[(line3_13:that q_1) => >> (Mp'_1((p_1 &\$_1 q_1), >> Conjunction_1(p_1,line2_12, >> q_1,line3_13),r_1,line1_11): >> that r_1)]) >> :that (q_1 ->\$_1 r_1))]) >> :that (p_1 ->\$_1 (q_1 ->\$_1 r_1)))]), >> ((p_1 ->\$_1 (q_1 ->\$_1 r_1)) ->\$_1 ((p_1 >> &\$_1 q_1) ->\$_1 r_1)),Deduction'_1((p_1 >> ->\$_1 (q_1 ->\$_1 r_1)),((p_1 &\$_1 q_1) >> ->\$_1 r_1),[(line8_14:that (p_1 ->\$_1 >> (q_1 ->\$_1 r_1))) => (Deduction'_1((p_1 >> &\$_1 q_1),r_1,[(line9_15:that (p_1 >> &\$_1 q_1)) => (Mp'_1(q_1,Simplification2_1(p_1, >> q_1,line9_15),r_1,Mp'_1(p_1, >> Simplification1_1(p_1,q_1, >> line9_15),(q_1 ->\$_1 r_1), >> line8_14)):that r_1)]) >> :that ((p_1 &\$_1 q_1) ->\$_1 r_1))])) >> :that ((((p_1 &\$_1 q_1) ->\$_1 r_1) ->\$_1 >> (p_1 ->\$_1 (q_1 ->\$_1 r_1))) &\$_1 ((p_1 >> ->\$_1 (q_1 ->\$_1 r_1)) ->\$_1 ((p_1 &\$_1 >> q_1) ->\$_1 r_1))))] >> {move 0} define Exprt p q r : Exprt0 &, Conj, Simp1, Simp2, ->, Mp, Deduction, ??, Dneg, p q r >> Exprt: [(p_1:prop),(q_1:prop),(r_1:prop) >> => (Exprt0(&,Conj,Simp1,Simp2,->,Mp, >> Deduction,??,Dneg,p_1,q_1,r_1):that >> ((((p_1 & q_1) -> r_1) -> (p_1 -> (q_1 >> -> r_1))) & ((p_1 -> (q_1 -> r_1)) -> >> ((p_1 & q_1) -> r_1))))] >> {move 0} clearcurrent current % primitives 1-5 implement propositional logic open declare x1 obj >> x1: obj {move 2} construct Pred x1 : prop >> Pred: [(x1_1:obj) => (---:prop)] >> {move 1:current} close % 6. the universal quantifier construct Forall Pred : prop >> Forall: [(Pred_1:[(x1_2:obj) => (---:prop)]) >> => (---:prop)] >> {move 0} declare univev that Forall Pred >> univev: that Forall(Pred) {move 1:current} declare x obj >> x: obj {move 1:current} % 7. the rule of universal instantiation construct Ui univev x : that Pred x >> Ui: [(.Pred_1:[(x1_2:obj) => (---:prop)]), >> (univev_1:that Forall(.Pred_1)),(x_1: >> obj) => (---:that .Pred_1(x_1))] >> {move 0} open declare x1 obj >> x1: obj {move 2} construct gen x1 : that Pred x1 >> gen: [(x1_1:obj) => (---:that Pred(x1_1))] >> {move 1:current} close % 8. the rule of universal generalization construct Ug gen : that Forall Pred >> Ug: [(.Pred_1:[(x1_2:obj) => (---:prop)]), >> (gen_1:[(x1_3:obj) => (---:that .Pred_1(x1_3))]) >> => (---:that Forall(.Pred_1))] >> {move 0} declare y obj >> y: obj {move 1:current} %% primitives 7-9 implement full first order logic % with the obvious definition of the existential quantifier % 9. the equality predicate construct = x y : prop >> =: [(x_1:obj),(y_1:obj) => (---:prop)] >> {move 0} % 10. reflexivity of equality construct Refleq x that x=x >> Refleq: [(x_1:obj) => (---:that (x_1 = x_1))] >> {move 0} declare predev that Pred x >> predev: that Pred(x) {move 1:current} declare eqev that x = y >> eqev: that (x = y) {move 1:current} %% 11. the substitution property of equality % Subs2 is a variant enforcing indifference to evidence for propositions. construct Subs Pred, predev eqev : that Pred y >> Subs: [(Pred_1:[(x1_2:obj) => (---:prop)]), >> (.x_1:obj),(predev_1:that Pred_1(.x_1)), >> (.y_1:obj),(eqev_1:that (.x_1 = .y_1)) >> => (---:that Pred_1(.y_1))] >> {move 0} define Subsb predev eqev :Subs Pred, predev eqev >> Subsb: [(.Pred_1:[(x1_2:obj) => (---:prop)]), >> (.x_1:obj),(predev_1:that .Pred_1(.x_1)), >> (.y_1:obj),(eqev_1:that (.x_1 = .y_1)) >> => (Subs(.Pred_1,predev_1,eqev_1):that >> .Pred_1(.y_1))] >> {move 0} open declare x1 obj >> x1: obj {move 2} construct Pred1 x1 prop >> Pred1: [(x1_1:obj) => (---:prop)] >> {move 1:current} declare xev1 that Pred1 x1 >> xev1: that Pred1(x1) {move 2} construct Pred3 x1 xev1 prop >> Pred3: [(x1_1:obj),(xev1_1:that Pred1(x1_1)) >> => (---:prop)] >> {move 1:current} close declare x5 obj >> x5: obj {move 1:current} declare xev5 that Pred1 x5 >> xev5: that Pred1(x5) {move 1:current} declare y5 obj >> y5: obj {move 1:current} declare yev5 that Pred1 y5 >> yev5: that Pred1(y5) {move 1:current} declare xeva5 that Pred3 x5 xev5 >> xeva5: that (x5 Pred3 xev5) {move 1:current} declare eqev5 that x5 = y5 >> eqev5: that (x5 = y5) {move 1:current} %% 12. A more sophisticated version of substitution, % working on objects specified via evidence for facts about them. %% Of course Subs2 can readily prove Subs % so we are not really increasing the axiom count. construct Subs2 Pred1, Pred3, yev5 xeva5 eqev5 : that Pred3 y5 yev5 >> Subs2: [(Pred1_1:[(x1_2:obj) => (---:prop)]), >> (Pred3_1:[(x1_3:obj),(xev1_3:that Pred1_1(x1_3)) >> => (---:prop)]), >> (.y5_1:obj),(yev5_1:that Pred1_1(.y5_1)), >> (.x5_1:obj),(.xev5_1:that Pred1_1(.x5_1)), >> (xeva5_1:that (.x5_1 Pred3_1 .xev5_1)), >> (eqev5_1:that (.x5_1 = .y5_1)) => (---: >> that (.y5_1 Pred3_1 yev5_1))] >> {move 0} % symmetry of equality open declare x1 obj >> x1: obj {move 2} define itequalsx x1 : x1 = x >> itequalsx: [(x1_1:obj) => ((x1_1 = x): >> prop)] >> {move 1:current} close define Eqsymm eqev : Subs(itequalsx,Refleq x,eqev) >> Eqsymm: [(.x_1:obj),(.y_1:obj),(eqev_1:that >> (.x_1 = .y_1)) => (Subs([(x1_2:obj) >> => ((x1_2 = .x_1):prop)] >> ,Refleq(.x_1),eqev_1):that (.y_1 = .x_1))] >> {move 0} declare x3 obj >> x3: obj {move 1:current} declare y3 obj >> y3: obj {move 1:current} declare z3 obj >> z3: obj {move 1:current} declare xytrans that x3=y3 >> xytrans: that (x3 = y3) {move 1:current} declare yztrans that y3=z3 >> yztrans: that (y3 = z3) {move 1:current} define Transeq xytrans yztrans: Eqsymm(Subs(=(z3),Eqsymm yztrans,Eqsymm xytrans)) >> Transeq: [(.x3_1:obj),(.y3_1:obj),(xytrans_1: >> that (.x3_1 = .y3_1)),(.z3_1:obj),(yztrans_1: >> that (.y3_1 = .z3_1)) => (Eqsymm(Subs([(y_2: >> obj) => ((.z3_1 = y_2):prop)] >> ,Eqsymm(yztrans_1),Eqsymm(xytrans_1))): >> that (.x3_1 = .z3_1))] >> {move 0} % primitives 9-12 implement the logic of equality % 13 the membership predicate construct E x y : prop >> E: [(x_1:obj),(y_1:obj) => (---:prop)] >> {move 0} % 14 the class abstraction constructor construct Classof Pred : obj >> Classof: [(Pred_1:[(x1_2:obj) => (---:prop)]) >> => (---:obj)] >> {move 0} open declare x1 obj >> x1: obj {move 2} define selfeq x1 : x1 = x1 >> selfeq: [(x1_1:obj) => ((x1_1 = x1_1): >> prop)] >> {move 1:current} close % an important defined notion, the class of all sets define V : Classof selfeq >> V: [(Classof([(x1_1:obj) => ((x1_1 = x1_1): >> prop)]) >> :obj)] >> {move 0} open declare x1 obj >> x1: obj {move 2} define isset x1 : x1 E V >> isset: [(x1_1:obj) => ((x1_1 E V):prop)] >> {move 1:current} close declare z obj >> z: obj {move 1:current} declare setev that y E V >> setev: that (y E V) {move 1:current} open declare x1 obj >> x1: obj {move 2} construct Pred2 x1 prop >> Pred2: [(x1_1:obj) => (---:prop)] >> {move 1:current} close declare inev that Pred2 y >> inev: that Pred2(y) {move 1:current} %% 15 comprehension 1: a set satisfying the defining predicate % of a class belongs to the class. construct comp1 setev Pred2, inev : that y E Classof Pred2 >> comp1: [(.y_1:obj),(setev_1:that (.y_1 E >> V)),(Pred2_1:[(x1_2:obj) => (---:prop)]), >> (inev_1:that Pred2_1(.y_1)) => (---: >> that (.y_1 E Classof(Pred2_1)))] >> {move 0} define compb1 setev inev : comp1 setev Pred2, inev >> compb1: [(.y_1:obj),(setev_1:that (.y_1 E >> V)),(.Pred2_1:[(x1_2:obj) => (---:prop)]), >> (inev_1:that .Pred2_1(.y_1)) => (comp1(setev_1, >> .Pred2_1,inev_1):that (.y_1 E Classof(.Pred2_1)))] >> {move 0} declare inev2 that y E Classof Pred >> inev2: that (y E Classof(Pred)) {move 1:current} %% 16. comprehension 2: an object belonging to a class % has its defining predicate construct comp2 inev2 : that Pred y >> comp2: [(.y_1:obj),(.Pred_1:[(x1_2:obj) => >> (---:prop)]), >> (inev2_1:that (.y_1 E Classof(.Pred_1))) >> => (---:that .Pred_1(.y_1))] >> {move 0} declare inev3 that y E x >> inev3: that (y E x) {move 1:current} %% 17. comprehension 3: an element of a class % belongs to the universal class V. construct comp3 inev3 : that y E V >> comp3: [(.y_1:obj),(.x_1:obj),(inev3_1:that >> (.y_1 E .x_1)) => (---:that (.y_1 E >> V))] >> {move 0} open declare z1 obj >> z1: obj {move 2} declare itsin that z1 E x >> itsin: that (z1 E x) {move 2} declare itsin2 that z1 E y >> itsin2: that (z1 E y) {move 2} construct subset1 itsin that z1 E y >> subset1: [(.z1_1:obj),(itsin_1:that >> (.z1_1 E x)) => (---:that (.z1_1 >> E y))] >> {move 1:current} construct subset2 itsin2 that z1 E x >> subset2: [(.z1_1:obj),(itsin2_1:that >> (.z1_1 E y)) => (---:that (.z1_1 >> E x))] >> {move 1:current} close %% 18. The axiom of extensionality: % classes with the same elements are the same. construct Extensionality subset1, subset2 : that x = y >> Extensionality: [(.x_1:obj),(.y_1:obj),(subset1_1: >> [(.z1_2:obj),(itsin_2:that (.z1_2 E >> .x_1)) => (---:that (.z1_2 E .y_1))]), >> (subset2_1:[(.z1_3:obj),(itsin2_3:that >> (.z1_3 E .y_1)) => (---:that (.z1_3 >> E .x_1))]) >> => (---:that (.x_1 = .y_1))] >> {move 0} %% primitives 13-18 complete the definition of % the impredicative theory of sets and classes. %% The remaining axioms require the definition of the notion %% of equal cardinality, which is rather complex. % It could be stated more simply in second order terms. % we begin with development of the ordered pair declare xev that x E V >> xev: that (x E V) {move 1:current} declare yev that y E V >> yev: that (y E V) {move 1:current} define v p q : ~p -> q >> v: [(p_1:prop),(q_1:prop) => ((~(p_1) -> >> q_1):prop)] >> {move 0} declare selfor that p v p >> selfor: that (p v p) {move 1:current} open declare selfor2 that ~p >> selfor2: that ~(p) {move 2} define selfor3 selfor2 : Mp selfor2 selfor >> selfor3: [(selfor2_1:that ~(p)) => ((selfor2_1 >> Mp selfor):that p)] >> {move 1:current} define selfor4 selfor2 : Mp selfor3 selfor2 selfor2 >> selfor4: [(selfor2_1:that ~(p)) => ((selfor3(selfor2_1) >> Mp selfor2_1):that ??)] >> {move 1:current} close define Selfor selfor : Dneg(Deduction selfor4) >> Selfor: [(.p_1:prop),(selfor_1:that (.p_1 >> v .p_1)) => (Dneg(Deduction([(selfor2_2: >> that ~(.p_1)) => (((selfor2_2 Mp >> selfor_1) Mp selfor2_2):that ??)])) >> :that .p_1)] >> {move 0} open declare z1 obj >> z1: obj {move 2} define pairpred z1: (x=z1) v y = z1 >> pairpred: [(z1_1:obj) => (((x = z1_1) >> v (y = z1_1)):prop)] >> {move 1:current} close %% the unordered pair: note that the projections % are packaged in evidence for their sethood. define upair xev yev : Classof pairpred >> upair: [(.x_1:obj),(xev_1:that (.x_1 E V)), >> (.y_1:obj),(yev_1:that (.y_1 E V)) => >> (Classof([(z1_2:obj) => (((.x_1 = z1_2) >> v (.y_1 = z1_2)):prop)]) >> :obj)] >> {move 0} declare xxev that ((upair xev xev) E V) >> xxev: that ((xev upair xev) E V) {move 1: >> current} declare xyev that ((upair xev yev) E V) >> xyev: that ((xev upair yev) E V) {move 1: >> current} %% the preliminary definition of the ordered pair. %% Eventually we will know that the components %% are sets, and we will have a definition of the pair % with explicit arguments xev and yev. define pair0 xxev xyev : upair xxev xyev >> pair0: [(.x_1:obj),(.xev_1:that (.x_1 E V)), >> (xxev_1:that ((.xev_1 upair .xev_1) >> E V)),(.y_1:obj),(.yev_1:that (.y_1 >> E V)),(xyev_1:that ((.xev_1 upair .yev_1) >> E V)) => ((xxev_1 upair xyev_1):obj)] >> {move 0} % prove that x E xev upair yev % to do this, prove that ~x=x -> y=x % assume ~x=x % goal y=x open declare line1 that ~(x=x) >> line1: that ~((x = x)) {move 2} define line2 line1 : Mp (Refleq x, line1) >> line2: [(line1_1:that ~((x = x))) => >> ((Refleq(x) Mp line1_1):that ??)] >> {move 1:current} open declare line3 that ~(y=x) >> line3: that ~((y = x)) {move 3} define line4 line3: line2 line1 >> line4: [(line3_1:that ~((y = x))) >> => (line2(line1):that ??)] >> {move 2} close define line5 line1 : Dneg(Deduction line4) >> line5: [(line1_1:that ~((x = x))) => >> (Dneg(Deduction([(line3_2:that >> ~((y = x))) => (line2(line1_1): >> that ??)])) >> :that (y = x))] >> {move 1:current} close define line6 x y : Deduction line5 >> line6: [(x_1:obj),(y_1:obj) => (Deduction([(line1_2: >> that ~((x_1 = x_1))) => (Dneg(Deduction([(line3_3: >> that ~((y_1 = x_1))) => ((Refleq(x_1) >> Mp line1_2):that ??)])) >> :that (y_1 = x_1))]) >> :that (~((x_1 = x_1)) -> (y_1 = x_1)))] >> {move 0} define Lemma1 xev yev : Fixfun (x E xev upair yev,comp1 xev pairpred, (line6 x y)) >> Lemma1: [(.x_1:obj),(xev_1:that (.x_1 E V)), >> (.y_1:obj),(yev_1:that (.y_1 E V)) => >> (((.x_1 E (xev_1 upair yev_1)) Fixfun >> comp1(xev_1,[(z1_2:obj) => (((.x_1 = >> z1_2) v (.y_1 = z1_2)):prop)] >> ,(.x_1 line6 .y_1))):that (.x_1 E (xev_1 >> upair yev_1)))] >> {move 0} % prove that y E xev upair yev % to do this, prove that ~x=y -> y=y % assume ~x=y open declare sillyassumption that ~(x=y) >> sillyassumption: that ~((x = y)) {move >> 2} define donehere sillyassumption : Refleq y >> donehere: [(sillyassumption_1:that ~((x >> = y))) => (Refleq(y):that (y = >> y))] >> {move 1:current} close define line3 x y : Deduction donehere >> line3: [(x_1:obj),(y_1:obj) => (Deduction([(sillyassumption_2: >> that ~((x_1 = y_1))) => (Refleq(y_1): >> that (y_1 = y_1))]) >> :that (~((x_1 = y_1)) -> (y_1 = y_1)))] >> {move 0} define Lemma2 xev yev : Fixfun(y E xev upair yev,comp1 yev pairpred, line3 x y) >> Lemma2: [(.x_1:obj),(xev_1:that (.x_1 E V)), >> (.y_1:obj),(yev_1:that (.y_1 E V)) => >> (((.y_1 E (xev_1 upair yev_1)) Fixfun >> comp1(yev_1,[(z1_2:obj) => (((.x_1 = >> z1_2) v (.y_1 = z1_2)):prop)] >> ,(.x_1 line3 .y_1))):that (.y_1 E (xev_1 >> upair yev_1)))] >> {move 0} %declare z obj declare zev that z E V >> zev: that (z E V) {move 1:current} % prove the lemma that if {x,y} = {x,z} then y=z % assume that {x,y} = {x,z) % goal: y=z declare line8 that (xev upair yev) = xev upair zev >> line8: that ((xev upair yev) = (xev upair >> zev)) {move 1:current} % show that y E {x,z} open declare w1 obj >> w1: obj {move 2} define yinit w1 : y E w1 >> yinit: [(w1_1:obj) => ((y E w1_1):prop)] >> {move 1:current} close define line9 line8 : Subs (yinit,Lemma2 xev yev,line8) >> line9: [(.x_1:obj),(.xev_1:that (.x_1 E V)), >> (.y_1:obj),(.yev_1:that (.y_1 E V)), >> (.z_1:obj),(.zev_1:that (.z_1 E V)), >> (line8_1:that ((.xev_1 upair .yev_1) >> = (.xev_1 upair .zev_1))) => (Subs([(w1_2: >> obj) => ((.y_1 E w1_2):prop)] >> ,(.xev_1 Lemma2 .yev_1),line8_1):that >> (.y_1 E (.xev_1 upair .zev_1)))] >> {move 0} define line10 line8 : comp2 (line9 line8) >> line10: [(.x_1:obj),(.xev_1:that (.x_1 E >> V)),(.y_1:obj),(.yev_1:that (.y_1 E >> V)),(.z_1:obj),(.zev_1:that (.z_1 E >> V)),(line8_1:that ((.xev_1 upair .yev_1) >> = (.xev_1 upair .zev_1))) => (comp2(line9(line8_1)): >> that ((.x_1 = .y_1) v (.z_1 = .y_1)))] >> {move 0} % assume ~(y=z) for the sake of a contradiction open declare line11 that ~(y=z) >> line11: that ~((y = z)) {move 2} open declare line12 that ~(x=y) >> line12: that ~((x = y)) {move 3} define line13 line12 : Mp(line12, line10 line8) >> line13: [(line12_1:that ~((x = >> y))) => ((line12_1 Mp line10(line8)): >> that (z = y))] >> {move 2} define line14 line12 :Eqsymm (line13 line12) >> line14: [(line12_1:that ~((x = >> y))) => (Eqsymm(line13(line12_1)): >> that (y = z))] >> {move 2} define line15 line12: Mp(Eqsymm (line13 line12),line11) >> line15: [(line12_1:that ~((x = >> y))) => ((Eqsymm(line13(line12_1)) >> Mp line11):that ??)] >> {move 2} close define line16 line11 : Dneg(Deduction line15) >> line16: [(line11_1:that ~((y = z))) >> => (Dneg(Deduction([(line12_2:that >> ~((x = y))) => ((Eqsymm((line12_2 >> Mp line10(line8))) Mp line11_1): >> that ??)])) >> :that (x = y))] >> {move 1:current} open declare w1 obj >> w1: obj {move 3} define zinit w1 : z E w1 >> zinit: [(w1_1:obj) => ((z E w1_1): >> prop)] >> {move 2} close define line17 line11: Subs(zinit, Lemma2 xev zev, Eqsymm line8) >> line17: [(line11_1:that ~((y = z))) >> => (Subs([(w1_2:obj) => ((z E w1_2): >> prop)] >> ,(xev Lemma2 zev),Eqsymm(line8)): >> that (z E (xev upair yev)))] >> {move 1:current} define line18 line11 : comp2(line17 line11) >> line18: [(line11_1:that ~((y = z))) >> => (comp2(line17(line11_1)):that >> ((x = z) v (y = z)))] >> {move 1:current} open declare notso that ~(x=z) >> notso: that ~((x = z)) {move 3} define line19 notso : Mp (notso, line18 line11) >> line19: [(notso_1:that ~((x = z))) >> => ((notso_1 Mp line18(line11)): >> that (y = z))] >> {move 2} define line20 notso : Mp (line19 notso,line11) >> line20: [(notso_1:that ~((x = z))) >> => ((line19(notso_1) Mp line11): >> that ??)] >> {move 2} close define line21 line11 : Dneg(Deduction line20) >> line21: [(line11_1:that ~((y = z))) >> => (Dneg(Deduction([(notso_2:that >> ~((x = z))) => (((notso_2 >> Mp line18(line11_1)) Mp line11_1): >> that ??)])) >> :that (x = z))] >> {move 1:current} open declare w1 obj >> w1: obj {move 3} define equalsz w1: w1=z >> equalsz: [(w1_1:obj) => ((w1_1 >> = z):prop)] >> {move 2} close define line22 line11 : Subs(equalsz,line21 line11,line16 line11) >> line22: [(line11_1:that ~((y = z))) >> => (Subs([(w1_2:obj) => ((w1_2 >> = z):prop)] >> ,line21(line11_1),line16(line11_1)): >> that (y = z))] >> {move 1:current} define line23 line11 : Mp (line22 line11,line11) >> line23: [(line11_1:that ~((y = z))) >> => ((line22(line11_1) Mp line11_1): >> that ??)] >> {move 1:current} close define Lemma3 line8 : Dneg(Deduction line23) >> Lemma3: [(.x_1:obj),(.xev_1:that (.x_1 E >> V)),(.y_1:obj),(.yev_1:that (.y_1 E >> V)),(.z_1:obj),(.zev_1:that (.z_1 E >> V)),(line8_1:that ((.xev_1 upair .yev_1) >> = (.xev_1 upair .zev_1))) => (Dneg(Deduction([(line11_2: >> that ~((.y_1 = .z_1))) => ((Subs([(w1_3: >> obj) => ((w1_3 = .z_1):prop)] >> ,Dneg(Deduction([(notso_4:that >> ~((.x_1 = .z_1))) => (((notso_4 >> Mp comp2(Subs([(w1_6:obj) >> => ((.z_1 E w1_6):prop)] >> ,(.xev_1 Lemma2 .zev_1),Eqsymm(line8_1)))) >> Mp line11_2):that ??)])) >> ,Dneg(Deduction([(line12_7:that >> ~((.x_1 = .y_1))) => ((Eqsymm((line12_7 >> Mp line10(line8_1))) Mp line11_2): >> that ??)])) >> ) Mp line11_2):that ??)])) >> :that (.y_1 = .z_1))] >> {move 0} declare w obj >> w: obj {move 1:current} declare wev that w E V >> wev: that (w E V) {move 1:current} declare xxev2 that (xev upair xev) E V >> xxev2: that ((xev upair xev) E V) {move 1: >> current} declare xyev2 that (xev upair yev) E V >> xyev2: that ((xev upair yev) E V) {move 1: >> current} declare zzev that (zev upair zev) E V >> zzev: that ((zev upair zev) E V) {move 1: >> current} declare zwev that (zev upair wev) E V >> zwev: that ((zev upair wev) E V) {move 1: >> current} declare xyzwev that (xxev2 upair xyev2) = (zzev upair zwev) >> xyzwev: that ((xxev2 upair xyev2) = (zzev >> upair zwev)) {move 1:current} define line24 xyzwev : comp2(Subs(E(xev upair xev),Lemma1 xxev2 xyev2,xyzwev)) >> line24: [(.x_1:obj),(.xev_1:that (.x_1 E >> V)),(.xxev2_1:that ((.xev_1 upair .xev_1) >> E V)),(.y_1:obj),(.yev_1:that (.y_1 >> E V)),(.xyev2_1:that ((.xev_1 upair >> .yev_1) E V)),(.z_1:obj),(.zev_1:that >> (.z_1 E V)),(.zzev_1:that ((.zev_1 upair >> .zev_1) E V)),(.w_1:obj),(.wev_1:that >> (.w_1 E V)),(.zwev_1:that ((.zev_1 upair >> .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (comp2(Subs([(y_3:obj) => (((.xev_1 >> upair .xev_1) E y_3):prop)] >> ,(.xxev2_1 Lemma1 .xyev2_1),xyzwev_1)): >> that (((.zev_1 upair .zev_1) = (.xev_1 >> upair .xev_1)) v ((.zev_1 upair .wev_1) >> = (.xev_1 upair .xev_1))))] >> {move 0} define revline24 xyzwev : line24(Eqsymm xyzwev) >> revline24: [(.x_1:obj),(.xev_1:that (.x_1 >> E V)),(.xxev2_1:that ((.xev_1 upair >> .xev_1) E V)),(.y_1:obj),(.yev_1:that >> (.y_1 E V)),(.xyev2_1:that ((.xev_1 >> upair .yev_1) E V)),(.z_1:obj),(.zev_1: >> that (.z_1 E V)),(.zzev_1:that ((.zev_1 >> upair .zev_1) E V)),(.w_1:obj),(.wev_1: >> that (.w_1 E V)),(.zwev_1:that ((.zev_1 >> upair .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (line24(Eqsymm(xyzwev_1)):that (((.xev_1 >> upair .xev_1) = (.zev_1 upair .zev_1)) >> v ((.xev_1 upair .yev_1) = (.zev_1 upair >> .zev_1))))] >> {move 0} define line25 xyzwev : comp2(Subs(E(xev upair yev),Lemma2 xxev2 xyev2,xyzwev)) >> line25: [(.x_1:obj),(.xev_1:that (.x_1 E >> V)),(.xxev2_1:that ((.xev_1 upair .xev_1) >> E V)),(.y_1:obj),(.yev_1:that (.y_1 >> E V)),(.xyev2_1:that ((.xev_1 upair >> .yev_1) E V)),(.z_1:obj),(.zev_1:that >> (.z_1 E V)),(.zzev_1:that ((.zev_1 upair >> .zev_1) E V)),(.w_1:obj),(.wev_1:that >> (.w_1 E V)),(.zwev_1:that ((.zev_1 upair >> .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (comp2(Subs([(y_3:obj) => (((.xev_1 >> upair .yev_1) E y_3):prop)] >> ,(.xxev2_1 Lemma2 .xyev2_1),xyzwev_1)): >> that (((.zev_1 upair .zev_1) = (.xev_1 >> upair .yev_1)) v ((.zev_1 upair .wev_1) >> = (.xev_1 upair .yev_1))))] >> {move 0} define revline25 xyzwev : line25(Eqsymm xyzwev) >> revline25: [(.x_1:obj),(.xev_1:that (.x_1 >> E V)),(.xxev2_1:that ((.xev_1 upair >> .xev_1) E V)),(.y_1:obj),(.yev_1:that >> (.y_1 E V)),(.xyev2_1:that ((.xev_1 >> upair .yev_1) E V)),(.z_1:obj),(.zev_1: >> that (.z_1 E V)),(.zzev_1:that ((.zev_1 >> upair .zev_1) E V)),(.w_1:obj),(.wev_1: >> that (.w_1 E V)),(.zwev_1:that ((.zev_1 >> upair .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (line25(Eqsymm(xyzwev_1)):that (((.xev_1 >> upair .xev_1) = (.zev_1 upair .wev_1)) >> v ((.xev_1 upair .yev_1) = (.zev_1 upair >> .wev_1))))] >> {move 0} open declare line26 that ~(x=z) >> line26: that ~((x = z)) {move 2} open declare line27 that (zev upair zev) = xev upair xev >> line27: that ((zev upair zev) = >> (xev upair xev)) {move 3} define line28 line27: comp2(Subs(E(z),Lemma1 zev zev,line27)) >> line28: [(line27_1:that ((zev upair >> zev) = (xev upair xev))) => >> (comp2(Subs([(y_3:obj) => >> ((z E y_3):prop)] >> ,(zev Lemma1 zev),line27_1)): >> that ((x = z) v (x = z)))] >> {move 2} define line29 line27: Mp line26 line28 line27 >> line29: [(line27_1:that ((zev upair >> zev) = (xev upair xev))) => >> ((line26 Mp line28(line27_1)): >> that (x = z))] >> {move 2} define line30 line27: Mp line29 line27 line26 >> line30: [(line27_1:that ((zev upair >> zev) = (xev upair xev))) => >> ((line29(line27_1) Mp line26): >> that ??)] >> {move 2} close define line31 line26 : Deduction line30 >> line31: [(line26_1:that ~((x = z))) >> => (Deduction([(line27_2:that ((zev >> upair zev) = (xev upair xev))) >> => (((line26_1 Mp comp2(Subs([(y_4: >> obj) => ((z E y_4):prop)] >> ,(zev Lemma1 zev),line27_2))) >> Mp line26_1):that ??)]) >> :that (((zev upair zev) = (xev >> upair xev)) -> ??))] >> {move 1:current} define line32 line26 : Mp line31 line26 line24 xyzwev >> line32: [(line26_1:that ~((x = z))) >> => ((line31(line26_1) Mp line24(xyzwev)): >> that ((zev upair wev) = (xev upair >> xev)))] >> {move 1:current} define line33 line26 : comp2(Subs(E(z),Lemma1 zev wev,line32 line26)) >> line33: [(line26_1:that ~((x = z))) >> => (comp2(Subs([(y_3:obj) => ((z >> E y_3):prop)] >> ,(zev Lemma1 wev),line32(line26_1))): >> that ((x = z) v (x = z)))] >> {move 1:current} define line34 line26 : Mp line26 line33 line26 >> line34: [(line26_1:that ~((x = z))) >> => ((line26_1 Mp line33(line26_1)): >> that (x = z))] >> {move 1:current} define line35 line26 : Mp line34 line26 line26 >> line35: [(line26_1:that ~((x = z))) >> => ((line34(line26_1) Mp line26_1): >> that ??)] >> {move 1:current} close define Firstprojeq xyzwev : Dneg(Deduction line35) >> Firstprojeq: [(.x_1:obj),(.xev_1:that (.x_1 >> E V)),(.xxev2_1:that ((.xev_1 upair >> .xev_1) E V)),(.y_1:obj),(.yev_1:that >> (.y_1 E V)),(.xyev2_1:that ((.xev_1 >> upair .yev_1) E V)),(.z_1:obj),(.zev_1: >> that (.z_1 E V)),(.zzev_1:that ((.zev_1 >> upair .zev_1) E V)),(.w_1:obj),(.wev_1: >> that (.w_1 E V)),(.zwev_1:that ((.zev_1 >> upair .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (Dneg(Deduction([(line26_2:that ~((.x_1 >> = .z_1))) => (((line26_2 Mp comp2(Subs([(y_4: >> obj) => ((.z_1 E y_4):prop)] >> ,(.zev_1 Lemma1 .wev_1),(Deduction([(line27_5: >> that ((.zev_1 upair .zev_1) >> = (.xev_1 upair .xev_1))) >> => (((line26_2 Mp comp2(Subs([(y_7: >> obj) => ((.z_1 E y_7): >> prop)] >> ,(.zev_1 Lemma1 .zev_1),line27_5))) >> Mp line26_2):that ??)]) >> Mp line24(xyzwev_1))))) Mp line26_2): >> that ??)])) >> :that (.x_1 = .z_1))] >> {move 0} open declare line36 that ~(y=w) >> line36: that ~((y = w)) {move 2} open declare line37 that (zev upair zev) = xev upair yev >> line37: that ((zev upair zev) = >> (xev upair yev)) {move 3} define line38 line37 : comp2(Subs(E(y),Lemma2 xev yev,Eqsymm line37)) >> line38: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> (comp2(Subs([(y_3:obj) => >> ((y E y_3):prop)] >> ,(xev Lemma2 yev),Eqsymm(line37_1))): >> that ((z = y) v (z = y)))] >> {move 2} define line39 line37 : Eqsymm(Selfor line38 line37) >> line39: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> (Eqsymm(Selfor(line38(line37_1))): >> that (y = z))] >> {move 2} open declare line40 that (xev upair xev) = zev upair wev >> line40: that ((xev upair xev) >> = (zev upair wev)) {move 4} define line41 line40 : Selfor(comp2(Subs(E(w),Lemma2 zev wev,Eqsymm line40))) >> line41: [(line40_1:that ((xev >> upair xev) = (zev upair >> wev))) => (Selfor(comp2(Subs([(y_3: >> obj) => ((w E y_3): >> prop)] >> ,(zev Lemma2 wev),Eqsymm(line40_1)))): >> that (x = w))] >> {move 3} define line42 line40 : Transeq Eqsymm line41 line40 Firstprojeq xyzwev >> line42: [(line40_1:that ((xev >> upair xev) = (zev upair >> wev))) => ((Eqsymm(line41(line40_1)) >> Transeq Firstprojeq(xyzwev)): >> that (w = z))] >> {move 3} define line43 line40 : Transeq line39 line37 Eqsymm line42 line40 >> line43: [(line40_1:that ((xev >> upair xev) = (zev upair >> wev))) => ((line39(line37) >> Transeq Eqsymm(line42(line40_1))): >> that (y = w))] >> {move 3} define line44 line40 : Mp line43 line40 line36 >> line44: [(line40_1:that ((xev >> upair xev) = (zev upair >> wev))) => ((line43(line40_1) >> Mp line36):that ??)] >> {move 3} close define line45 line37 : Deduction line44 >> line45: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> (Deduction([(line40_2:that >> ((xev upair xev) = (zev >> upair wev))) => (((line39(line37_1) >> Transeq Eqsymm((Eqsymm(Selfor(comp2(Subs([(y_4: >> obj) => ((w E y_4): >> prop)] >> ,(zev Lemma2 wev),Eqsymm(line40_2))))) >> Transeq Firstprojeq(xyzwev)))) >> Mp line36):that ??)]) >> :that (((xev upair xev) = >> (zev upair wev)) -> ??))] >> {move 2} define line46 line37 : Mp line45 line37 revline25 xyzwev >> line46: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> ((line45(line37_1) Mp revline25(xyzwev)): >> that ((xev upair yev) = (zev >> upair wev)))] >> {move 2} open declare x1 obj >> x1: obj {move 4} declare xev1 that x1 E V >> xev1: that (x1 E V) {move >> 4} define noncepreda x1 xev1 : (xev1 upair yev) = zev upair wev >> noncepreda: [(x1_1:obj),(xev1_1: >> that (x1_1 E V)) => (((xev1_1 >> upair yev) = (zev upair >> wev)):prop)] >> {move 3} close define line47 line37: Lemma3 Subs2 isset, noncepreda, zev line46 line37 Firstprojeq xyzwev >> line47: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> (Lemma3(Subs2(isset,[(x1_2: >> obj),(xev1_2:that (x1_2 >> E V)) => (((xev1_2 upair >> yev) = (zev upair wev)): >> prop)] >> ,zev,line46(line37_1),Firstprojeq(xyzwev))): >> that (y = w))] >> {move 2} define line48 line37: Mp line47 line37 line36 >> line48: [(line37_1:that ((zev upair >> zev) = (xev upair yev))) => >> ((line47(line37_1) Mp line36): >> that ??)] >> {move 2} close define line49 line36 : Deduction line48 >> line49: [(line36_1:that ~((y = w))) >> => (Deduction([(line37_2:that ((zev >> upair zev) = (xev upair yev))) >> => ((Lemma3(Subs2(isset,[(x1_3: >> obj),(xev1_3:that (x1_3 >> E V)) => (((xev1_3 upair >> yev) = (zev upair wev)): >> prop)] >> ,zev,(Deduction([(line40_4: >> that ((xev upair xev) >> = (zev upair wev))) => >> (((Eqsymm(Selfor(comp2(Subs([(y_6: >> obj) => ((y E y_6): >> prop)] >> ,(xev Lemma2 yev),Eqsymm(line37_2))))) >> Transeq Eqsymm((Eqsymm(Selfor(comp2(Subs([(y_8: >> obj) => ((w E y_8): >> prop)] >> ,(zev Lemma2 wev),Eqsymm(line40_4))))) >> Transeq Firstprojeq(xyzwev)))) >> Mp line36_1):that ??)]) >> Mp revline25(xyzwev)),Firstprojeq(xyzwev))) >> Mp line36_1):that ??)]) >> :that (((zev upair zev) = (xev >> upair yev)) -> ??))] >> {move 1:current} define line50 line36 : Mp line49 line36 line25 xyzwev >> line50: [(line36_1:that ~((y = w))) >> => ((line49(line36_1) Mp line25(xyzwev)): >> that ((zev upair wev) = (xev upair >> yev)))] >> {move 1:current} open declare x1 obj >> x1: obj {move 3} declare xev1 that x1 E V >> xev1: that (x1 E V) {move 3} define noncepred x1 xev1 : (zev upair wev) = xev1 upair yev >> noncepred: [(x1_1:obj),(xev1_1: >> that (x1_1 E V)) => (((zev >> upair wev) = (xev1_1 upair >> yev)):prop)] >> {move 2} close define line51 line36 : Eqsymm Lemma3 Subs2 isset, noncepred, zev line50 line36 Firstprojeq xyzwev >> line51: [(line36_1:that ~((y = w))) >> => (Eqsymm(Lemma3(Subs2(isset,[(x1_2: >> obj),(xev1_2:that (x1_2 E >> V)) => (((zev upair wev) = >> (xev1_2 upair yev)):prop)] >> ,zev,line50(line36_1),Firstprojeq(xyzwev)))): >> that (y = w))] >> {move 1:current} define line52 line36 : Mp line51 line36 line36 >> line52: [(line36_1:that ~((y = w))) >> => ((line51(line36_1) Mp line36_1): >> that ??)] >> {move 1:current} close define Secondprojeq xyzwev : Dneg(Deduction line52) >> Secondprojeq: [(.x_1:obj),(.xev_1:that (.x_1 >> E V)),(.xxev2_1:that ((.xev_1 upair >> .xev_1) E V)),(.y_1:obj),(.yev_1:that >> (.y_1 E V)),(.xyev2_1:that ((.xev_1 >> upair .yev_1) E V)),(.z_1:obj),(.zev_1: >> that (.z_1 E V)),(.zzev_1:that ((.zev_1 >> upair .zev_1) E V)),(.w_1:obj),(.wev_1: >> that (.w_1 E V)),(.zwev_1:that ((.zev_1 >> upair .wev_1) E V)),(xyzwev_1:that ((.xxev2_1 >> upair .xyev2_1) = (.zzev_1 upair .zwev_1))) >> => (Dneg(Deduction([(line36_2:that ~((.y_1 >> = .w_1))) => ((Eqsymm(Lemma3(Subs2([(x1_3: >> obj) => ((x1_3 E V):prop)] >> ,[(x1_4:obj),(xev1_4:that (x1_4 >> E V)) => (((.zev_1 upair .wev_1) >> = (xev1_4 upair .yev_1)):prop)] >> ,.zev_1,(Deduction([(line37_5:that >> ((.zev_1 upair .zev_1) = (.xev_1 >> upair .yev_1))) => ((Lemma3(Subs2([(x1_6: >> obj) => ((x1_6 E V):prop)] >> ,[(x1_7:obj),(xev1_7:that >> (x1_7 E V)) => (((xev1_7 >> upair .yev_1) = (.zev_1 >> upair .wev_1)):prop)] >> ,.zev_1,(Deduction([(line40_8: >> that ((.xev_1 upair .xev_1) >> = (.zev_1 upair .wev_1))) >> => (((Eqsymm(Selfor(comp2(Subs([(y_10: >> obj) => ((.y_1 E >> y_10):prop)] >> ,(.xev_1 Lemma2 .yev_1), >> Eqsymm(line37_5))))) >> Transeq Eqsymm((Eqsymm(Selfor(comp2(Subs([(y_12: >> obj) => ((.w_1 E >> y_12):prop)] >> ,(.zev_1 Lemma2 .wev_1), >> Eqsymm(line40_8))))) >> Transeq Firstprojeq(xyzwev_1)))) >> Mp line36_2):that ??)]) >> Mp revline25(xyzwev_1)),Firstprojeq(xyzwev_1))) >> Mp line36_2):that ??)]) >> Mp line25(xyzwev_1)),Firstprojeq(xyzwev_1)))) >> Mp line36_2):that ??)])) >> :that (.y_1 = .w_1))] >> {move 0} open declare x1 obj >> x1: obj {move 2} define Notpred x1 : ~(Pred x1) >> Notpred: [(x1_1:obj) => (~(Pred(x1_1)): >> prop)] >> {move 1:current} close define Exists Pred : ~ Forall Notpred >> Exists: [(Pred_1:[(x1_2:obj) => (---:prop)]) >> => (~(Forall([(x1_3:obj) => (~(Pred_1(x1_3)): >> prop)])) >> :prop)] >> {move 0} % define bijection from A to B declare A obj >> A: obj {move 1:current} declare B obj >> B: obj {move 1:current} declare a obj >> a: obj {move 1:current} declare aina that a E A >> aina: that (a E A) {move 1:current} declare b obj >> b: obj {move 1:current} declare binb that b E B >> binb: that (b E B) {move 1:current} define aev aina : comp3 aina >> aev: [(.a_1:obj),(.A_1:obj),(aina_1:that >> (.a_1 E .A_1)) => (comp3(aina_1):that >> (.a_1 E V))] >> {move 0} declare f obj >> f: obj {move 1:current} % define "f is a relation from A to B" % define the predicate "is an unordered pair" open declare y1 obj >> y1: obj {move 2} open declare z1 obj >> z1: obj {move 3} open declare w1 obj >> w1: obj {move 4} define inthepair w1 : (w1 = y1) v w1 = z1 >> inthepair: [(w1_1:obj) => >> (((w1_1 = y1) v (w1_1 >> = z1)):prop)] >> {move 3} close define isthepairz z1 : ((z1 E V) & x = Classof inthepair) >> isthepairz: [(z1_1:obj) => (((z1_1 >> E V) & (x = Classof([(w1_2: >> obj) => (((w1_2 = y1) >> v (w1_2 = z1_1)):prop)])) >> ):prop)] >> {move 2} close define isthepairy y1 : (y1 E V) & Exists isthepairz >> isthepairy: [(y1_1:obj) => (((y1_1 E >> V) & Exists([(z1_2:obj) => (((z1_2 >> E V) & (x = Classof([(w1_3: >> obj) => (((w1_3 = y1_1) >> v (w1_3 = z1_2)):prop)])) >> ):prop)])) >> :prop)] >> {move 1:current} close define isunorderedpair x : Exists isthepairy >> isunorderedpair: [(x_1:obj) => (Exists([(y1_2: >> obj) => (((y1_2 E V) & Exists([(z1_3: >> obj) => (((z1_3 E V) & (x_1 >> = Classof([(w1_4:obj) => (((w1_4 >> = y1_2) v (w1_4 = z1_3)): >> prop)])) >> ):prop)])) >> :prop)]) >> :prop)] >> {move 0} % define the predicate "is an ordered pair" open declare y1 obj >> y1: obj {move 2} open declare z1 obj >> z1: obj {move 3} open declare w1 obj >> w1: obj {move 4} define inthesingleton w1 : w1 = y1 >> inthesingleton: [(w1_1:obj) >> => ((w1_1 = y1):prop)] >> {move 3} define inthepair w1 : (w1=y1) v w1=z1 >> inthepair: [(w1_1:obj) => >> (((w1_1 = y1) v (w1_1 >> = z1)):prop)] >> {move 3} declare u1 obj >> u1: obj {move 4} define intheorderedpair u1 : (u1 = Classof inthesingleton) v u1 = Classof inthepair >> intheorderedpair: [(u1_1:obj) >> => (((u1_1 = Classof(inthesingleton)) >> v (u1_1 = Classof(inthepair))): >> prop)] >> {move 3} close define istheorderedpairz z1 : (z1 E V) & ((Classof inthesingleton) E V) & ((Classof inthepair) E V) & x = Classof intheorderedpair >> istheorderedpairz: [(z1_1:obj) >> => (((z1_1 E V) & ((Classof([(w1_2: >> obj) => ((w1_2 = y1): >> prop)]) >> E V) & ((Classof([(w1_3:obj) >> => (((w1_3 = y1) v (w1_3 >> = z1_1)):prop)]) >> E V) & (x = Classof([(u1_4: >> obj) => (((u1_4 = Classof([(w1_5: >> obj) => ((w1_5 = >> y1):prop)])) >> v (u1_4 = Classof([(w1_6: >> obj) => (((w1_6 >> = y1) v (w1_6 = >> z1_1)):prop)])) >> ):prop)])) >> ))):prop)] >> {move 2} close define istheorderedpairy y1 : (y1 E V) & Exists istheorderedpairz >> istheorderedpairy: [(y1_1:obj) => (((y1_1 >> E V) & Exists([(z1_2:obj) => (((z1_2 >> E V) & ((Classof([(w1_3:obj) >> => ((w1_3 = y1_1):prop)]) >> E V) & ((Classof([(w1_4:obj) >> => (((w1_4 = y1_1) v >> (w1_4 = z1_2)):prop)]) >> E V) & (x = Classof([(u1_5: >> obj) => (((u1_5 = Classof([(w1_6: >> obj) => ((w1_6 = >> y1_1):prop)])) >> v (u1_5 = Classof([(w1_7: >> obj) => (((w1_7 >> = y1_1) v (w1_7 >> = z1_2)):prop)])) >> ):prop)])) >> ))):prop)])) >> :prop)] >> {move 1:current} close define isanorderedpair x : Exists istheorderedpairy >> isanorderedpair: [(x_1:obj) => (Exists([(y1_2: >> obj) => (((y1_2 E V) & Exists([(z1_3: >> obj) => (((z1_3 E V) & ((Classof([(w1_4: >> obj) => ((w1_4 = y1_2): >> prop)]) >> E V) & ((Classof([(w1_5:obj) >> => (((w1_5 = y1_2) v >> (w1_5 = z1_3)):prop)]) >> E V) & (x_1 = Classof([(u1_6: >> obj) => (((u1_6 = Classof([(w1_7: >> obj) => ((w1_7 = >> y1_2):prop)])) >> v (u1_6 = Classof([(w1_8: >> obj) => (((w1_8 >> = y1_2) v (w1_8 >> = z1_3)):prop)])) >> ):prop)])) >> ))):prop)])) >> :prop)]) >> :prop)] >> {move 0} open declare x1 obj >> x1: obj {move 2} define xinfispair1 x1: (x1 E f) -> isanorderedpair x1 >> xinfispair1: [(x1_1:obj) => (((x1_1 >> E f) -> isanorderedpair(x1_1)): >> prop)] >> {move 1:current} close % define "f is a relation" define Relation f: Forall xinfispair1 >> Relation: [(f_1:obj) => (Forall([(x1_2:obj) >> => (((x1_2 E f_1) -> isanorderedpair(x1_2)): >> prop)]) >> :prop)] >> {move 0} open declare w1 obj >> w1: obj {move 2} define inthepair0 w1: (x=w1) v y=w1 >> inthepair0: [(w1_1:obj) => (((x = w1_1) >> v (y = w1_1)):prop)] >> {move 1:current} close % pair definitions without evidence components define upair0 x y: Classof inthepair0 >> upair0: [(x_1:obj),(y_1:obj) => (Classof([(w1_2: >> obj) => (((x_1 = w1_2) v (y_1 = >> w1_2)):prop)]) >> :obj)] >> {move 0} define opair0 x y: (x upair0 x) upair0 upair0 x y >> opair0: [(x_1:obj),(y_1:obj) => (((x_1 upair0 >> x_1) upair0 (x_1 upair0 y_1)):obj)] >> {move 0} %% prove that the definitions are the same. Note sensitivity to order of equations. % of course they are only the same in the presence of evidence. define samedef1 xev yev : Fixfun((upair xev yev) = upair0 x y,Refleq upair xev yev) >> samedef1: [(.x_1:obj),(xev_1:that (.x_1 E >> V)),(.y_1:obj),(yev_1:that (.y_1 E V)) >> => ((((xev_1 upair yev_1) = (.x_1 upair0 >> .y_1)) Fixfun Refleq((xev_1 upair yev_1))): >> that ((xev_1 upair yev_1) = (.x_1 upair0 >> .y_1)))] >> {move 0} % define "f is a function" open declare x1 obj >> x1: obj {move 2} open declare y1 obj >> y1: obj {move 3} open declare z1 obj >> z1: obj {move 4} define thesituationz z1: ((x1 E V) & (y1 E V) & (z1 E V) & ((x1 upair0 x1) E V) & ((x1 upair0 y1) E V) & ((x1 upair0 z1) E V) & ((x1 opair0 y1) E f) & ((x1 opair0 z1) E f)) -> y1 = z1 >> thesituationz: [(z1_1:obj) >> => ((((x1 E V) & ((y1 >> E V) & ((z1_1 E V) & >> (((x1 upair0 x1) E V) >> & (((x1 upair0 y1) E >> V) & (((x1 upair0 z1_1) >> E V) & (((x1 opair0 y1) >> E f) & ((x1 opair0 z1_1) >> E f)))))))) -> (y1 = >> z1_1)):prop)] >> {move 3} close define thesituationy y1: Forall thesituationz >> thesituationy: [(y1_1:obj) => (Forall([(z1_2: >> obj) => ((((x1 E V) & >> ((y1_1 E V) & ((z1_2 >> E V) & (((x1 upair0 x1) >> E V) & (((x1 upair0 y1_1) >> E V) & (((x1 upair0 z1_2) >> E V) & (((x1 opair0 y1_1) >> E f) & ((x1 opair0 z1_2) >> E f)))))))) -> (y1_1 >> = z1_2)):prop)]) >> :prop)] >> {move 2} close define thesituationx x1: Forall thesituationy >> thesituationx: [(x1_1:obj) => (Forall([(y1_2: >> obj) => (Forall([(z1_3:obj) >> => ((((x1_1 E V) & ((y1_2 >> E V) & ((z1_3 E V) & >> (((x1_1 upair0 x1_1) >> E V) & (((x1_1 upair0 >> y1_2) E V) & (((x1_1 >> upair0 z1_3) E V) & (((x1_1 >> opair0 y1_2) E f) & ((x1_1 >> opair0 z1_3) E f)))))))) >> -> (y1_2 = z1_3)):prop)]) >> :prop)]) >> :prop)] >> {move 1:current} close define Function f : (Relation f) & Forall thesituationx >> Function: [(f_1:obj) => ((Relation(f_1) & >> Forall([(x1_2:obj) => (Forall([(y1_3: >> obj) => (Forall([(z1_4:obj) >> => ((((x1_2 E V) & ((y1_3 >> E V) & ((z1_4 E V) & >> (((x1_2 upair0 x1_2) >> E V) & (((x1_2 upair0 >> y1_3) E V) & (((x1_2 >> upair0 z1_4) E V) & (((x1_2 >> opair0 y1_3) E f_1) & >> ((x1_2 opair0 z1_4) E >> f_1)))))))) -> (y1_3 >> = z1_4)):prop)]) >> :prop)]) >> :prop)])) >> :prop)] >> {move 0} % define "f is the inverse of a function" open declare x1 obj >> x1: obj {move 2} open declare y1 obj >> y1: obj {move 3} open declare z1 obj >> z1: obj {move 4} define thesituationz z1: ((x1 E V) & (y1 E V) & (z1 E V) & ((x1 upair0 x1) E V) & ((y1 upair0 y1) E V) & ((x1 upair0 z1) E V) & ((y1 upair0 z1) E V) & ((x1 opair0 z1) E f) & ((y1 opair0 z1) E f)) -> x1 = y1 >> thesituationz: [(z1_1:obj) >> => ((((x1 E V) & ((y1 >> E V) & ((z1_1 E V) & >> (((x1 upair0 x1) E V) >> & (((y1 upair0 y1) E >> V) & (((x1 upair0 z1_1) >> E V) & (((y1 upair0 z1_1) >> E V) & (((x1 opair0 z1_1) >> E f) & ((y1 opair0 z1_1) >> E f))))))))) -> (x1 = >> y1)):prop)] >> {move 3} close define thesituationy y1: Forall thesituationz >> thesituationy: [(y1_1:obj) => (Forall([(z1_2: >> obj) => ((((x1 E V) & >> ((y1_1 E V) & ((z1_2 >> E V) & (((x1 upair0 x1) >> E V) & (((y1_1 upair0 >> y1_1) E V) & (((x1 upair0 >> z1_2) E V) & (((y1_1 >> upair0 z1_2) E V) & (((x1 >> opair0 z1_2) E f) & ((y1_1 >> opair0 z1_2) E f))))))))) >> -> (x1 = y1_1)):prop)]) >> :prop)] >> {move 2} close define thesituationx2 x1: Forall thesituationy >> thesituationx2: [(x1_1:obj) => (Forall([(y1_2: >> obj) => (Forall([(z1_3:obj) >> => ((((x1_1 E V) & ((y1_2 >> E V) & ((z1_3 E V) & >> (((x1_1 upair0 x1_1) >> E V) & (((y1_2 upair0 >> y1_2) E V) & (((x1_1 >> upair0 z1_3) E V) & (((y1_2 >> upair0 z1_3) E V) & (((x1_1 >> opair0 z1_3) E f) & ((y1_2 >> opair0 z1_3) E f))))))))) >> -> (x1_1 = y1_2)):prop)]) >> :prop)]) >> :prop)] >> {move 1:current} close define Inversefn f : (Relation f) & Forall thesituationx2 >> Inversefn: [(f_1:obj) => ((Relation(f_1) >> & Forall([(x1_2:obj) => (Forall([(y1_3: >> obj) => (Forall([(z1_4:obj) >> => ((((x1_2 E V) & ((y1_3 >> E V) & ((z1_4 E V) & >> (((x1_2 upair0 x1_2) >> E V) & (((y1_3 upair0 >> y1_3) E V) & (((x1_2 >> upair0 z1_4) E V) & (((y1_3 >> upair0 z1_4) E V) & (((x1_2 >> opair0 z1_4) E f_1) & >> ((y1_3 opair0 z1_4) E >> f_1))))))))) -> (x1_2 >> = y1_3)):prop)]) >> :prop)]) >> :prop)])) >> :prop)] >> {move 0} % define the domain of f open declare x1 obj >> x1: obj {move 2} open declare y1 obj >> y1: obj {move 3} define indomainy y1 : (x1 E V) & (y1 E V) & ((upair0 x1 x1) E V) & ((upair0 x1 y1) E V) & (opair0 x1 y1) E f >> indomainy: [(y1_1:obj) => (((x1 >> E V) & ((y1_1 E V) & (((x1 >> upair0 x1) E V) & (((x1 upair0 >> y1_1) E V) & ((x1 opair0 y1_1) >> E f))))):prop)] >> {move 2} close define indomainx x1: Exists indomainy >> indomainx: [(x1_1:obj) => (Exists([(y1_2: >> obj) => (((x1_1 E V) & ((y1_2 >> E V) & (((x1_1 upair0 x1_1) >> E V) & (((x1_1 upair0 y1_2) >> E V) & ((x1_1 opair0 y1_2) >> E f))))):prop)]) >> :prop)] >> {move 1:current} close define Domain f : Classof indomainx >> Domain: [(f_1:obj) => (Classof([(x1_2:obj) >> => (Exists([(y1_3:obj) => (((x1_2 >> E V) & ((y1_3 E V) & (((x1_2 >> upair0 x1_2) E V) & (((x1_2 >> upair0 y1_3) E V) & ((x1_2 >> opair0 y1_3) E f_1))))):prop)]) >> :prop)]) >> :obj)] >> {move 0} % define the range of f open declare y1 obj >> y1: obj {move 2} open declare x1 obj >> x1: obj {move 3} define inrangex x1 : (x1 E V) & (y1 E V) & ((upair0 x1 x1) E V) & ((upair0 x1 y1) E V) & (opair0 x1 y1) E f >> inrangex: [(x1_1:obj) => (((x1_1 >> E V) & ((y1 E V) & (((x1_1 >> upair0 x1_1) E V) & (((x1_1 >> upair0 y1) E V) & ((x1_1 opair0 >> y1) E f))))):prop)] >> {move 2} close define inrangey y1: Exists inrangex >> inrangey: [(y1_1:obj) => (Exists([(x1_2: >> obj) => (((x1_2 E V) & ((y1_1 >> E V) & (((x1_2 upair0 x1_2) >> E V) & (((x1_2 upair0 y1_1) >> E V) & ((x1_2 opair0 y1_1) >> E f))))):prop)]) >> :prop)] >> {move 1:current} close define Range f : Classof inrangey >> Range: [(f_1:obj) => (Classof([(y1_2:obj) >> => (Exists([(x1_3:obj) => (((x1_3 >> E V) & ((y1_2 E V) & (((x1_3 >> upair0 x1_3) E V) & (((x1_3 >> upair0 y1_2) E V) & ((x1_3 >> opair0 y1_2) E f_1))))):prop)]) >> :prop)]) >> :obj)] >> {move 0} define Bijection A B f : (A = Domain f) & (B = Range f) & (Function f) & Inversefn f >> Bijection: [(A_1:obj),(B_1:obj),(f_1:obj) >> => (((A_1 = Domain(f_1)) & ((B_1 = Range(f_1)) >> & (Function(f_1) & Inversefn(f_1)))): >> prop)] >> {move 0} define Samesize A B : Exists(Bijection(A,B)) >> Samesize: [(A_1:obj),(B_1:obj) => (Exists([(f_2: >> obj) => (Bijection(A_1,B_1,f_2): >> prop)]) >> :prop)] >> {move 0} define <-> p q : (p->q) & q->p >> <->: [(p_1:prop),(q_1:prop) => (((p_1 -> >> q_1) & (q_1 -> p_1)):prop)] >> {move 0} open declare C1 obj >> C1: obj {move 2} open declare D1 obj >> D1: obj {move 3} define vonneumannd D1 : ~(C1 E V) -> ~(D1 E V) <-> C1 Samesize D1 >> vonneumannd: [(D1_1:obj) => ((~((C1 >> E V)) -> (~((D1_1 E V)) <-> >> (C1 Samesize D1_1))):prop)] >> {move 2} close define vonneumannc C1 : Forall vonneumannd >> vonneumannc: [(C1_1:obj) => (Forall([(D1_2: >> obj) => ((~((C1_1 E V)) -> >> (~((D1_2 E V)) <-> (C1_1 Samesize >> D1_2))):prop)]) >> :prop)] >> {move 1:current} close construct Vonneumann that Forall vonneumannc >> Vonneumann: that Forall([(C1_1:obj) => (Forall([(D1_2: >> obj) => ((~((C1_1 E V)) -> (~((D1_2 >> E V)) <-> (C1_1 Samesize D1_2))): >> prop)]) >> :prop)]) >> {move 0} open declare z1 obj >> z1: obj {move 2} define subset0 z1 : (z1 E x) -> z1 E y >> subset0: [(z1_1:obj) => (((z1_1 E x) >> -> (z1_1 E y)):prop)] >> {move 1:current} close define c x y : Forall subset0 >> c: [(x_1:obj),(y_1:obj) => (Forall([(z1_2: >> obj) => (((z1_2 E x_1) -> (z1_2 >> E y_1)):prop)]) >> :prop)] >> {move 0} define cneq x y : (x c y) & ~(x c y) >> cneq: [(x_1:obj),(y_1:obj) => (((x_1 c y_1) >> & ~((x_1 c y_1))):prop)] >> {move 0} open declare y1 obj >> y1: obj {move 2} define infinite0 y1 : (x E V) & (y1 E V) & (y1 cneq x) & y1 Samesize x >> infinite0: [(y1_1:obj) => (((x E V) >> & ((y1_1 E V) & ((y1_1 cneq x) >> & (y1_1 Samesize x)))):prop)] >> {move 1:current} close define Infiniteset x : Exists infinite0 >> Infiniteset: [(x_1:obj) => (Exists([(y1_2: >> obj) => (((x_1 E V) & ((y1_2 E >> V) & ((y1_2 cneq x_1) & (y1_2 Samesize >> x_1)))):prop)]) >> :prop)] >> {move 0} construct I obj >> I: obj {move 0} open declare x1 obj >> x1: obj {move 2} define infinity2 x1:(Infiniteset x1) <-> x1 Samesize I >> infinity2: [(x1_1:obj) => ((Infiniteset(x1_1) >> <-> (x1_1 Samesize I)):prop)] >> {move 1:current} close construct Infinityax1 that Infiniteset I >> Infinityax1: that Infiniteset(I) {move 0} construct Infinityax2 that Forall infinity2 >> Infinityax2: that Forall([(x1_1:obj) => ((Infiniteset(x1_1) >> <-> (x1_1 Samesize I)):prop)]) >> {move 0} >> Inspector Lestrade says: Done reading scratch to pocket: >> type lines or type quit to exit interface quit