Residuated Boolean Algebra

A residuated Boolean algebra is an algebraic structure (L, ∧, ∨, ¬, 0, 1, •, I, \, /) such that

(i) (L, ∧, ∨, •, I, \, /) is a residuated lattice, and

(ii) (L, ∧, ∨, ¬, 0, 1) is a Boolean algebra.

An equivalent signature better suited to the relation algebra application is (L, ∧, ∨, ¬, 0, 1, •, I, ▷, ◁) where the unary operations x\ and x▷ are intertranslatable in the manner of De Morgan's laws via

x\y = ¬(x▷¬y), x▷y = ¬(x\¬y), and dually /y and ◁y as

x/y = ¬(¬x◁y), x◁y = ¬(¬x/y),

with the residuation axioms in the residuated lattice article reorganized accordingly (replacing z by ¬z) to read

(x▷z)∧y = 0 ⇔ (x•y)∧z = 0 ⇔ (z◁y)∧x = 0

This De Morgan dual reformulation is motivated and discussed in more detail in the section below on conjugacy.

Since residuated lattices and Boolean algebras are each definable with finitely many equations, so are residuated Boolean algebras, whence they form a finitely axiomatizable variety.