:: A Model of ZF Set Theory Language
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2016 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];