Brouwerian algebras
A Brouwerian algebra is a structure A = (A, ∨, ∧, 1, →) such that
(A, ∨, ∧, 1) is a distributive lattice
with top, and
→ gives the residual of ∧: x∧y ≤ z ⇔ y ≤ x→z.
Let A and B be Brouwerian 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(x∧y) = h(x)∧h(y) and h(1) = 1 and h(x→y) = h(x)→h(y).
A Brouwerian algebra is a BL-algebra A = (A, ∨, ∧, 1, ·, →) such that x∧y = x·y.
| Equational theory | decidable |
| Quasiequational theory | decidable |
| First-order theory | undecidable |
| Locally finite | no |
| Residual size | unbounded |
| Congruence distributive | yes |
| Congruence modular | yes |
| Congruence n-permutable | yes, n = 2 |
| Congruence e-regular | yes, e = 1 |
| Congruence uniform | no |
| Congruence extension property | yes |
| Definable principal congruences | yes |
| Equationally definable principal congruences | yes |
| Amalgamation property | yes |
| Strong amalgamation property | yes |
| Epimorphisms are surjective | yes |