MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Equational definition of Residuated Lattices

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)?

-
It's not terribly messy but it doesn't look useful to do that. What is your motivation? (Since the principal reason why these are of interest is that / and \ are the two adjoints of •, it doesn't seem advised to obscure that fact.) – François G. Dorais Mar 5 2010 at 23:10
It would be nice when doing formalized reasoning about algebraic structures to have one presentation that is both obviously (aka syntactically) a variety and simultaneously is a reasonable set of axioms to reason from. My alternative is two create two presentations and prove they are equivalent. That wouldn't be so bad, but it would be nicer if I could get it all in one. – Russell O'Connor Mar 8 2010 at 15:20

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.

-