The Mizar abstract of BVFUNC

Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users
The abstract of the Mizar article:: A Theory of Boolean Valued Functions and Quantifiers with Respect to Partitions
by
Shunichi Kobayashi, and
Yatsuka Nakamura
Received December 21, 1998
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);
The abstract of the Mizar article:

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