The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part I

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received December 21, 1998

MML identifier: BVFUNC_3

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTIT1, FUNCT_2, MARGREL1, EQREL_1, BVFUNC_1, ZF_LANG, T_1TOPSP,
      BVFUNC_2, BINARITH, FUNCT_1;
 notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BINARITH,
      BVFUNC_1, BVFUNC_2;
 constructors BINARITH, BVFUNC_2, BVFUNC_1;
 clusters VALUAT_1, MARGREL1, FRAENKEL;


begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set,
        G for Subset of PARTITIONS(Y),
        a,b,c,u for Element of Funcs(Y,BOOLEAN),
        PA for a_partition of Y;

theorem :: BVFUNC_3:1
    (a 'imp' b) '<' (All(a,PA,G) 'imp' Ex(b,PA,G));

theorem :: BVFUNC_3:2
    (All(a,PA,G) '&' All(b,PA,G)) '<' (a '&' b);

theorem :: BVFUNC_3:3
    (a '&' b) '<' (Ex(a,PA,G) '&' Ex(b,PA,G));

theorem :: BVFUNC_3:4
    'not' (All(a,PA,G) '&' All(b,PA,G)) = Ex('not' a,PA,G) 'or' Ex('not' b,PA,G
);

theorem :: BVFUNC_3:5
    'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) = All('not' a,PA,G) 'or' All('not' b,PA,G
);

theorem :: BVFUNC_3:6
    (All(a,PA,G) 'or' All(b,PA,G)) '<' (a 'or' b);

theorem :: BVFUNC_3:7
    (a 'or' b) '<' (Ex(a,PA,G) 'or' Ex(b,PA,G));

theorem :: BVFUNC_3:8
    (a 'xor' b) '<'
   ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex(
'not' b,PA,G)));

theorem :: BVFUNC_3:9
    All(a 'or' b,PA,G) '<' All(a,PA,G) 'or' Ex(b,PA,G);

theorem :: BVFUNC_3:10
    All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' All(b,PA,G);

theorem :: BVFUNC_3:11
    All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' Ex(b,PA,G);

theorem :: BVFUNC_3:12
    Ex(a,PA,G) '&' All(b,PA,G) '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:13
    All(a,PA,G) '&' Ex(b,PA,G) '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:14
    All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G);

theorem :: BVFUNC_3:15
    All(a 'imp' b,PA,G) '<' Ex(a,PA,G) 'imp' Ex(b,PA,G);

theorem :: BVFUNC_3:16
    Ex(a,PA,G) 'imp' All(b,PA,G) '<' All(a 'imp' b,PA,G);

theorem :: BVFUNC_3:17
    (a 'imp' b) '<' (a 'imp' Ex(b,PA,G));

theorem :: BVFUNC_3:18
    (a 'imp' b) '<' (All(a,PA,G) 'imp' b);

theorem :: BVFUNC_3:19
    Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G);

theorem :: BVFUNC_3:20
    All(a,PA,G) '<' Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:21
    u is_independent_of PA,G implies
   Ex(u 'imp' a,PA,G) '<' (u 'imp' Ex(a,PA,G));

theorem :: BVFUNC_3:22
    u is_independent_of PA,G implies
   Ex(a 'imp' u,PA,G) '<' (All(a,PA,G) 'imp' u);

theorem :: BVFUNC_3:23
    All(a,PA,G) 'imp' Ex(b,PA,G) = Ex(a 'imp' b,PA,G);

theorem :: BVFUNC_3:24
    All(a,PA,G) 'imp' All(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G);

theorem :: BVFUNC_3:25
    Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G);

theorem :: BVFUNC_3:26
  All(a 'imp' b,PA,G) = All('not' a 'or' b,PA,G);

theorem :: BVFUNC_3:27
     All(a 'imp' b,PA,G) = 'not' (Ex(a '&' 'not' b,PA,G));

theorem :: BVFUNC_3:28
    Ex(a,PA,G) '<' 'not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G));

theorem :: BVFUNC_3:29
    Ex(a,PA,G) '<'
    'not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G));

theorem :: BVFUNC_3:30
    Ex(a,PA,G) '&' All(a 'imp' b,PA,G) '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:31
    Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G) '<' 'not' All(a 'imp' b,PA,G);

theorem :: BVFUNC_3:32
    All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G) '<' All(a 'imp' b,PA,G);

theorem :: BVFUNC_3:33
    All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:34
    All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G) '<'
    All(a 'imp' 'not' b,PA,G);

theorem :: BVFUNC_3:35
    All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G) '<'
    All(a 'imp' 'not' b,PA,G);

theorem :: BVFUNC_3:36
    All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' 'not' b,PA,G);

theorem :: BVFUNC_3:37
    All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G) '<' Ex(a '&' 'not' b,PA,G);

theorem :: BVFUNC_3:38
    Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:39
    All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G)
   '<' All(a 'imp' 'not' b,PA,G);

theorem :: BVFUNC_3:40
    Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' b,PA,G);

theorem :: BVFUNC_3:41
    Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' 'not' b,PA,G);