Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### A Model of ZF Set Theory Language

**by****Grzegorz Bancerek**- Received April 4, 1989
- MML identifier: ZF_LANG

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, FUNCT_1, BOOLE, RELAT_1, ARYTM_1, ZF_LANG; notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, NAT_1, NUMBERS, FINSEQ_1; constructors NAT_1, FINSEQ_1, XREAL_0, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve k,m,n for 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; definition 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 definition let x; redefine func <*x*> -> FinSequence of NAT; 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; canceled 5; theorem :: ZF_LANG:6 x '=' y = z '=' t implies x = z & y = t; theorem :: ZF_LANG:7 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; canceled 2; theorem :: ZF_LANG:10 'not' p = 'not' q implies p = q; definition let x,p; func All(x,p)-> FinSequence of NAT equals :: ZF_LANG:def 7 <*4*>^<*x*>^p; end; canceled; theorem :: ZF_LANG:12 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; definition cluster ZF-formula-like FinSequence of NAT; end; definition mode ZF-formula is ZF-formula-like FinSequence of NAT; end; canceled; theorem :: ZF_LANG:14 a is ZF-formula iff a in WFF; reserve F,F1,G,G1,H,H1 for ZF-formula; definition let x,y; cluster x '=' y -> ZF-formula-like; cluster x 'in' y -> ZF-formula-like; end; definition let H; cluster 'not' H -> ZF-formula-like; let G; cluster H '&' G -> ZF-formula-like; end; definition 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; synonym H is_equality; attr H is being_membership means :: ZF_LANG:def 11 ex x,y st H = x 'in' y; synonym H is_membership; 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; canceled; theorem :: ZF_LANG:16 (H is_equality iff ex x,y st H = x '=' y) & (H is_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_equality or H is_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; canceled 5; theorem :: ZF_LANG:22 (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:23 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:24 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:25 H is_equality or H is_membership or H is negative or H is conjunctive or H is universal; theorem :: ZF_LANG:26 H is atomic or H is negative or H is conjunctive or H is universal; theorem :: ZF_LANG:27 H is atomic implies len H = 3; theorem :: ZF_LANG:28 H is atomic or ex H1 st len H1 + 1 <= len H; theorem :: ZF_LANG:29 3 <= len H; theorem :: ZF_LANG:30 len H = 3 implies H is atomic; theorem :: ZF_LANG:31 for x,y holds (x '=' y).1 = 0 & (x 'in' y ).1 = 1; theorem :: ZF_LANG:32 for H holds ('not' H).1 = 2; theorem :: ZF_LANG:33 for F,G holds (F '&' G).1 = 3; theorem :: ZF_LANG:34 for x,H holds All(x,H).1 = 4; theorem :: ZF_LANG:35 H is_equality implies H.1 = 0; theorem :: ZF_LANG:36 H is_membership implies H.1 = 1; theorem :: ZF_LANG:37 H is negative implies H.1 = 2; theorem :: ZF_LANG:38 H is conjunctive implies H.1 = 3; theorem :: ZF_LANG:39 H is universal implies H.1 = 4; theorem :: ZF_LANG:40 H is_equality & H.1 = 0 or H is_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:41 H.1 = 0 implies H is_equality; theorem :: ZF_LANG:42 H.1 = 1 implies H is_membership; theorem :: ZF_LANG:43 H.1 = 2 implies H is negative; theorem :: ZF_LANG:44 H.1 = 3 implies H is conjunctive; theorem :: ZF_LANG:45 H.1 = 4 implies H is universal; reserve sq,sq' for FinSequence; theorem :: ZF_LANG:46 H = F^sq implies H = F; theorem :: ZF_LANG:47 H '&' G = H1 '&' G1 implies H = H1 & G = G1; theorem :: ZF_LANG:48 F 'or' G = F1 'or' G1 implies F = F1 & G = G1; theorem :: ZF_LANG:49 F => G = F1 => G1 implies F = F1 & G = G1; theorem :: ZF_LANG:50 F <=> G = F1 <=> G1 implies F = F1 & G = G1; theorem :: ZF_LANG:51 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:52 H is atomic implies Var1 H = H.2 & Var2 H = H.3; theorem :: ZF_LANG:53 H is_equality implies H = (Var1 H) '=' Var2 H; theorem :: ZF_LANG:54 H is_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; canceled; theorem :: ZF_LANG:56 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:57 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:58 H is conjunctive implies H = (the_left_argument_of H) '&' the_right_argument_of H; theorem :: ZF_LANG:59 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:60 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:61 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:62 H is universal implies H = All(bound_in H,the_scope_of H); theorem :: ZF_LANG:63 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:64 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:65 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:66 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:67 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; canceled; theorem :: ZF_LANG:69 not H is_immediate_constituent_of x '=' y; theorem :: ZF_LANG:70 not H is_immediate_constituent_of x 'in' y; theorem :: ZF_LANG:71 F is_immediate_constituent_of 'not' H iff F = H; theorem :: ZF_LANG:72 F is_immediate_constituent_of G '&' H iff F = G or F = H; theorem :: ZF_LANG:73 F is_immediate_constituent_of All(x,H) iff F = H; theorem :: ZF_LANG:74 H is atomic implies not F is_immediate_constituent_of H; theorem :: ZF_LANG:75 H is negative implies (F is_immediate_constituent_of H iff F = the_argument_of H); theorem :: ZF_LANG:76 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:77 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,L' 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; canceled; theorem :: ZF_LANG:79 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; canceled; theorem :: ZF_LANG:81 H is_immediate_constituent_of F implies len H < len F; theorem :: ZF_LANG:82 H is_immediate_constituent_of F implies H is_proper_subformula_of F; theorem :: ZF_LANG:83 H is_proper_subformula_of F implies len H < len F; theorem :: ZF_LANG:84 H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F; reserve j,j1 for Nat; theorem :: ZF_LANG:85 F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H; theorem :: ZF_LANG:86 F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H; theorem :: ZF_LANG:87 G is_subformula_of H & H is_subformula_of G implies G = H; theorem :: ZF_LANG:88 not F is_proper_subformula_of x '=' y; theorem :: ZF_LANG:89 not F is_proper_subformula_of x 'in' y; theorem :: ZF_LANG:90 F is_proper_subformula_of 'not' H implies F is_subformula_of H; theorem :: ZF_LANG:91 F is_proper_subformula_of G '&' H implies F is_subformula_of G or F is_subformula_of H; theorem :: ZF_LANG:92 F is_proper_subformula_of All(x,H) implies F is_subformula_of H; theorem :: ZF_LANG:93 H is atomic implies not F is_proper_subformula_of H; theorem :: ZF_LANG:94 H is negative implies the_argument_of H is_proper_subformula_of H; theorem :: ZF_LANG:95 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:96 H is universal implies the_scope_of H is_proper_subformula_of H; theorem :: ZF_LANG:97 H is_subformula_of x '=' y iff H = x '=' y; theorem :: ZF_LANG:98 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; canceled; theorem :: ZF_LANG:100 G in Subformulae H implies G is_subformula_of H; theorem :: ZF_LANG:101 F is_subformula_of H implies Subformulae F c= Subformulae H; theorem :: ZF_LANG:102 Subformulae x '=' y = { x '=' y }; theorem :: ZF_LANG:103 Subformulae x 'in' y = { x 'in' y }; theorem :: ZF_LANG:104 Subformulae 'not' H = Subformulae H \/ { 'not' H }; theorem :: ZF_LANG:105 Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }; theorem :: ZF_LANG:106 Subformulae All(x,H) = Subformulae H \/ { All(x,H) }; theorem :: ZF_LANG:107 H is atomic iff Subformulae H = { H }; theorem :: ZF_LANG:108 H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }; theorem :: ZF_LANG:109 H is conjunctive implies Subformulae H = Subformulae the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }; theorem :: ZF_LANG:110 H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }; theorem :: ZF_LANG:111 (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_Ind { 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_CompInd { 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];

Back to top