Question

The usual axiomatization of residuated lattices involve using ≤. I know I can expand away the use of ≤ using a definition such as (x ≤ y) := (x ∧ y = x), but I fear I will get a set of messy axioms.

What is a nice equational axiomatization of residuated lattices for the signature (U, ∧, ∨, •, e, /, \) (or any other signature if you prefer)?

Answer 1

If by "the usual axiomatization" you mean the implications,

$x/y \leq z \Leftrightarrow x \leq zy \quad$ and $\quad x\backslash y \leq z \Leftrightarrow y\leq xz,$

and if you mean you want an axiomatization that does not involve implications, then I believe the following theorem, due to Blount, Jipsen, and Tsinakis, answers your question:

Theorem. An algebra is a residuated lattice if and only if it satisfies the equations defining lattices, the equations defining monoids, and the following four equations:

1. $x(x\backslash z\wedge y) \leq z$,
2. $(y\wedge z/x)x \leq z$,
3. $y \leq x\backslash (xy\vee z)$,
4. $y \leq (z\vee yx)/x$.

Thus the class of residuated lattices does form an equational class. (If you don't like the appearances of $\leq$, then, as you say, you can replace them using an extra meet operation.)

This version of the theorem appears in Galatos, Jipsen, Kowalski, Ono MR2531579, page 94.