Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions

by
Shunichi Kobayashi, and
Yatsuka Nakamura

MML identifier: BVFUNC_2
[ Mizar article, MML identifier index ]

```environ

vocabulary PARTIT1, T_1TOPSP, EQREL_1, FUNCT_1, SETFAM_1, RELAT_1, CANTOR_1,
BOOLE, PARTFUN1, FINSEQ_4, TARSKI, SUBSET_1, GROUP_4, FUNCT_2, MARGREL1,
BVFUNC_1, ZF_LANG, BINARITH, BVFUNC_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1,
FUNCT_1, SETFAM_1, FRAENKEL, RELSET_1, PARTFUN1, FINSEQ_4, EQREL_1,
CANTOR_1, T_1TOPSP, BINARITH, PARTIT1, BVFUNC_1;
constructors FINSEQ_4, BINARITH, CANTOR_1, PARTIT1, BVFUNC_1, PUA2MSS1;
clusters RELSET_1, PARTIT1, T_1TOPSP, SUBSET_1, MARGREL1, VALUAT_1, BINARITH,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Chap. 1  Preliminaries

reserve Y for non empty set,
G for Subset of PARTITIONS(Y);

definition let X be set;
redefine func PARTITIONS X -> Part-Family of X;
end;

definition let X be set; let F be non empty Part-Family of X;
redefine mode Element of F -> a_partition of X;
end;

theorem :: BVFUNC_2:1
for y being Element of Y
ex X being Subset of Y st y in X &
ex h being Function, F being Subset-Family of Y st
dom h=G & rng h = F &
(for d being set st d in G holds h.d in d) &
X=Intersect F & X<>{};

definition let Y;let G be Subset of PARTITIONS(Y);
func '/\' G -> a_partition of Y means
:: BVFUNC_2:def 1
for x being set holds
x in it iff ex h being Function, F being Subset-Family of Y st
dom h=G & rng h = F &
(for d being set st d in G holds h.d in d) &
x=Intersect F & x<>{};
end;

definition let Y;let G be Subset of PARTITIONS(Y),b be set;
pred b is_upper_min_depend_of G means
:: BVFUNC_2:def 2
(for d being a_partition of Y st d in G holds
b is_a_dependent_set_of d) &
(for e being set st (e c= b &
(for d being a_partition of Y st d in G holds e is_a_dependent_set_of d))
holds e=b);
end;

theorem :: BVFUNC_2:2
for y being Element of Y st G<>{} holds
(ex X being Subset of Y st y in X &
X is_upper_min_depend_of G);

definition let Y;let G be Subset of PARTITIONS(Y);
func '\/' G -> a_partition of Y means
:: BVFUNC_2:def 3
(for x being set holds x in it iff x is_upper_min_depend_of G) if G<>{}
otherwise it = %I(Y);
end;

theorem :: BVFUNC_2:3
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st
PA in G holds PA '>' ('/\' G);

theorem :: BVFUNC_2:4
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st
PA in G holds PA '<' ('\/' G);

begin :: Chap. 2  Coordinate and Quantifiers

definition let Y;let G be Subset of PARTITIONS(Y);
attr G is generating means
:: BVFUNC_2:def 4
('/\' G) = %I(Y);
end;

definition let Y;let G be Subset of PARTITIONS(Y);
attr G is independent means
:: BVFUNC_2:def 5
for h being Function, F being Subset-Family of Y st
dom h=G & rng h=F &
(for d being set st d in G holds h.d in d)
holds (Intersect F)<>{};
end;

definition let Y;let G be Subset of PARTITIONS(Y);
pred G is_a_coordinate means
:: BVFUNC_2:def 6
G is independent generating;
end;

definition let Y;let PA be a_partition of Y;
redefine func {PA} -> Subset of PARTITIONS(Y);
end;

definition let Y;let PA be a_partition of Y;let G be Subset of PARTITIONS(Y);
func CompF(PA,G) -> a_partition of Y equals
:: BVFUNC_2:def 7
'/\' (G \ {PA});
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y),PA be a_partition of Y;
pred a is_independent_of PA,G means
:: BVFUNC_2:def 8
a is_dependent_of CompF(PA,G);
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),
G be Subset of PARTITIONS(Y),
PA be a_partition of Y;
func All(a,PA,G) -> Element of Funcs(Y,BOOLEAN) equals
:: BVFUNC_2:def 9
B_INF(a,CompF(PA,G));
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),
G be Subset of PARTITIONS(Y),
PA be a_partition of Y;
func Ex(a,PA,G) -> Element of Funcs(Y,BOOLEAN) equals
:: BVFUNC_2:def 10
B_SUP(a,CompF(PA,G));
end;

theorem :: BVFUNC_2:5
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(a,PA,G) is_dependent_of CompF(PA,G);

theorem :: BVFUNC_2:6
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(a,PA,G) is_dependent_of CompF(PA,G);

theorem :: BVFUNC_2:7
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(I_el(Y),PA,G) = I_el(Y);

theorem :: BVFUNC_2:8
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(I_el(Y),PA,G) = I_el(Y);

theorem :: BVFUNC_2:9
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(O_el(Y),PA,G) = O_el(Y);

theorem :: BVFUNC_2:10
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(O_el(Y),PA,G) = O_el(Y);

theorem :: BVFUNC_2:11
for a being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(a,PA,G) '<' a;

theorem :: BVFUNC_2:12
for a being Element of Funcs(Y,BOOLEAN),
PA being a_partition of Y holds a '<' Ex(a,PA,G);

theorem :: BVFUNC_2:13
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(a '&' b,PA,G) = All(a,PA,G) '&' All(b,PA,G);

theorem :: BVFUNC_2:14
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(a,PA,G) 'or' All(b,PA,G) '<' All(a 'or' b,PA,G);

theorem :: BVFUNC_2:15
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' All(b,PA,G);

theorem :: BVFUNC_2:16
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(a 'or' b,PA,G) = Ex(a,PA,G) 'or' Ex(b,PA,G);

theorem :: BVFUNC_2:17
for a,b being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
PA being a_partition of Y holds
Ex(a '&' b,PA,G) '<' Ex(a,PA,G) '&' Ex(b,PA,G);

theorem :: BVFUNC_2:18
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(a,PA,G) 'xor' Ex(b,PA,G) '<' Ex(a 'xor' b,PA,G);

theorem :: BVFUNC_2:19
for a,b being Element of Funcs(Y,BOOLEAN), PA being a_partition of Y holds
Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' Ex(a 'imp' b,PA,G);

reserve a, u for Element of Funcs(Y,BOOLEAN);

theorem :: BVFUNC_2:20 :: De'Morgan's Law
for PA being a_partition of Y holds 'not' All(a,PA,G) = Ex('not' a,PA,G);

theorem :: BVFUNC_2:21 :: De'Morgan's Law
for PA being a_partition of Y holds 'not' Ex(a,PA,G) = All('not' a,PA,G);

theorem :: BVFUNC_2:22
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'imp' a,PA,G) = u 'imp' All(a,PA,G);

theorem :: BVFUNC_2:23
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a 'imp' u,PA,G) = Ex(a,PA,G) 'imp' u;

theorem :: BVFUNC_2:24
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'or' a,PA,G) = u 'or' All(a,PA,G);

theorem :: BVFUNC_2:25
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a 'or' u,PA,G) = All(a,PA,G) 'or' u;

theorem :: BVFUNC_2:26
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a 'or' u,PA,G) '<' Ex(a,PA,G) 'or' u;

theorem :: BVFUNC_2:27
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u '&' a,PA,G) = u '&' All(a,PA,G);

theorem :: BVFUNC_2:28
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a '&' u,PA,G) = All(a,PA,G) '&' u;

theorem :: BVFUNC_2:29
for PA being a_partition of Y holds
All(a '&' u,PA,G) '<' Ex(a,PA,G) '&' u;

theorem :: BVFUNC_2:30
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'xor' a,PA,G) '<' u 'xor' All(a,PA,G);

theorem :: BVFUNC_2:31
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a 'xor' u,PA,G) '<' All(a,PA,G) 'xor' u;

theorem :: BVFUNC_2:32
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'eqv' a,PA,G) '<' u 'eqv' All(a,PA,G);

theorem :: BVFUNC_2:33
for PA being a_partition of Y st u is_independent_of PA,G holds
All(a 'eqv' u,PA,G) '<' All(a,PA,G) 'eqv' u;

theorem :: BVFUNC_2:34
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u 'or' a,PA,G) = u 'or' Ex(a,PA,G);

theorem :: BVFUNC_2:35
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(a 'or' u,PA,G) = Ex(a,PA,G) 'or' u;

theorem :: BVFUNC_2:36
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u '&' a,PA,G) = u '&' Ex(a,PA,G);

theorem :: BVFUNC_2:37
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(a '&' u,PA,G) = Ex(a,PA,G) '&' u;

theorem :: BVFUNC_2:38
for PA being a_partition of Y holds
u 'imp' Ex(a,PA,G) '<' Ex(u 'imp' a,PA,G);

theorem :: BVFUNC_2:39
for PA being a_partition of Y holds
Ex(a,PA,G) 'imp' u '<' Ex(a 'imp' u,PA,G);

theorem :: BVFUNC_2:40
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' Ex(a,PA,G) '<' Ex(u 'xor' a,PA,G);

theorem :: BVFUNC_2:41
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(a,PA,G) 'xor' u '<' Ex(a 'xor' u,PA,G);
```