BCI-algebras

A BCI-algebra is a structure A = (A,·,0) of type (2,0) such that

(1): ((x·y)·(x·z))·(z·y) = 0,
(2): (x·(x·y))·y = 0,
(3): x·x = 0,
(4): x·y = y·x = 0 ⇒ x = y, and
(5): x·0 = 0 ⇒ x = 0.

Remark:

Let A and B be BCI-algebras. A morphism from A to B is a function h : A→B that is a homomorphism: h(x·y) = h(x)·h(y) and h(0) = 0.

Classtype	Quasivariety
Equational theory
Quasiequational theory
First-order theory
Locally finite	No
Residual size
Congruence distributive	No
Congruence modular	No
Congruence n-permutable	No
Congruence regular	No
Congruence uniform	No
Congruence extension property	No
Definable principal congruences
Equationally definable principal congruences
Amalgamation property
Strong amalgamation property
Epimorphisms are surjective

[Size 1]?: 1
[Size 2]?:
[Size 3]?:
[Size 4]?:
[Size 5]?:
[Size 6]?: