Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
    
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 '10 at 23:10
1  
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 '10 at 15:20

1 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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.