The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part I

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received March 13, 1999

MML identifier: BVFUNC_5

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;


begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem :: BVFUNC_5:1
for a,b being Element of Funcs(Y,BOOLEAN) holds
a=I_el(Y) & b=I_el(Y) iff (a '&' b)=I_el(Y);

theorem :: BVFUNC_5:2
for a,b being Element of Funcs(Y,BOOLEAN) st
a=I_el(Y) & (a 'imp' b)=I_el(Y) holds b=I_el(Y);

theorem :: BVFUNC_5:3
for a,b being Element of Funcs(Y,BOOLEAN) st
a=I_el(Y) holds (a 'or' b)=I_el(Y);

canceled;

theorem :: BVFUNC_5:5
for a,b being Element of Funcs(Y,BOOLEAN) st
b=I_el(Y) holds (a 'imp' b)=I_el(Y);

theorem :: BVFUNC_5:6
for a,b being Element of Funcs(Y,BOOLEAN) st
('not' a)=I_el(Y) holds (a 'imp' b)=I_el(Y);

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

theorem :: BVFUNC_5:8  :: Identity law
  for a being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' a)=I_el(Y);

theorem :: BVFUNC_5:9
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b)=I_el(Y) iff ('not' b 'imp' 'not' a)=I_el(Y);

theorem :: BVFUNC_5:10
for a,b,c being Element of Funcs(Y,BOOLEAN) st
(a 'imp' b)=I_el(Y) & (b 'imp' c)=I_el(Y) holds
(a 'imp' c)=I_el(Y);

theorem :: BVFUNC_5:11
for a,b being Element of Funcs(Y,BOOLEAN) st
(a 'imp' b)=I_el(Y) & (a 'imp' 'not' b)=I_el(Y) holds
'not' a=I_el(Y);

theorem :: BVFUNC_5:12
for a being Element of Funcs(Y,BOOLEAN) holds
('not' a 'imp' a) 'imp' a = I_el(Y);

theorem :: BVFUNC_5:13
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) 'imp' ('not' (b '&' c) 'imp' 'not' (a '&' c)) =I_el(Y);

theorem :: BVFUNC_5:14
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))=I_el(Y);

theorem :: BVFUNC_5:15
for a,b,c being Element of Funcs(Y,BOOLEAN) st
(a 'imp' b)=I_el(Y) holds (b 'imp' c) 'imp' (a 'imp' c)=I_el(Y);

theorem :: BVFUNC_5:16
for a,b being Element of Funcs(Y,BOOLEAN) holds
b 'imp' (a 'imp' b) =I_el(Y);

theorem :: BVFUNC_5:17
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'imp' b) 'imp' c) 'imp' (b 'imp' c)=I_el(Y);

theorem :: BVFUNC_5:18
for a,b being Element of Funcs(Y,BOOLEAN) holds
b 'imp' ((b 'imp' a) 'imp' a)=I_el(Y);

theorem :: BVFUNC_5:19  :: Contraposition
  for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))=I_el(Y);

theorem :: BVFUNC_5:20
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))=I_el(Y);

theorem :: BVFUNC_5:21  :: A Hilbert axiom
  for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)=I_el(Y);

theorem :: BVFUNC_5:22  :: Frege's law
  for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))=I_el(Y);

theorem :: BVFUNC_5:23
for a,b being Element of Funcs(Y,BOOLEAN) holds
a=I_el(Y) implies (a 'imp' b) 'imp' b=I_el(Y);

theorem :: BVFUNC_5:24
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
c 'imp' (b 'imp' a)=I_el(Y) implies b 'imp' (c 'imp' a)=I_el(Y);

theorem :: BVFUNC_5:25
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
c 'imp' (b 'imp' a)=I_el(Y) & b=I_el(Y) implies
c 'imp' a=I_el(Y);

theorem :: BVFUNC_5:26
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
c 'imp' (b 'imp' a)=I_el(Y) & b=I_el(Y) & c = I_el(Y) implies
a=I_el(Y);

theorem :: BVFUNC_5:27
for b,c being Element of Funcs(Y,BOOLEAN) holds
b 'imp' (b 'imp' c)=I_el(Y) implies b 'imp' c = I_el(Y);

theorem :: BVFUNC_5:28
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' (b 'imp' c)) = I_el(Y) implies
(a 'imp' b) 'imp' (a 'imp' c) = I_el(Y);

theorem :: BVFUNC_5:29
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' (b 'imp' c)) = I_el(Y) & a 'imp' b = I_el(Y) implies
a 'imp' c = I_el(Y);

theorem :: BVFUNC_5:30
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' (b 'imp' c)) = I_el(Y) & a 'imp' b = I_el(Y) & a = I_el(Y)
implies c = I_el(Y);

theorem :: BVFUNC_5:31
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'imp' c) = I_el(Y) & a 'imp' (c 'imp' d) = I_el(Y)
implies a 'imp' (b 'imp' d) = I_el(Y);

theorem :: BVFUNC_5:32
for a,b being Element of Funcs(Y,BOOLEAN) holds
('not' a 'imp' 'not' b) 'imp' (b 'imp' a) = I_el(Y);

theorem :: BVFUNC_5:33
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) 'imp' ('not' b 'imp' 'not' a)=I_el(Y);

theorem :: BVFUNC_5:34
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' 'not' b) 'imp' (b 'imp' 'not' a)=I_el(Y);

theorem :: BVFUNC_5:35
for a,b being Element of Funcs(Y,BOOLEAN) holds
('not' a 'imp' b) 'imp' ('not' b 'imp' a)=I_el(Y);

theorem :: BVFUNC_5:36
for a being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' 'not' a) 'imp' 'not' a=I_el(Y);

theorem :: BVFUNC_5:37
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a 'imp' (a 'imp' b)=I_el(Y);

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

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

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

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