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

### A Theory of Boolean Valued Functions and Partitions

by
Shunichi Kobayashi, and
Kui Jia

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

```environ

vocabulary MARGREL1, ZF_LANG, BINARITH, ORDINAL2, PARTIT1, FUNCT_2, FRAENKEL,
VALUAT_1, RELAT_1, FUNCT_1, BOOLE, SEQM_3, EQREL_1, T_1TOPSP, SETFAM_1,
TARSKI, BVFUNC_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, XREAL_0, MARGREL1,
VALUAT_1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, FRAENKEL, BINARITH,
EQREL_1, T_1TOPSP, PARTIT1, SEQM_3;
constructors BINARITH, T_1TOPSP, PARTIT1, SEQM_3, PUA2MSS1, VALUAT_1, XREAL_0,
MEMBERED;
clusters SUBSET_1, MARGREL1, PARTIT1, XREAL_0, ARYTM_3, VALUAT_1, BINARITH,
FRAENKEL;
requirements NUMERALS, REAL, SUBSET, BOOLE;

begin :: Chap. 1  Boolean Operations

reserve Y for set;

definition let k,l be boolean set;
func k 'imp' l equals
:: BVFUNC_1:def 1
'not' k 'or' l;

func k 'eqv' l equals
:: BVFUNC_1:def 2
'not' (k 'xor' l);
commutativity;
end;

definition let k,l be boolean set;
cluster k 'imp' l -> boolean;
cluster k 'eqv' l -> boolean;
end;

definition
cluster boolean -> natural set;
end;

definition let k,l be boolean set;
redefine
pred k <= l means
:: BVFUNC_1:def 3
k 'imp' l = TRUE;
synonym k '<' l;
end;

begin :: Chap.2   Boolean Valued Functions

definition let Y;
func BVF(Y) equals
:: BVFUNC_1:def 4
Funcs(Y,BOOLEAN);
end;

definition let Y be set;
cluster BVF(Y) -> functional non empty;
end;

definition let Y be set;
cluster -> boolean-valued Element of BVF Y;
end;

reserve Y for non empty set;
reserve B for Subset of Y;

definition let a be boolean-valued Function, x be set;
redefine
func a.x;
synonym Pj(a,x);
end;

definition let Y;let a be Element of BVF(Y);
redefine
func 'not' a ->Element of BVF(Y);
let b be Element of BVF(Y);
func a '&' b ->Element of BVF(Y);
end;

definition
let p,q be boolean-valued Function;
func p 'or' q -> Function means
:: BVFUNC_1:def 5
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) 'or' (q.x);
commutativity;
func p 'xor' q -> Function means
:: BVFUNC_1:def 6
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) 'xor' (q.x);
commutativity;
end;

definition
let p,q be boolean-valued Function;
cluster p 'or' q -> boolean-valued;
cluster p 'xor' q -> boolean-valued;
end;

definition let A be non empty set;
redefine
let p,q be Element of Funcs(A,BOOLEAN);
func p 'or' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 7
for x being Element of A holds it.x = (p.x) 'or' (q.x);
func p 'xor' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 8
for x being Element of A holds it.x = (p.x) 'xor' (q.x);
end;

definition let Y;let a,b be Element of BVF(Y);
redefine
func a 'or' b ->Element of BVF(Y);
func a 'xor' b ->Element of BVF(Y);
end;

definition
let p,q be boolean-valued Function;
func p 'imp' q -> Function means
:: BVFUNC_1:def 9
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) 'imp' (q.x);
func p 'eqv' q -> Function means
:: BVFUNC_1:def 10
dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) 'eqv' (q.x);
commutativity;
end;

definition
let p,q be boolean-valued Function;
cluster p 'imp' q -> boolean-valued;
cluster p 'eqv' q -> boolean-valued;
end;

definition let A be non empty set;
redefine
let p,q be Element of Funcs(A,BOOLEAN);
func p 'imp' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 11
for x being Element of A holds it.x = ('not' Pj(p,x)) 'or' Pj(q,x);
func p 'eqv' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 12
for x being Element of A holds it.x = 'not' (Pj(p,x) 'xor' Pj(q,x));
end;

definition let Y;let a,b be Element of BVF(Y);
redefine
func a 'imp' b ->Element of BVF(Y);
func a 'eqv' b ->Element of BVF(Y);
end;

definition let Y;
func O_el(Y) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 13
for x being Element of Y holds Pj(it,x)= FALSE;
end;

definition let Y;
func I_el(Y) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 14
for x being Element of Y holds Pj(it,x)= TRUE;
end;

canceled 3;

theorem :: BVFUNC_1:4
for a being boolean-valued Function holds 'not' 'not' a=a;

theorem :: BVFUNC_1:5
for a being Element of Funcs(Y,BOOLEAN) holds
'not' I_el(Y)=O_el(Y) & 'not' O_el(Y)=I_el(Y);

theorem :: BVFUNC_1:6
for a,b being Element of Funcs(Y,BOOLEAN) holds
a '&' a=a;

theorem :: BVFUNC_1:7
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a '&' b '&' c = a '&' (b '&' c);

theorem :: BVFUNC_1:8
for a being Element of Funcs(Y,BOOLEAN) holds
a '&' O_el(Y)=O_el(Y);

theorem :: BVFUNC_1:9
for a being Element of Funcs(Y,BOOLEAN) holds
a '&' I_el(Y)=a;

theorem :: BVFUNC_1:10
for a being Element of Funcs(Y,BOOLEAN) holds
a 'or' a=a;

theorem :: BVFUNC_1:11
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'or' b 'or' c = a 'or' (b 'or' c);

theorem :: BVFUNC_1:12
for a being Element of Funcs(Y,BOOLEAN) holds
a 'or' O_el(Y)=a;

theorem :: BVFUNC_1:13
for a being Element of Funcs(Y,BOOLEAN) holds
a 'or' I_el(Y)=I_el(Y);

theorem :: BVFUNC_1:14  ::Distributive
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c);

theorem :: BVFUNC_1:15  ::Distributive
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b) '&' c = (a '&' c) 'or' (b '&' c);

theorem :: BVFUNC_1:16  ::De'Morgan
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' (a 'or' b)=('not' a) '&' ('not' b);

theorem :: BVFUNC_1:17  ::De'Morgan
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' (a '&' b)=('not' a) 'or' ('not' b);

definition let Y;let a,b be Element of Funcs(Y,BOOLEAN);
pred a '<' b means
:: BVFUNC_1:def 15
for x being Element of Y st Pj(a,x)= TRUE holds Pj(b,x)=TRUE;
reflexivity;
end;

theorem :: BVFUNC_1:18
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '<' b) & (b '<' a) implies a=b)&
((a '<' b) & (b '<' c) implies a '<' c);

theorem :: BVFUNC_1:19
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b)=I_el(Y) iff a '<' b;

theorem :: BVFUNC_1:20
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) iff a = b;

theorem :: BVFUNC_1:21
for a being Element of Funcs(Y,BOOLEAN) holds
O_el(Y) '<' a & a '<' I_el(Y);

begin :: Chap. 3  Infimum and Supremum

definition let Y;let a be Element of Funcs(Y,BOOLEAN);
func B_INF(a) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 16
it = I_el(Y) if (for x being Element of Y holds Pj(a,x)=TRUE)
otherwise it = O_el(Y);

func B_SUP(a) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 17
it = O_el(Y) if (for x being Element of Y holds Pj(a,x)=FALSE)
otherwise it = I_el(Y);
end;

theorem :: BVFUNC_1:22
for a being Element of Funcs(Y,BOOLEAN) holds
'not' B_INF(a) = B_SUP('not' a) & 'not' B_SUP(a)=B_INF('not' a);

theorem :: BVFUNC_1:23
B_INF(O_el(Y)) = O_el(Y) & B_INF(I_el(Y))=I_el(Y) &
B_SUP(O_el(Y)) = O_el(Y) & B_SUP(I_el(Y))=I_el(Y);

definition let Y;
cluster O_el(Y) -> constant;
end;

definition let Y;
cluster I_el(Y) -> constant;
end;

definition
let Y be non empty set;
cluster constant Element of Funcs(Y,BOOLEAN);
end;

theorem :: BVFUNC_1:24
for a being constant Element of Funcs(Y,BOOLEAN) holds
a=O_el(Y) or a=I_el(Y);

theorem :: BVFUNC_1:25
for d being constant Element of Funcs(Y,BOOLEAN) holds
B_INF(d) = d & B_SUP(d) = d;

theorem :: BVFUNC_1:26
for a,b being Element of Funcs(Y,BOOLEAN) holds
B_INF(a '&' b) = B_INF(a) '&' B_INF(b) &
B_SUP(a 'or' b) = B_SUP(a) 'or' B_SUP(b);

theorem :: BVFUNC_1:27
for a being Element of Funcs(Y,BOOLEAN),
d being constant Element of Funcs(Y,BOOLEAN) holds
B_INF(d 'imp' a) = d 'imp' B_INF(a) &
B_INF(a 'imp' d) = B_SUP(a) 'imp' d;

theorem :: BVFUNC_1:28
for a being Element of Funcs(Y,BOOLEAN),
d being constant Element of Funcs(Y,BOOLEAN) holds
B_INF(d 'or' a) = d 'or' B_INF(a) &
B_SUP(d '&' a) = d '&' B_SUP(a) &
B_SUP(a '&' d) = B_SUP(a) '&' d;

theorem :: BVFUNC_1:29
for a being Element of Funcs(Y,BOOLEAN),x being Element of Y holds
Pj(B_INF(a),x) '<' Pj(a,x);

theorem :: BVFUNC_1:30
for a being Element of Funcs(Y,BOOLEAN),x being Element of Y holds
Pj(a,x) '<' Pj(B_SUP(a),x);

begin :: Chap. 4  Boolean Valued Functions and Partitions

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
pred a is_dependent_of PA means
:: BVFUNC_1:def 18
for F being set st F in PA
for x1,x2 being set st x1 in F & x2 in F holds a.x1=a.x2;
end;

theorem :: BVFUNC_1:31
for a being Element of Funcs(Y,BOOLEAN) holds
a is_dependent_of %I(Y);

theorem :: BVFUNC_1:32
for a being constant Element of Funcs(Y,BOOLEAN) holds
a is_dependent_of %O(Y);

definition let Y;let PA be a_partition of Y;
redefine mode Element of PA -> Subset of Y;
end;

definition let Y;let x be Element of Y;let PA be a_partition of Y;
redefine func EqClass(x,PA) -> Element of PA;
synonym Lift(x,PA);
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
func B_INF(a,PA) -> Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 19
for y being Element of Y holds
( (for x being Element of Y st x in EqClass(y,PA) holds Pj(a,x)=TRUE)
implies Pj(it,y) = TRUE ) &
(not (for x being Element of Y st x in EqClass(y,PA) holds Pj(a,x)=TRUE)
implies Pj(it,y) = FALSE);
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
func B_SUP(a,PA) -> Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 20
for y being Element of Y holds
( (ex x being Element of Y st x in EqClass(y,PA) & Pj(a,x)=TRUE)
implies Pj(it,y) = TRUE ) &
(not (ex x being Element of Y st x in EqClass(y,PA) & Pj(a,x)=TRUE)
implies Pj(it,y) = FALSE);
end;

theorem :: BVFUNC_1:33
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
B_INF(a,PA) is_dependent_of PA;

theorem :: BVFUNC_1:34
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
B_SUP(a,PA) is_dependent_of PA;

theorem :: BVFUNC_1:35
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
B_INF(a,PA) '<' a;

theorem :: BVFUNC_1:36
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
a '<' B_SUP(a,PA);

theorem :: BVFUNC_1:37
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
'not' B_INF(a,PA) = B_SUP('not' a,PA);

theorem :: BVFUNC_1:38
for a being Element of Funcs(Y,BOOLEAN) holds
B_INF(a,%O(Y))=B_INF(a);

theorem :: BVFUNC_1:39
for a being Element of Funcs(Y,BOOLEAN) holds
B_SUP(a,%O(Y))=B_SUP(a);

theorem :: BVFUNC_1:40
for a being Element of Funcs(Y,BOOLEAN) holds
B_INF(a,%I(Y))=a;

theorem :: BVFUNC_1:41
for a being Element of Funcs(Y,BOOLEAN) holds
B_SUP(a,%I(Y))=a;

theorem :: BVFUNC_1:42
for a,b being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds B_INF(a '&' b,PA)=B_INF(a,PA) '&' B_INF(b,PA);

theorem :: BVFUNC_1:43
for a,b being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds B_SUP(a 'or' b,PA)=B_SUP(a,PA) 'or' B_SUP(b,PA);

definition let Y;let f be Element of Funcs(Y,BOOLEAN);
func GPart(f) -> a_partition of Y equals
:: BVFUNC_1:def 21
{{x where x is Element of Y:f.x = TRUE },
{x' where x' is Element of Y:f.x' = FALSE}} \ {{}};
end;

theorem :: BVFUNC_1:44
for a being Element of Funcs(Y,BOOLEAN) holds
a is_dependent_of GPart(a);

theorem :: BVFUNC_1:45
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
st a is_dependent_of PA holds PA is_finer_than GPart(a);
```