:: A Model of ZF Set Theory Language :: by Grzegorz Bancerek :: :: Received April 4, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, ARYTM_3, CARD_1, ORDINAL4, FUNCT_1, XBOOLEAN, BVFUNC_2, RELAT_1, CLASSES2, NAT_1, ARYTM_1, ZF_LANG, ORDINAL1; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, NUMBERS, FINSEQ_1, XXREAL_0, TREES_3; constructors XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, NUMBERS, TREES_3; registrations ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, CARD_1, XBOOLE_0, NAT_1, MEMBERED; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve k,m,n for Element of NAT, a,X,Y for set, D,D1,D2 for non empty set; reserve p,q for FinSequence of NAT; :: :: The Construction of ZF Set Theory Language :: :: The set and the mode of ZF-language variables definition func VAR -> Subset of NAT equals :: ZF_LANG:def 1 { k : 5 <= k }; end; registration cluster VAR -> non empty; end; definition mode Variable is Element of VAR; end; definition let n; func x.n -> Variable equals :: ZF_LANG:def 2 5 + n; end; reserve x,y,z,t for Variable; :: The operations to make ZF-formulae registration cluster -> natural for Variable; end; definition let x,y; func x '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3 <*0*>^<*x*>^<*y*>; func x 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4 <*1*>^<*x*>^<*y*>; end; theorem :: ZF_LANG:1 x '=' y = z '=' t implies x = z & y = t; theorem :: ZF_LANG:2 x 'in' y = z 'in' t implies x = z & y = t; definition let p; func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5 <*2*>^p; let q; func p '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6 <*3*>^p^q; end; definition let x,p; func All(x,p)-> FinSequence of NAT equals :: ZF_LANG:def 7 <*4*>^<*x*>^p; end; theorem :: ZF_LANG:3 All(x,p) = All(y,q) implies x = y & p = q; :: The set of all well formed formulae of ZF-language definition func WFF -> non empty set means :: ZF_LANG:def 8 (for a st a in it holds a is FinSequence of NAT ) & (for x,y holds x '=' y in it & x 'in' y in it ) & (for p st p in it holds 'not' p in it ) & (for p,q st p in it & q in it holds p '&' q in it ) & (for x,p st p in it holds All(x,p) in it ) & for D st (for a st a in D holds a is FinSequence of NAT ) & (for x,y holds x '=' y in D & x 'in' y in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for x,p st p in D holds All(x,p) in D ) holds it c= D; end; definition let IT be FinSequence of NAT; attr IT is ZF-formula-like means :: ZF_LANG:def 9 IT is Element of WFF; end; registration cluster ZF-formula-like for FinSequence of NAT; end; definition mode ZF-formula is ZF-formula-like FinSequence of NAT; end; theorem :: ZF_LANG:4 a is ZF-formula iff a in WFF; reserve F,F1,G,G1,H,H1 for ZF-formula; registration let x,y; cluster x '=' y -> ZF-formula-like; cluster x 'in' y -> ZF-formula-like; end; registration let H; cluster 'not' H -> ZF-formula-like; let G; cluster H '&' G -> ZF-formula-like; end; registration let x,H; cluster All(x,H) -> ZF-formula-like; end; :: :: The Properties of ZF-formulae :: definition let H; attr H is being_equality means :: ZF_LANG:def 10 ex x,y st H = x '=' y; attr H is being_membership means :: ZF_LANG:def 11 ex x,y st H = x 'in' y; attr H is negative means :: ZF_LANG:def 12 ex H1 st H = 'not' H1; attr H is conjunctive means :: ZF_LANG:def 13 ex F,G st H = F '&' G; attr H is universal means :: ZF_LANG:def 14 ex x,H1 st H = All(x,H1); end; theorem :: ZF_LANG:5 (H is being_equality iff ex x,y st H = x '=' y) & (H is being_membership iff ex x,y st H = x 'in' y) & (H is negative iff ex H1 st H = 'not' H1) & (H is conjunctive iff ex F,G st H = F '&' G) & (H is universal iff ex x,H1 st H = All(x,H1) ); definition let H; attr H is atomic means :: ZF_LANG:def 15 H is being_equality or H is being_membership; end; definition let F,G; func F 'or' G -> ZF-formula equals :: ZF_LANG:def 16 'not'('not' F '&' 'not' G); func F => G -> ZF-formula equals :: ZF_LANG:def 17 'not' (F '&' 'not' G); end; definition let F,G; func F <=> G -> ZF-formula equals :: ZF_LANG:def 18 (F => G) '&' (G => F); end; definition let x,H; func Ex(x,H) -> ZF-formula equals :: ZF_LANG:def 19 'not' All(x,'not' H); end; definition let H; attr H is disjunctive means :: ZF_LANG:def 20 ex F,G st H = F 'or' G; attr H is conditional means :: ZF_LANG:def 21 ex F,G st H = F => G; attr H is biconditional means :: ZF_LANG:def 22 ex F,G st H = F <=> G; attr H is existential means :: ZF_LANG:def 23 ex x,H1 st H = Ex(x,H1); end; theorem :: ZF_LANG:6 (H is disjunctive iff ex F,G st H = F 'or' G) & (H is conditional iff ex F,G st H = F => G) & (H is biconditional iff ex F,G st H = F <=> G) & (H is existential iff ex x,H1 st H = Ex(x,H1) ); definition let x,y,H; func All(x,y,H) -> ZF-formula equals :: ZF_LANG:def 24 All(x,All(y,H)); func Ex(x,y,H) -> ZF-formula equals :: ZF_LANG:def 25 Ex(x,Ex(y,H)); end; theorem :: ZF_LANG:7 All(x,y,H) = All(x,All(y,H)) & Ex(x,y,H) = Ex(x,Ex(y,H)); definition let x,y,z,H; func All(x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 26 All(x,All(y,z,H)); func Ex(x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27 Ex(x,Ex(y,z,H)); end; theorem :: ZF_LANG:8 All(x,y,z,H) = All(x,All(y,z,H)) & Ex(x,y,z,H) = Ex(x,Ex(y,z,H)); theorem :: ZF_LANG:9 H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal; theorem :: ZF_LANG:10 H is atomic or H is negative or H is conjunctive or H is universal; theorem :: ZF_LANG:11 H is atomic implies len H = 3; theorem :: ZF_LANG:12 H is atomic or ex H1 st len H1 + 1 <= len H; theorem :: ZF_LANG:13 3 <= len H; theorem :: ZF_LANG:14 len H = 3 implies H is atomic; theorem :: ZF_LANG:15 for x,y holds (x '=' y).1 = 0 & (x 'in' y ).1 = 1; theorem :: ZF_LANG:16 for F,G holds (F '&' G).1 = 3; theorem :: ZF_LANG:17 for x,H holds All(x,H).1 = 4; theorem :: ZF_LANG:18 H is being_equality implies H.1 = 0; theorem :: ZF_LANG:19 H is being_membership implies H.1 = 1; theorem :: ZF_LANG:20 H is negative implies H.1 = 2; theorem :: ZF_LANG:21 H is conjunctive implies H.1 = 3; theorem :: ZF_LANG:22 H is universal implies H.1 = 4; theorem :: ZF_LANG:23 H is being_equality & H.1 = 0 or H is being_membership & H.1 = 1 or H is negative & H.1 = 2 or H is conjunctive & H.1 = 3 or H is universal & H. 1 = 4; theorem :: ZF_LANG:24 H.1 = 0 implies H is being_equality; theorem :: ZF_LANG:25 H.1 = 1 implies H is being_membership; theorem :: ZF_LANG:26 H.1 = 2 implies H is negative; theorem :: ZF_LANG:27 H.1 = 3 implies H is conjunctive; theorem :: ZF_LANG:28 H.1 = 4 implies H is universal; reserve sq,sq9 for FinSequence; theorem :: ZF_LANG:29 H = F^sq implies H = F; theorem :: ZF_LANG:30 H '&' G = H1 '&' G1 implies H = H1 & G = G1; theorem :: ZF_LANG:31 F 'or' G = F1 'or' G1 implies F = F1 & G = G1; theorem :: ZF_LANG:32 F => G = F1 => G1 implies F = F1 & G = G1; theorem :: ZF_LANG:33 F <=> G = F1 <=> G1 implies F = F1 & G = G1; theorem :: ZF_LANG:34 Ex(x,H) = Ex(y,G) implies x = y & H = G; :: :: The Select Function of ZF-fomrulae :: definition let H; assume H is atomic; func Var1 H -> Variable equals :: ZF_LANG:def 28 H.2; func Var2 H -> Variable equals :: ZF_LANG:def 29 H.3; end; theorem :: ZF_LANG:35 H is atomic implies Var1 H = H.2 & Var2 H = H.3; theorem :: ZF_LANG:36 H is being_equality implies H = (Var1 H) '=' Var2 H; theorem :: ZF_LANG:37 H is being_membership implies H = (Var1 H) 'in' Var2 H; definition let H; assume H is negative; func the_argument_of H -> ZF-formula means :: ZF_LANG:def 30 'not' it = H; end; definition let H; assume H is conjunctive or H is disjunctive; func the_left_argument_of H -> ZF-formula means :: ZF_LANG:def 31 ex H1 st it '&' H1 = H if H is conjunctive otherwise ex H1 st it 'or' H1 = H; func the_right_argument_of H -> ZF-formula means :: ZF_LANG:def 32 ex H1 st H1 '&' it = H if H is conjunctive otherwise ex H1 st H1 'or' it = H; end; theorem :: ZF_LANG:38 H is conjunctive implies (F = the_left_argument_of H iff ex G st F '&' G = H) & (F = the_right_argument_of H iff ex G st G '&' F = H); theorem :: ZF_LANG:39 H is disjunctive implies (F = the_left_argument_of H iff ex G st F 'or' G = H) & (F = the_right_argument_of H iff ex G st G 'or' F = H); theorem :: ZF_LANG:40 H is conjunctive implies H = (the_left_argument_of H) '&' the_right_argument_of H; theorem :: ZF_LANG:41 H is disjunctive implies H = (the_left_argument_of H) 'or' the_right_argument_of H; definition let H; assume H is universal or H is existential; func bound_in H -> Variable means :: ZF_LANG:def 33 ex H1 st All(it,H1) = H if H is universal otherwise ex H1 st Ex(it,H1) = H; func the_scope_of H -> ZF-formula means :: ZF_LANG:def 34 ex x st All(x,it) = H if H is universal otherwise ex x st Ex(x,it) = H; end; theorem :: ZF_LANG:42 H is universal implies (x = bound_in H iff ex H1 st All(x,H1) = H) & ( H1 = the_scope_of H iff ex x st All(x,H1) = H); theorem :: ZF_LANG:43 H is existential implies (x = bound_in H iff ex H1 st Ex(x,H1) = H) & (H1 = the_scope_of H iff ex x st Ex(x,H1) = H); theorem :: ZF_LANG:44 H is universal implies H = All(bound_in H,the_scope_of H); theorem :: ZF_LANG:45 H is existential implies H = Ex(bound_in H,the_scope_of H); definition let H; assume H is conditional; func the_antecedent_of H -> ZF-formula means :: ZF_LANG:def 35 ex H1 st H = it => H1; func the_consequent_of H -> ZF-formula means :: ZF_LANG:def 36 ex H1 st H = H1 => it; end; theorem :: ZF_LANG:46 H is conditional implies (F = the_antecedent_of H iff ex G st H = F => G) & (F = the_consequent_of H iff ex G st H = G => F); theorem :: ZF_LANG:47 H is conditional implies H = (the_antecedent_of H) => the_consequent_of H; definition let H; assume H is biconditional; func the_left_side_of H -> ZF-formula means :: ZF_LANG:def 37 ex H1 st H = it <=> H1; func the_right_side_of H -> ZF-formula means :: ZF_LANG:def 38 ex H1 st H = H1 <=> it; end; theorem :: ZF_LANG:48 H is biconditional implies (F = the_left_side_of H iff ex G st H = F <=> G) & (F = the_right_side_of H iff ex G st H = G <=> F); theorem :: ZF_LANG:49 H is biconditional implies H = (the_left_side_of H) <=> the_right_side_of H; :: :: The Immediate Constituents of ZF-formulae :: definition let H,F; pred H is_immediate_constituent_of F means :: ZF_LANG:def 39 F = 'not' H or ( ex H1 st F = H '&' H1 or F = H1 '&' H ) or ex x st F = All(x,H); end; theorem :: ZF_LANG:50 not H is_immediate_constituent_of x '=' y; theorem :: ZF_LANG:51 not H is_immediate_constituent_of x 'in' y; theorem :: ZF_LANG:52 F is_immediate_constituent_of 'not' H iff F = H; theorem :: ZF_LANG:53 F is_immediate_constituent_of G '&' H iff F = G or F = H; theorem :: ZF_LANG:54 F is_immediate_constituent_of All(x,H) iff F = H; theorem :: ZF_LANG:55 H is atomic implies not F is_immediate_constituent_of H; theorem :: ZF_LANG:56 H is negative implies (F is_immediate_constituent_of H iff F = the_argument_of H); theorem :: ZF_LANG:57 H is conjunctive implies (F is_immediate_constituent_of H iff F = the_left_argument_of H or F = the_right_argument_of H); theorem :: ZF_LANG:58 H is universal implies (F is_immediate_constituent_of H iff F = the_scope_of H); :: :: The Subformulae and The Proper Subformulae of ZF-formulae :: reserve L,L9 for FinSequence; definition let H,F; pred H is_subformula_of F means :: ZF_LANG:def 40 ex n,L st 1 <= n & len L = n & L.1 = H & L.n = F & for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1 is_immediate_constituent_of F1; end; theorem :: ZF_LANG:59 H is_subformula_of H; definition let H,F; pred H is_proper_subformula_of F means :: ZF_LANG:def 41 H is_subformula_of F & H <> F; end; theorem :: ZF_LANG:60 H is_immediate_constituent_of F implies len H < len F; theorem :: ZF_LANG:61 H is_immediate_constituent_of F implies H is_proper_subformula_of F; theorem :: ZF_LANG:62 H is_proper_subformula_of F implies len H < len F; theorem :: ZF_LANG:63 H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F; reserve j,j1 for Element of NAT; theorem :: ZF_LANG:64 F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H; theorem :: ZF_LANG:65 F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H; theorem :: ZF_LANG:66 G is_subformula_of H & H is_subformula_of G implies G = H; theorem :: ZF_LANG:67 not F is_proper_subformula_of x '=' y; theorem :: ZF_LANG:68 not F is_proper_subformula_of x 'in' y; theorem :: ZF_LANG:69 F is_proper_subformula_of 'not' H implies F is_subformula_of H; theorem :: ZF_LANG:70 F is_proper_subformula_of G '&' H implies F is_subformula_of G or F is_subformula_of H; theorem :: ZF_LANG:71 F is_proper_subformula_of All(x,H) implies F is_subformula_of H; theorem :: ZF_LANG:72 H is atomic implies not F is_proper_subformula_of H; theorem :: ZF_LANG:73 H is negative implies the_argument_of H is_proper_subformula_of H; theorem :: ZF_LANG:74 H is conjunctive implies the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ; theorem :: ZF_LANG:75 H is universal implies the_scope_of H is_proper_subformula_of H; theorem :: ZF_LANG:76 H is_subformula_of x '=' y iff H = x '=' y; theorem :: ZF_LANG:77 H is_subformula_of x 'in' y iff H = x 'in' y; :: :: The Set of Subformulae of ZF-formulae :: definition let H; func Subformulae H -> set means :: ZF_LANG:def 42 a in it iff ex F st F = a & F is_subformula_of H; end; theorem :: ZF_LANG:78 G in Subformulae H implies G is_subformula_of H; theorem :: ZF_LANG:79 F is_subformula_of H implies Subformulae F c= Subformulae H; theorem :: ZF_LANG:80 Subformulae x '=' y = { x '=' y }; theorem :: ZF_LANG:81 Subformulae x 'in' y = { x 'in' y }; theorem :: ZF_LANG:82 Subformulae 'not' H = Subformulae H \/ { 'not' H }; theorem :: ZF_LANG:83 Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }; theorem :: ZF_LANG:84 Subformulae All(x,H) = Subformulae H \/ { All(x,H) }; theorem :: ZF_LANG:85 H is atomic iff Subformulae H = { H }; theorem :: ZF_LANG:86 H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }; theorem :: ZF_LANG:87 H is conjunctive implies Subformulae H = Subformulae the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }; theorem :: ZF_LANG:88 H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }; theorem :: ZF_LANG:89 (H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G) & G in Subformulae F implies H in Subformulae F; :: :: The Structural Induction Schemes :: scheme :: ZF_LANG:sch 1 ZFInd { P[ZF-formula] } : for H holds P[H] provided for H st H is atomic holds P[H] and for H st H is negative & P[the_argument_of H] holds P[H] and for H st H is conjunctive & P[the_left_argument_of H] & P[ the_right_argument_of H] holds P[H] and for H st H is universal & P[the_scope_of H] holds P[H]; scheme :: ZF_LANG:sch 2 ZFCompInd { P[ZF-formula] } : for H holds P[H] provided for H st for F st F is_proper_subformula_of H holds P[F] holds P[H];