Self-cancellative residuated lattices

A residuated lattice is defined to be self-cancellative if it satisfies the equations x\x = e and x/x = e. Every integral, cancellative, or divisible residuated lattice is self-cancellative, and, conversely, every bounded self-cancellative residuated lattice is integral. It is proved that the mapping a -> (a\e)\e on any self-cancellative residuated lattice is a homomorphism onto a lattice-ordered group. A Glivenko-style property is then established for varieties of self-cancellative residuated lattices with respect to varieties of lattice-ordered groups, showing in particular that self-cancellative residuated lattices form the largest variety of residuated lattices admitting this property with respect to lattice-ordered groups. The Glivenko property is used to obtain a sequent calculus admitting cut-elimination for the variety of self-cancellative residuated lattices and to establish the decidability, indeed PSPACE-completenes, of its equational theory. Finally, these results are related to previous work on (pseudo) BCI-algebras, semi-integral residuated partially ordered monoids, and algebras for Casari's comparative logic.