Lemma: The identities   (x ∨ y)\z = x\z ∧ y\z   and   x/(y ∨ z) = x/y ∧ x/z   hold in any residuated lattice.
Proof:
  w ≤ (x ∨ y)\z  
iff   (x ∨ y)w ≤ z   (since I:   b ≤ a\c  ⇔  a*b ≤ c   )
iff   x ∨ y ≤ z/w   (since II:   a*b ≤ c  ⇔  a ≤ c/b   )
iff   x ≤ z/w  and  y ≤ z/w       (since   x, y ≤ x ∨ y   )
iff   xw ≤ z  and  yw ≤ z   (by II)
iff   w ≤ x\z  and  w ≤ y\z   (by I)
iff   w ≤ x\z ∧ y\z   (since   a ∧ b ≤ a, b   )
hence the first identity holds, and the proof for the second one is the opposite.

Note that this actually uses quasi-equational reasoning rather than equational reasoning from the equational basis.

Lemma: The identities   (x ∧ y)\z = x\z ∨ y\z   and   x/(y ∧ z) = x/y ∨ x/z   hold in any l-group.
Proof:   (x ∧ y)\z = (x ∧ y)-1z = (x-1 ∨ y-1)z = x-1z ∨ y-1z = x\z ∨ 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.)

So   x ∧ y ≤ x   implies   (x ∧ y)\z ≥ x\z,

hence   (x ∧ y)\z ≥ x\z ∨ y\z   holds in all residuated lattices.

If   x   and   y   are comparable, say   x ≤ y, then   x ∧ y = x   and   y\z ≤ x\z  

so   (x ∧ y)\z = x\z = x\z ∨ y\z.

Hence the two identities hold in all residuated chains.

Is there a procedure that we can apply to find out if they hold in general? Click here

 

 

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 equational theory.
Proof: Click here

Next