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

### Predicate Calculus for Boolean Valued Functions. Part I

by
Shunichi Kobayashi, and
Yatsuka Nakamura

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);

```