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