>> Inspector Lestrade says: >> Welcome to the Lestrade Type Inspector, >> full version of 8/12/2016 (pretty printing upgrade) >> 11 am Boise time % development of MacLane set theory. % may be extended to Zermelo, ZFC, Kelley-Morse. % start with logic. declare p prop >> p: prop {world 1} declare q prop >> q: prop {world 1} construct & p q : prop >> &: [(p_1:prop),(q_1:prop) => (---:prop)] >> {world 0} construct ?? : prop >> ??: prop {world 0} declare pp that p >> pp: that p {world 1} declare qq that q >> qq: that q {world 1} declare pq that p & q >> pq: that (p & q) {world 1} construct Andi pp qq : that p & q >> Andi: [(.p_1:prop),(pp_1:that .p_1),(.q_1:prop),(qq_1: >> that .q_1) => (---:that (.p_1 & .q_1))] >> {world 0} construct Ande1 pq : that p >> Ande1: [(.p_1:prop),(.q_1:prop),(pq_1:that (.p_1 & >> .q_1)) => (---:that .p_1)] >> {world 0} construct Ande2 pq : that q >> Ande2: [(.p_1:prop),(.q_1:prop),(pq_1:that (.p_1 & >> .q_1)) => (---:that .q_1)] >> {world 0} construct ~ p :prop >> ~: [(p_1:prop) => (---:prop)] >> {world 0} open declare pp2 that p >> pp2: that p {world 2} construct neg pp2 that ?? >> neg: [(pp2_1:that p) => (---:that ??)] >> {world 1} close construct Negproof neg : that ~ p >> Negproof: [(.p_1:prop),(neg_1:[(pp2_2:that .p_1) => >> (---:that ??)]) >> => (---:that ~(.p_1))] >> {world 0} declare np that ~ p >> np: that ~(p) {world 1} construct Contra pp np : that ?? >> Contra: [(.p_1:prop),(pp_1:that .p_1),(np_1:that ~(.p_1)) >> => (---:that ??)] >> {world 0} declare maybe that ~ ~ p >> maybe: that ~(~(p)) {world 1} construct Dneg maybe : that p >> Dneg: [(.p_1:prop),(maybe_1:that ~(~(.p_1))) => (---: >> that .p_1)] >> {world 0} construct Dnegfull p maybe : that p >> Dnegfull: [(p_1:prop),(maybe_1:that ~(~(p_1))) => (---: >> that p_1)] >> {world 0} %% To demonstrate that I have enough %% logical primitives I demonstrate the % basic properties of implication. define -> p q : ~ (p & ~q) >> ->: [(p_1:prop),(q_1:prop) => (~((p_1 & ~(q_1))):prop)] >> {world 0} open declare pp2 that p >> pp2: that p {world 2} construct Ded pp2 that q >> Ded: [(pp2_1:that p) => (---:that q)] >> {world 1} close open declare hyp that p & ~ q >> hyp: that (p & ~(q)) {world 2} define weird hyp : Contra (Ded (Ande1 hyp),Ande2 hyp) >> weird: [(hyp_1:that (p & ~(q))) => (Contra(q,Ded(Ande1(p, >> ~(q),hyp_1)),Ande2(p,~(q),hyp_1)):that ??)] >> {world 1} close define Impi1 Ded: Negproof weird >> Impi1: [(.p_1:prop),(.q_1:prop),(Ded_1:[(pp2_2:that >> .p_1) => (---:that .q_1)]) >> => (((.p_1 & ~(.q_1)) Negproof [(hyp_3:that (.p_1 >> & ~(.q_1))) => (Contra(.q_1,Ded_1(Ande1(.p_1, >> ~(.q_1),hyp_3)),Ande2(.p_1,~(.q_1),hyp_3)): >> that ??)]) >> :that ~((.p_1 & ~(.q_1))))] >> {world 0} open declare pp2 that p >> pp2: that p {world 2} open declare nn2 that ~ p >> nn2: that ~(p) {world 3} define dneg nn2 : Contra pp2 nn2 >> dneg: [(nn2_1:that ~(p)) => (Contra(p,pp2, >> nn2_1):that ??)] >> {world 2} close define dneg2 pp2 : Negproof dneg >> dneg2: [(pp2_1:that p) => ((~(p) Negproof [(nn2_2: >> that ~(p)) => (Contra(p,pp2_1,nn2_2): >> that ??)]) >> :that ~(~(p)))] >> {world 1} close define Dneg2 pp: dneg2 pp >> Dneg2: [(.p_1:prop),(pp_1:that .p_1) => ((~(.p_1) Negproof >> [(nn2_2:that ~(.p_1)) => (Contra(.p_1,pp_1,nn2_2): >> that ??)]) >> :that ~(~(.p_1)))] >> {world 0} define Impi Ded: Dnegfull (p -> q, Dneg2 (Impi1 Ded)) >> Impi: [(.p_1:prop),(.q_1:prop),(Ded_1:[(pp2_2:that >> .p_1) => (---:that .q_1)]) >> => (((.p_1 -> .q_1) Dnegfull (~((.p_1 & ~(.q_1))) >> Dneg2 Impi1(.p_1,.q_1,Ded_1))):that (.p_1 -> .q_1))] >> {world 0} declare piq that p -> q >> piq: that (p -> q) {world 1} open declare nq that ~ q >> nq: that ~(q) {world 2} define mp nq : Contra (Andi (pp, nq),piq) >> mp: [(nq_1:that ~(q)) => (Contra((p & ~(q)),Andi(p, >> pp,~(q),nq_1),piq):that ??)] >> {world 1} close define Mp pp piq : Dneg (Negproof mp) >> Mp: [(.p_1:prop),(pp_1:that .p_1),(.q_1:prop),(piq_1: >> that (.p_1 -> .q_1)) => ((.q_1 Dneg (~(.q_1) Negproof >> [(nq_2:that ~(.q_1)) => (Contra((.p_1 & ~(.q_1)), >> Andi(.p_1,pp_1,~(.q_1),nq_2),piq_1):that >> ??)])) >> :that .q_1)] >> {world 0} define v p q : ~ p -> q >> v: [(p_1:prop),(q_1:prop) => ((~(p_1) -> q_1):prop)] >> {world 0} define <-> p q : (p -> q) & (q -> p) >> <->: [(p_1:prop),(q_1:prop) => (((p_1 -> q_1) & (q_1 >> -> p_1)):prop)] >> {world 0} % equality declare x obj >> x: obj {world 1} declare y obj >> y: obj {world 1} construct = x y : prop >> =: [(x_1:obj),(y_1:obj) => (---:prop)] >> {world 0} construct Refl x : that x = x >> Refl: [(x_1:obj) => (---:that (x_1 = x_1))] >> {world 0} open declare x2 obj >> x2: obj {world 2} construct P x2 : prop >> P: [(x2_1:obj) => (---:prop)] >> {world 1} close declare Px that P x >> Px: that P(x) {world 1} declare eq that x = y >> eq: that (x = y) {world 1} construct Subs P, Px eq : that P y >> Subs: [(P_1:[(x2_2:obj) => (---:prop)]), >> (.x_1:obj),(Px_1:that P_1(.x_1)),(.y_1:obj),(eq_1: >> that (.x_1 = .y_1)) => (---:that P_1(.y_1))] >> {world 0} %% Our approach to implementing MacLane's restrictions %% on comprehension is to restrict the formation of %% quantified propositions % so that no bad sets can be defined. construct E x y : prop >> E: [(x_1:obj),(y_1:obj) => (---:prop)] >> {world 0} open declare x1 obj >> x1: obj {world 2} declare evs1 that x1 E x >> evs1: that (x1 E x) {world 2} construct Q x1 evs1 prop >> Q: [(x1_1:obj),(evs1_1:that (x1_1 E x)) => (---: >> prop)] >> {world 1} close construct Setof x Q : obj >> Setof: [(x_1:obj),(Q_1:[(x1_2:obj),(evs1_2:that (x1_2 >> E x_1)) => (---:prop)]) >> => (---:obj)] >> {world 0} open declare x1 obj >> x1: obj {world 2} declare evs1 that x1 E y >> evs1: that (x1 E y) {world 2} construct Qy x1 evs1 prop >> Qy: [(x1_1:obj),(evs1_1:that (x1_1 E y)) => (---: >> prop)] >> {world 1} close declare ev1 that x E y >> ev1: that (x E y) {world 1} declare ev2 that x E Setof y Qy >> ev2: that (x E (y Setof Qy)) {world 1} construct comp1 ev1 ev2 : that Qy x ev1 >> comp1: [(.x_1:obj),(.y_1:obj),(ev1_1:that (.x_1 E .y_1)), >> (.Qy_1:[(x1_2:obj),(evs1_2:that (x1_2 E .y_1)) >> => (---:prop)]), >> (ev2_1:that (.x_1 E (.y_1 Setof .Qy_1))) => (---: >> that (.x_1 .Qy_1 ev1_1))] >> {world 0} declare ev3 that x E y >> ev3: that (x E y) {world 1} declare ev4 that Qy x ev3 >> ev4: that (x Qy ev3) {world 1} construct comp2 ev3 ev4 : that x E (Setof y Qy) >> comp2: [(.x_1:obj),(.y_1:obj),(ev3_1:that (.x_1 E .y_1)), >> (.Qy_1:[(x1_2:obj),(evs1_2:that (x1_2 E .y_1)) >> => (---:prop)]), >> (ev4_1:that (.x_1 .Qy_1 ev3_1)) => (---:that (.x_1 >> E (.y_1 Setof .Qy_1)))] >> {world 0} construct C x y : prop >> C: [(x_1:obj),(y_1:obj) => (---:prop)] >> {world 0} open declare z obj >> z: obj {world 2} declare ev5 that z E x >> ev5: that (z E x) {world 2} construct subset ev5 that z E y >> subset: [(.z_1:obj),(ev5_1:that (.z_1 E x)) => >> (---:that (.z_1 E y))] >> {world 1} close construct Subset subset : that x C y >> Subset: [(.x_1:obj),(.y_1:obj),(subset_1:[(.z_2:obj), >> (ev5_2:that (.z_2 E .x_1)) => (---:that (.z_2 >> E .y_1))]) >> => (---:that (.x_1 C .y_1))] >> {world 0} declare ev6 that x C y >> ev6: that (x C y) {world 1} declare ev7 that y C x >> ev7: that (y C x) {world 1} construct Ext ev6 ev7 that x = y >> Ext: [(.x_1:obj),(.y_1:obj),(ev6_1:that (.x_1 C .y_1)), >> (ev7_1:that (.y_1 C .x_1)) => (---:that (.x_1 >> = .y_1))] >> {world 0} declare z obj >> z: obj {world 1} declare evs1 that x E y >> evs1: that (x E y) {world 1} declare evs2 that y C z >> evs2: that (y C z) {world 1} construct Incl evs1 evs2 that x E z >> Incl: [(.x_1:obj),(.y_1:obj),(evs1_1:that (.x_1 E .y_1)), >> (.z_1:obj),(evs2_1:that (.y_1 C .z_1)) => (---: >> that (.x_1 E .z_1))] >> {world 0} % definition of the bounded universal quantifier define Forall x Q : x C Setof x Q >> Forall: [(x_1:obj),(Q_1:[(x1_2:obj),(evs1_2:that (x1_2 >> E x_1)) => (---:prop)]) >> => ((x_1 C (x_1 Setof Q_1)):prop)] >> {world 0} declare univev1 that y E x >> univev1: that (y E x) {world 1} declare univev2 that Forall x Q >> univev2: that (x Forall Q) {world 1} define Ui univev1 univev2 : comp1 univev1 (Incl univev1 univev2) >> Ui: [(.y_1:obj),(.x_1:obj),(univev1_1:that (.y_1 E >> .x_1)),(.Q_1:[(x1_2:obj),(evs1_2:that (x1_2 E >> .x_1)) => (---:prop)]), >> (univev2_1:that (.x_1 Forall .Q_1)) => (comp1(.y_1, >> .x_1,univev1_1,.Q_1,Incl(.y_1,.x_1,univev1_1,(.x_1 >> Setof .Q_1),univev2_1)):that (.y_1 .Q_1 univev1_1))] >> {world 0} % develop a universal generalization rule % given a function which takes a proof that x E y % to a proof of P y construct a proof of Forall y P open declare x1 obj >> x1: obj {world 2} declare evi that x1 E y >> evi: that (x1 E y) {world 2} construct univevi x1 evi that Qy x1 evi >> univevi: [(x1_1:obj),(evi_1:that (x1_1 E y)) => >> (---:that (x1_1 Qy evi_1))] >> {world 1} define testa evi: univevi x1 evi >> testa: [(.x1_1:obj),(evi_1:that (.x1_1 E y)) => >> ((.x1_1 univevi evi_1):that (.x1_1 Qy evi_1))] >> {world 1} define test1 evi : comp2 evi (univevi x1 evi) >> test1: [(.x1_1:obj),(evi_1:that (.x1_1 E y)) => >> (comp2(.x1_1,y,evi_1,Qy,(.x1_1 univevi evi_1)): >> that (.x1_1 E (y Setof Qy)))] >> {world 1} close construct Pow x : obj >> Pow: [(x_1:obj) => (---:obj)] >> {world 0} declare eva8 that x C y >> eva8: that (x C y) {world 1} construct Pow1 eva8 that x E Pow y >> Pow1: [(.x_1:obj),(.y_1:obj),(eva8_1:that (.x_1 C .y_1)) >> => (---:that (.x_1 E Pow(.y_1)))] >> {world 0} declare ev8 that x E Pow y >> ev8: that (x E Pow(y)) {world 1} construct Pow2 ev8 that x C y >> Pow2: [(.x_1:obj),(.y_1:obj),(ev8_1:that (.x_1 E Pow(.y_1))) >> => (---:that (.x_1 C .y_1))] >> {world 0} %% get the rest of the axioms by defining % ranks construct Rank x : prop >> Rank: [(x_1:obj) => (---:prop)] >> {world 0} construct rankof x: obj >> rankof: [(x_1:obj) => (---:obj)] >> {world 0} construct isrank x : that Rank (rankof x) >> isrank: [(x_1:obj) => (---:that Rank(rankof(x_1)))] >> {world 0} construct inrank x : that x E rankof x >> inrank: [(x_1:obj) => (---:that (x_1 E rankof(x_1)))] >> {world 0} declare ev9 that Rank x >> ev9: that Rank(x) {world 1} construct nextrank ev9 : that Rank (Pow x) >> nextrank: [(.x_1:obj),(ev9_1:that Rank(.x_1)) => (---: >> that Rank(Pow(.x_1)))] >> {world 0} declare ev10 that Rank y >> ev10: that Rank(y) {world 1} declare ev11 that ~ (y C x) >> ev11: that ~((y C x)) {world 1} construct maxrank x y : obj >> maxrank: [(x_1:obj),(y_1:obj) => (---:obj)] >> {world 0} construct rankorder ev9 ev10 ev11 that x C y >> rankorder: [(.x_1:obj),(ev9_1:that Rank(.x_1)),(.y_1: >> obj),(ev10_1:that Rank(.y_1)),(ev11_1:that ~((.y_1 >> C .x_1))) => (---:that (.x_1 C .y_1))] >> {world 0} construct rankorder2 ev9 ev10 ev11 that y = maxrank x y >> rankorder2: [(.x_1:obj),(ev9_1:that Rank(.x_1)),(.y_1: >> obj),(ev10_1:that Rank(.y_1)),(ev11_1:that ~((.y_1 >> C .x_1))) => (---:that (.y_1 = (.x_1 maxrank .y_1)))] >> {world 0} construct limit obj >> limit: obj {world 0} construct limitisrank that Rank limit >> limitisrank: that Rank(limit) {world 0} construct limitelt obj >> limitelt: obj {world 0} construct limithaselt that limitelt E limit >> limithaselt: that (limitelt E limit) {world 0} declare ev12 that x E limit >> ev12: that (x E limit) {world 1} construct limitislimit ev12 that Pow (rankof x) C limit >> limitislimit: [(.x_1:obj),(ev12_1:that (.x_1 E limit)) >> => (---:that (Pow(rankof(.x_1)) C limit))] >> {world 0} >> Inspector Lestrade says: Done reading scratch to maclanetest: >> type lines or type quit to exit interface quit