:: Several Classes of {BCI}-algebras and Their Properties :: by Yuzhong Ding :: :: Received February 23, 2007 :: Copyright (c) 2007-2021 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 STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, FUNCT_1, SUPINF_2, FUNCT_5, ZFMISC_1, UNIALG_2, TARSKI, REALSET1, RELAT_1, XXREAL_0, WAYBEL15, CARD_FIL, RCOMP_1, FILTER_0, BCIALG_1, CARD_1; notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, ORDINAL1, BINOP_1, FUNCT_5, REALSET1, STRUCT_0, RELAT_1; constructors BINOP_1, REALSET1, MIDSP_1, FUNCT_5, RELSET_1, NUMBERS; registrations RELAT_1, STRUCT_0, CARD_1; requirements SUBSET, BOOLE; begin :: The Basics of General Theory of BCI-algebra definition struct (1-sorted) BCIStr (# carrier -> set, InternalDiff -> BinOp of the carrier #); end; registration cluster non empty strict for BCIStr; end; definition let A be BCIStr; let x,y be Element of A; func x \ y -> Element of A equals :: BCIALG_1:def 1 (the InternalDiff of A).(x,y); end; definition struct (BCIStr,ZeroStr) BCIStr_0 (# carrier -> set, InternalDiff -> BinOp of the carrier, ZeroF -> Element of the carrier #); end; registration cluster non empty strict for BCIStr_0; end; definition let IT be non empty BCIStr_0, x be Element of IT; func x` -> Element of IT equals :: BCIALG_1:def 2 0.IT\x; end; definition let IT be non empty BCIStr_0; attr IT is being_B means :: BCIALG_1:def 3 for x,y,z being Element of IT holds ((x\y)\( z\y))\(x\z)=0.IT; attr IT is being_C means :: BCIALG_1:def 4 for x,y,z being Element of IT holds ((x\y)\z )\((x\z)\y)=0.IT; attr IT is being_I means :: BCIALG_1:def 5 for x being Element of IT holds x\x=0.IT; attr IT is being_K means :: BCIALG_1:def 6 for x,y being Element of IT holds (x\y)\x=0. IT; attr IT is being_BCI-4 means :: BCIALG_1:def 7 for x,y being Element of IT holds (x\y= 0.IT&y\x=0.IT implies x = y); attr IT is being_BCK-5 means :: BCIALG_1:def 8 for x being Element of IT holds x`=0.IT; end; definition func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9 BCIStr_0 (# {0}, op2, op0 #); end; registration cluster BCI-EXAMPLE -> strict 1-element; end; registration cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5; end; registration cluster strict being_B being_C being_I being_BCI-4 being_BCK-5 for non empty BCIStr_0; end; definition mode BCI-algebra is being_B being_C being_I being_BCI-4 non empty BCIStr_0; end; definition mode BCK-algebra is being_BCK-5 BCI-algebra; end; definition let X be BCI-algebra; mode SubAlgebra of X -> BCI-algebra means :: BCIALG_1:def 10 0.it = 0.X & the carrier of it c= the carrier of X & the InternalDiff of it = (the InternalDiff of X)|| the carrier of it; end; ::T1.1.11 theorem :: BCIALG_1:1 for X being non empty BCIStr_0 holds (X is BCI-algebra iff (X is being_I & X is being_BCI-4 &for x,y,z being Element of X holds ((x\y)\(x\z))\(z \y)=0.X & (x\(x\y))\y = 0.X )); definition let IT be non empty BCIStr_0; let x,y be Element of IT; pred x <= y means :: BCIALG_1:def 11 x \ y = 0.IT; end; reserve X for BCI-algebra; reserve x,y,z,u,a,b for Element of X; reserve IT for non empty Subset of X; theorem :: BCIALG_1:2 x \ 0.X = x; theorem :: BCIALG_1:3 x\y=0.X & y\z=0.X implies x\z=0.X; theorem :: BCIALG_1:4 x\y=0.X implies (x\z)\(y\z)=0.X & (z\y)\(z\x)=0.X; theorem :: BCIALG_1:5 x <= y implies x\z <= y\z & z\y <= z\x; theorem :: BCIALG_1:6 x\y=0.X implies (y\x)` = 0.X; theorem :: BCIALG_1:7 (x\y)\z = (x\z)\y; theorem :: BCIALG_1:8 x\(x\(x\y)) = x\y; theorem :: BCIALG_1:9 (x\y)` = x`\y`; theorem :: BCIALG_1:10 ((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X; theorem :: BCIALG_1:11 ::T1.1.6 for X being non empty BCIStr_0 holds (X is BCI-algebra iff (X is being_BCI-4 & for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0. X = x )); theorem :: BCIALG_1:12 (for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x)) implies X is BCK-algebra; theorem :: BCIALG_1:13 (for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y) implies X is BCK-algebra; theorem :: BCIALG_1:14 (for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x) implies X is BCK-algebra; theorem :: BCIALG_1:15 (for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\ (y\z) ) implies X is BCK-algebra; theorem :: BCIALG_1:16 (for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y) implies X is BCK-algebra; theorem :: BCIALG_1:17 (for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y\ x))=0.X) implies X is BCK-algebra; theorem :: BCIALG_1:18 for X being BCI-algebra holds X is being_K iff X is BCK-algebra; definition let X be BCI-algebra; ::P4 1.3 atom BranchV func BCK-part(X) -> non empty Subset of X equals :: BCIALG_1:def 12 {x where x is Element of X: 0.X<=x}; end; theorem :: BCIALG_1:19 0.X in BCK-part(X); theorem :: BCIALG_1:20 for x,y being Element of BCK-part(X) holds x\y in BCK-part(X); theorem :: BCIALG_1:21 for x being Element of X,y being Element of BCK-part(X) holds x\y <= x; theorem :: BCIALG_1:22 X is SubAlgebra of X; definition let X be BCI-algebra,IT be SubAlgebra of X; attr IT is proper means :: BCIALG_1:def 13 IT <> X; end; registration let X; cluster non proper for SubAlgebra of X; end; definition let X be BCI-algebra,IT be Element of X; attr IT is atom means :: BCIALG_1:def 14 for z being Element of X holds z\IT=0.X implies z=IT; end; definition let X be BCI-algebra; func AtomSet(X) -> non empty Subset of X equals :: BCIALG_1:def 15 {x where x is Element of X:x is atom}; end; theorem :: BCIALG_1:23 0.X in AtomSet(X); theorem :: BCIALG_1:24 for x being Element of X holds x in AtomSet(X) iff for z being Element of X holds z\(z\x)=x; theorem :: BCIALG_1:25 for x being Element of X holds x in AtomSet(X) iff for u,z being Element of X holds (z\u)\(z\x)=x\u; theorem :: BCIALG_1:26 for x being Element of X holds x in AtomSet(X) iff for y,z being Element of X holds x\(z\y)<=y\(z\x); theorem :: BCIALG_1:27 for x being Element of X holds x in AtomSet(X) iff for y,z,u being Element of X holds (x\u)\(z\y)<=(y\u)\(z\x); theorem :: BCIALG_1:28 for x being Element of X holds x in AtomSet(X) iff for z being Element of X holds z`\x`=x\z; theorem :: BCIALG_1:29 for x being Element of X holds x in AtomSet(X) iff x``=x; theorem :: BCIALG_1:30 for x being Element of X holds x in AtomSet(X) iff for z being Element of X holds (z\x)`=x\z; theorem :: BCIALG_1:31 for x being Element of X holds x in AtomSet(X) iff for z being Element of X holds ((x\z)`)`=x\z; theorem :: BCIALG_1:32 for x being Element of X holds x in AtomSet(X) iff for z,u being Element of X holds z\(z\(x\u))=x\u; theorem :: BCIALG_1:33 ::tuilun1.3.3 for a being Element of AtomSet(X),x being Element of X holds a\x in AtomSet(X); definition let X be BCI-algebra,a,b be Element of AtomSet(X); redefine func a\b -> Element of AtomSet(X); end; theorem :: BCIALG_1:34 for x being Element of X holds x` in AtomSet(X); theorem :: BCIALG_1:35 for x being Element of X holds ex a being Element of AtomSet(X) st a<=x; definition let X be BCI-algebra; attr X is generated_by_atom means :: BCIALG_1:def 16 for x being Element of X holds ex a being Element of AtomSet(X) st a<=x; end; definition let X be BCI-algebra,a be Element of AtomSet(X); func BranchV(a) -> non empty Subset of X equals :: BCIALG_1:def 17 {x where x is Element of X:a <=x}; end; theorem :: BCIALG_1:36 for X being BCI-algebra holds X is generated_by_atom; theorem :: BCIALG_1:37 for a,b being Element of AtomSet(X),x being Element of BranchV(b) holds a\x =a\b; theorem :: BCIALG_1:38 for a being Element of AtomSet(X),x being Element of BCK-part(X) holds a\x =a ; theorem :: BCIALG_1:39 for a,b being Element of AtomSet(X),x being Element of BranchV(a ), y being Element of BranchV(b) holds x\y in BranchV(a\b); theorem :: BCIALG_1:40 for a being Element of AtomSet(X),x,y being Element of BranchV(a) holds x\y in BCK-part(X); theorem :: BCIALG_1:41 for a,b being Element of AtomSet(X),x being Element of BranchV(a), y being Element of BranchV(b) st a<>b holds not x\y in BCK-part(X); theorem :: BCIALG_1:42 for a,b being Element of AtomSet(X) st a<>b holds BranchV(a) /\ BranchV(b) = {}; ::Ideal definition let X be BCI-algebra; mode Ideal of X -> non empty Subset of X means :: BCIALG_1:def 18 0.X in it & for x,y being Element of X st x\y in it & y in it holds x in it; end; definition let X be BCI-algebra, IT be Ideal of X; attr IT is closed means :: BCIALG_1:def 19 for x being Element of IT holds x` in IT; end; registration let X; cluster closed for Ideal of X; end; theorem :: BCIALG_1:43 {0.X} is closed Ideal of X; theorem :: BCIALG_1:44 the carrier of X is closed Ideal of X; theorem :: BCIALG_1:45 BCK-part(X) is closed Ideal of X; theorem :: BCIALG_1:46 IT is Ideal of X implies for x,y being Element of X st x in IT & y<=x holds y in IT; begin :: Several Classes of BCI-algebra---associative BCI-algebra definition let IT be BCI-algebra; attr IT is associative means :: BCIALG_1:def 20 for x,y,z being Element of IT holds x\y \z = x\(y\z); attr IT is quasi-associative means :: BCIALG_1:def 21 for x being Element of IT holds x ``=x`; attr IT is positive-implicative means :: BCIALG_1:def 22 for x,y being Element of IT holds (x\(x\y))\(y\x)=x\(x\(y\(y\x))); attr IT is weakly-positive-implicative means :: BCIALG_1:def 23 for x,y,z being Element of IT holds (x\y)\z=((x\z)\z)\(y\z); attr IT is implicative means :: BCIALG_1:def 24 for x,y being Element of IT holds (x\(x \y))\(y\x)=y\(y\x); attr IT is weakly-implicative means :: BCIALG_1:def 25 for x,y being Element of IT holds (x\(y\ x))\(y\x)`=x; attr IT is p-Semisimple means :: BCIALG_1:def 26 for x,y being Element of IT holds x\(x \y) = y; attr IT is alternative means :: BCIALG_1:def 27 for x,y being Element of IT holds x\(x\ y) = (x\x)\y & (x\y)\y=x\(y\y); end; registration cluster BCI-EXAMPLE -> implicative positive-implicative p-Semisimple associative weakly-implicative weakly-positive-implicative; end; registration cluster implicative positive-implicative p-Semisimple associative weakly-implicative weakly-positive-implicative for BCI-algebra; end; theorem :: BCIALG_1:47 X is associative iff for x being Element of X holds x`=x; theorem :: BCIALG_1:48 (for x,y being Element of X holds y\x=x\y) iff X is associative; theorem :: BCIALG_1:49 for X being non empty BCIStr_0 holds (X is associative BCI-algebra iff for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x ); theorem :: BCIALG_1:50 for X being non empty BCIStr_0 holds (X is associative BCI-algebra iff for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x ); theorem :: BCIALG_1:51 for X being non empty BCIStr_0 holds (X is associative BCI-algebra iff for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x ); begin :: Several Classes of BCI-algebra----p-Semisimple BCI-algebra theorem :: BCIALG_1:52 X is p-Semisimple iff for x being Element of X holds x is atom; theorem :: BCIALG_1:53 X is p-Semisimple implies BCK-part(X)={0.X}; theorem :: BCIALG_1:54 X is p-Semisimple iff for x being Element of X holds x`` = x; theorem :: BCIALG_1:55 X is p-Semisimple iff for x,y holds y\(y\x) = x; theorem :: BCIALG_1:56 X is p-Semisimple iff for x,y,z holds (z\y)\(z\x) = x\y; theorem :: BCIALG_1:57 X is p-Semisimple iff for x,y,z holds x\(z\y) = y\(z\x); theorem :: BCIALG_1:58 X is p-Semisimple iff for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x); theorem :: BCIALG_1:59 X is p-Semisimple iff for x,z holds z`\x` = x\z; theorem :: BCIALG_1:60 X is p-Semisimple iff for x,z holds (x\z)`` = x\z; theorem :: BCIALG_1:61 X is p-Semisimple iff for x,u,z holds z\(z\(x\u)) = x\u; theorem :: BCIALG_1:62 ::TL2232: X is p-Semisimple iff for x st x`=0.X holds x=0.X; theorem :: BCIALG_1:63 X is p-Semisimple iff for x,y holds x\y`=y\x`; theorem :: BCIALG_1:64 X is p-Semisimple iff for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u); theorem :: BCIALG_1:65 X is p-Semisimple iff for x,y,z holds (x\y)\(z\y)=x\z; theorem :: BCIALG_1:66 X is p-Semisimple iff for x,y,z holds x\(y\z)=(z\y)\x`; theorem :: BCIALG_1:67 X is p-Semisimple iff for x,y,z st y\x=z\x holds y=z; theorem :: BCIALG_1:68 X is p-Semisimple iff for x,y,z st x\y=x\z holds y=z; theorem :: BCIALG_1:69 for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra iff for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x\0.X=x ); theorem :: BCIALG_1:70 for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra iff (X is being_I &for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x )); begin theorem :: BCIALG_1:71 X is quasi-associative iff for x being Element of X holds x`<=x; theorem :: BCIALG_1:72 X is quasi-associative iff for x,y being Element of X holds (x\y )`=(y\x)`; theorem :: BCIALG_1:73 X is quasi-associative iff for x,y being Element of X holds x`\y =(x\y)`; theorem :: BCIALG_1:74 X is quasi-associative iff for x,y being Element of X holds (x\y)\(y\x ) in BCK-part(X); theorem :: BCIALG_1:75 X is quasi-associative iff for x,y,z being Element of X holds (x\y)\z <=x\(y\z); begin :: Several Classes of BCI-algebra----alternative BCI-algebra theorem :: BCIALG_1:76 X is alternative implies x` = x & x\(x\y) = y & (x\y)\y = x; theorem :: BCIALG_1:77 X is alternative & x\a=x\b implies a=b; theorem :: BCIALG_1:78 X is alternative & a\x=b\x implies a=b; theorem :: BCIALG_1:79 X is alternative & x\y=0.X implies x=y; theorem :: BCIALG_1:80 X is alternative & (x\a)\b = 0.X implies a=x\b & b=x\a; registration cluster alternative -> associative for BCI-algebra; cluster associative -> alternative for BCI-algebra; cluster alternative -> implicative for BCI-algebra; end; theorem :: BCIALG_1:81 X is alternative implies (x\(x\y))\(y\x) = x; theorem :: BCIALG_1:82 X is alternative implies y\(y\(x\(x\y))) = y; begin registration cluster associative -> weakly-positive-implicative for BCI-algebra; cluster p-Semisimple -> weakly-positive-implicative for BCI-algebra; end; theorem :: BCIALG_1:83 for X being non empty BCIStr_0 holds (X is implicative BCI-algebra iff for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x &(x\(x\y)) \(y\x)=y\(y\x) ); theorem :: BCIALG_1:84 X is weakly-positive-implicative iff for x,y being Element of X holds x\y=((x\y)\y)\y`; registration cluster positive-implicative -> weakly-positive-implicative for BCI-algebra; cluster alternative -> weakly-positive-implicative for BCI-algebra; end; theorem :: BCIALG_1:85 X is weakly-positive-implicative BCI-algebra implies for x,y being Element of X holds (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y); theorem :: BCIALG_1:86 for X being non empty BCIStr_0 holds (X is positive-implicative BCI-algebra iff for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\ 0.X=x & x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y) );