Compare the decidability of residuated lattices with two important
results about l-groups:
Theorem (C. Holland and S.H. McCleary 1979):
The variety of l-groups has a decidable
Theorem (A.M.W. Glass and Y. Gurevich 1983):
The (local) word problem for l-groups is undecidable,
i.e. there exists a finitely presented l-group
(with one relator) for which there is no algorithm that
decides if two words are representatives of the same
The quasi-equational theory of l-groups is undecidable.
This is also refered to as the undecidability of the global
(or uniform) word problem.
The same theorem holds for semigroups
(E. Post ~'40) and groups (Novikov, W. Boone 1959)
Theorem (N. G. Khisamiew 1966): The universal theory
of abelian l-groups is decidable.
If a class is closed under finite products, then any universal
formula is equivalent to a finite number of
disjunction of quasi-identities
and negated equations.
Hence such a class has a decidable universal theory iff it has
a decidable quasi-equational theory.
Theorem (V. Weispfenning 1986): The universal theory of
abelian l-groups is co-NP-complete.
Theorem (Y. Gurevich 1967): The first-order theory of
abelian l-groups is hereditarily undecidable. (S. Burris
1985 gives a short proof).
What about the quasi-equational theory of residuated