:: Propositional Calculus for Boolean Valued Functions, I :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received March 13, 1999 :: Copyright (c) 1999-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, MARGREL1, BVFUNC_1, XBOOLEAN, FUNCT_1; notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, BVFUNC_1; constructors BVFUNC_1, NUMBERS; registrations XBOOLEAN, MARGREL1; requirements SUBSET, BOOLE, NUMERALS; begin ::Chap. 1 Propositional Calculus reserve Y for non empty set; theorem :: BVFUNC_5:1 for a,b being Function of Y,BOOLEAN holds a=I_el(Y) & b=I_el(Y) iff (a '&' b)=I_el(Y); theorem :: BVFUNC_5:2 for b being Function of Y,BOOLEAN st (I_el(Y) 'imp' b)=I_el (Y) holds b=I_el(Y); theorem :: BVFUNC_5:3 for a,b being Function of Y,BOOLEAN st a=I_el(Y) holds (a 'or' b )=I_el(Y); theorem :: BVFUNC_5:4 for a,b being Function of Y,BOOLEAN st b=I_el(Y) holds (a 'imp' b)=I_el(Y); theorem :: BVFUNC_5:5 for a,b being Function of Y,BOOLEAN st ('not' a)=I_el(Y) holds ( a 'imp' b)=I_el(Y); theorem :: BVFUNC_5:6 for a being Function of Y,BOOLEAN holds 'not' (a '&' 'not' a)= I_el(Y); theorem :: BVFUNC_5:7 :: Identity law for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y; theorem :: BVFUNC_5:8 for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el(Y) iff ('not' b 'imp' 'not' a)=I_el(Y); theorem :: BVFUNC_5:9 for a,b,c being Function of 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:10 for a,b being Function of 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:11 for a being Function of Y,BOOLEAN holds ('not' a 'imp' a) 'imp' a = I_el(Y); theorem :: BVFUNC_5:12 for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ( 'not' (b '&' c) 'imp' 'not' (a '&' c)) =I_el(Y); theorem :: BVFUNC_5:13 for a,b,c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (( b 'imp' c) 'imp' (a 'imp' c))=I_el(Y); theorem :: BVFUNC_5:14 for a,b,c being Function of Y,BOOLEAN st (a 'imp' b)=I_el( Y) holds (b 'imp' c) 'imp' (a 'imp' c)=I_el(Y); theorem :: BVFUNC_5:15 for a,b being Function of Y,BOOLEAN holds b 'imp' (a 'imp' b) =I_el(Y); theorem :: BVFUNC_5:16 for a,b,c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c ) 'imp' (b 'imp' c)=I_el(Y); theorem :: BVFUNC_5:17 for a,b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a)=I_el(Y); theorem :: BVFUNC_5:18 :: Contraposition for a,b,c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a) ) 'imp' (b 'imp' (c 'imp' a))=I_el(Y); theorem :: BVFUNC_5:19 for a,b,c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' (( a 'imp' b) 'imp' (a 'imp' c))=I_el(Y); theorem :: BVFUNC_5:20 :: A Hilbert axiom for a,b,c being Function of Y,BOOLEAN holds (b 'imp' (b 'imp' c) ) 'imp' (b 'imp' c)=I_el(Y); theorem :: BVFUNC_5:21 :: Frege's law for a,b,c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))=I_el(Y); theorem :: BVFUNC_5:22 for a,b being Function of Y,BOOLEAN holds a=I_el(Y) implies (a 'imp' b) 'imp' b=I_el(Y); theorem :: BVFUNC_5:23 for a,b,c being Function of Y,BOOLEAN holds c 'imp' (b 'imp' a)= I_el(Y) implies b 'imp' (c 'imp' a)=I_el(Y); theorem :: BVFUNC_5:24 for a,b,c being Function of 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:25 for a being Function of Y,BOOLEAN holds I_el Y 'imp' (I_el Y 'imp' a)=I_el Y implies a=I_el Y; theorem :: BVFUNC_5:26 for b,c being Function of Y,BOOLEAN holds b 'imp' (b 'imp' c)= I_el(Y) implies b 'imp' c = I_el(Y); theorem :: BVFUNC_5:27 for a,b,c being Function of 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:28 for a,b,c being Function of 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:29 for a,b,c being Function of 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:30 for a,b,c,d being Function of 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:31 for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' 'not' b ) 'imp' (b 'imp' a) = I_el(Y); theorem :: BVFUNC_5:32 for a,b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ( 'not' b 'imp' 'not' a)=I_el(Y); theorem :: BVFUNC_5:33 for a,b being Function of Y,BOOLEAN holds (a 'imp' 'not' b) 'imp' (b 'imp' 'not' a)=I_el(Y); theorem :: BVFUNC_5:34 for a,b being Function of Y,BOOLEAN holds ('not' a 'imp' b) 'imp' ('not' b 'imp' a)=I_el(Y); theorem :: BVFUNC_5:35 for a being Function of Y,BOOLEAN holds (a 'imp' 'not' a) 'imp' 'not' a=I_el(Y); theorem :: BVFUNC_5:36 for a,b being Function of Y,BOOLEAN holds 'not' a 'imp' (a 'imp' b)=I_el(Y); theorem :: BVFUNC_5:37 ::De'Morgan for a,b,c being Function of Y,BOOLEAN holds 'not' (a '&' b '&' c )=('not' a) 'or' ('not' b) 'or' ('not' c); theorem :: BVFUNC_5:38 ::De'Morgan for a,b,c being Function of Y,BOOLEAN holds 'not' (a 'or' b 'or' c)=('not' a) '&' ('not' b) '&' ('not' c); theorem :: BVFUNC_5:39 ::Distributive for a,b,c,d being Function of Y,BOOLEAN holds a 'or' (b '&' c '&' d) = (a 'or' b) '&' (a 'or' c) '&' (a 'or' d); theorem :: BVFUNC_5:40 ::Distributive for a,b,c,d being Function of Y,BOOLEAN holds a '&' (b 'or' c 'or' d) = (a '&' b) 'or' (a '&' c) 'or' (a '&' d);