Note that this actually uses quasi-equational reasoning rather
than equational reasoning from the equational basis.
Lemma: The identities `(x ^^ y)\z=x\z vv y\z` and
`x/(y ^^ z)=x/y vv x/z` hold in any l-group.
Proof: `((x ^^ y)\z=(x ^^ y)^-1.z)=(x^-1 vv y^-1).z=x^-1.z vv y^-1.z
=x\z vv y\z`, and the second identity follows similarly.
So: Does every residuated lattice satisfy these two identities?
Note that `\` is order-reversing in the first argument. (This follows
from the first lemma.)
hence `(x^^y)\z>=x\z vv y\z` holds in all
If `x` and `y` are comparable, say `x<=y`, then `x^^y=x` and `y\z<=x\z`
`(x^^y)\z=x\z=x\z vv y\z`.
Hence the two identities hold in all
Is there a procedure that we can apply to find out if they hold
A class K of universal algebras has a
decidable equational theory
if there is an algorithm that takes any identity as input and
determines if it holds in all members of K.
For a (quasi-) variety K
this is equivalent to the word problem
for the free algebras of K: determine if
two words (elements of the absolutely free algebra) are
representatives of the same equivalence class.
Theorem: The variety of residuated lattices has a decidable
Proof: Click here