The variety of residuated lattices is denoted by RL. An algebra (L,Ú,Ù,*,\,/,1) is a member of this variety if (L,Ú,Ù) is a lattice, (L,*,1) is a monoid, and x*y £ z iff y £ x\z iff x £ z/y for all x,y,z Î L (these equivalences can be expressed by equations). We use s,t,u for terms in the language of RL, and g,d,r,s for (finite) sequences of terms. Concatenation of sequences g and d is denoted by gd, and terms are considered as sequences of length 1. (In this note, multiplication in RL is written explicitly as s*t.) A pair (s,t) is called a sequent and is written s  t. The symbol  is read as yields, and the semantic interpretation of s_{1}s_{2}¼s_{n}  t is that the inclusion s_{1}*s_{2}*¼*s_{n} £ t holds in RL. The empty sequence e is interpreted as the multiplicative unit 1. Using this notation, we list below some quasiinclusions s_{1} £ t_{1} & ¼& s_{n} £ t_{n}Þs £ t in the style of Gentzen rules:

With the given semantic interpretation it is straight forward to check that all these quasiinclusions hold in RL. The details in the proof of the completeness lemma (Lemma 3 below) justify the specific form of these rules.






A prooftree is a tree in which each node is a sequent, and if s_{1}  t_{1},..., s_{n}  t_{n} are all the child nodes of node s  t, then n Î {0,1,2} and the rule [(s_{1}  t_{1} ¼ s_{n}  t_{n})/(s  t)] matches one of the above rules. Hence each node has at most 2 child nodes, and a sequent can appear at a leaf iff it matches one of the rules Id or 1right. A sequent is said to be provable^{1} if there exists a prooftree with this sequent as the root. A subtree of a prooftree is again a prooftree, hence all the nodes in a prooftree are provable.
Note that for each of the rules, there are only a finite number of ways a given sequent can match the denominator of a rule, and this determines exactly what sequents must appear in the numerator of the rule. In each case the sequents in the numerator are structurally simpler than the sequent in the denominator, so the depth of a prooftree is bounded by the size (defined in a suitable way) of the sequent at the root. Hence it is decidable whether a given sequent is provable.
As an exercise it is instructive to show that sequents such as

We now prove the result of Okada and Terui[] which shows that for terms s,t, the sequent s  t is provable iff the inclusion s £ t holds in RL. The forward implication is the soundness of the proof procedure, and follows from the observation that all the rules are vaild (as quasiinclusions) in RL. The reverse implication is completeness, which is proved by defining a semantics for residuated lattices, based on a noncommutative version of the phase spaces of linear logic. In the theory of quantales, such phase spaces can also be viewed as quantic nuclei of powerset quantales. However the argument below does not require any knowledge of linear logic or quantales.
A noncommutative phase space is of the form (M,L), where M is a monoid (with unit e and x·y written as xy), and L Í P(M) such that
where X\Y = {z Î M:X{z} Í Y}, Y/X = {z Î M:{z}X Í Y} and XY = {xy:x Î X, y Î Y}. We also define


Lemma 1 For any noncommutative phase space (M,L), the algebra (L,Ú,Ù,*,\,/,1) is a residuated lattice.
It is a lattice (in fact a complete lattice) since it is the collection of closed sets of a closure operation. By definition of \ we have Z Í X\Y iff XZ Í Y, and for Y Î L this is equivalent to X*Y = (XY)^{C} Í Y. Similarly, Z Í Y/X is equivalent to Z*X Í Y. It remains to show that * is associative and 1 is an identity.
For all X,Y Í M, XY Í (XY)^{C} implies Y Í X\(XY)^{C}, hence

In logic it is common to refer to a structure with an assignment as a model. Let X be a set of variables. A noncommutative phase model M = (M,L,h) is a noncommutative phase space (M,L) together with an assignment h:X®L. As usual, h extends to a homomorphism from the absolutely free term algebra T(X) to L, with h(1) defined as 1. A term p is satisfied in M if e Î h(p). This is equivalent to h(1) Í h(p), which agrees with the usual algebraic notion of satisfaction for the inclusion 1 £ p under the assignment h. Since s £ t is equivalent to 1 £ s\t, the satisfaction of arbitrary inclusions is captured by this notion.
Given a term p, let S(p) be the set of subterms of p. We now define
a syntactical model M(p) = (M(p),L(p),h). The universe M(p) is
the free monoid generated by S(p), i.e. the set of all finite
sequences of subterms of p. The empty sequence is again denoted by e.
For g,d Î M(p), u Î S(p), define

In the subsequent proofs we will frequently make use of the following observation:
(*) For any X Í M(p), t Î S(p),
t X^C if and only if
for all g,d Î M(p) and u Î S(p), X Í [g_d  u]
implies t Î [g_d  u].
Lemma 2 M(p) is a noncommutative phase model.
(P1) holds by construction. To prove (P2), let X Í M(p) and Y Î L(p).
Now s Î X\Y iff X{s} Í Y iff for all r Î X, rs Î Y = Y^{C}. By (*) this is equivalent to showing that Y Í [g_d  u] implies
rs Î [g_d  u]. This last containment holds iff grsd  u
is proveable iff s Î [gr_d  u]. Hence

The following result is the central part of the completeness argument.
Lemma 3 Let M(p) be defined as above. For any subterm t of p we have t Î h(t) Í [t]. In particular, if e Î h(t) then the sequent e  t is provable.
By induction on the structure of the subterm. If it is a variable of p, say x, then h(x) = [x] by definition, and x Î [x] since x  x is provable (using Id). Suppose s,t are subterms of p, and s Î h(s) Í [s], t Î h(t) Í [t].
sÚt Î h(sÚt) Í [sÚt]: Note that h(sÚt) = (h(s)Èh(t))^{C}. Let g Î h(s)Èh(t). If g Î h(s), then g Î [s], so g  s is provable. By the Úright_{1} rule it follows that g  sÚt is provable, hence g Î [sÚt] and therefore h(s) Í [sÚt]. Similarly h(t) Í [sÚt], and since [sÚt] is closed, h(sÚt) Í [sÚt].
To see that sÚt Î h(sÚt), we use observation (*): Suppose h(s)Èh(t) Í [g_d  u] where g,d Î M(p), u Î S(p). Then gsd  u and gtd  u are provable (since s Î h(s) and t Î h(t)). Therefore gsÚtd  u is provable by Úleft and so sÚt Î [g_d  u]. By (*) we conclude that sÚt Î (h(s)Èh(t))^{C} = h(sÚt).
sÙt Î h(sÙt) Í [sÙt]: Let g Î h(sÙt) = h(s)Çh(t). Then g Î [s]Ç[t], hence g  s and g  t are provable. So now g  sÙt is provable by the Ùright rule, which shows that g Î [sÙt].
Suppose h(s) Í [g_d  u]. Then gsd  u is provable, and by the Ùleft_{1} rule, gsÙtd  u is provable. Therefore sÙt Î [g_d  u], and it follows from (*) that sÙt Î h(s)^{C} = h(s). Similarly sÙt Î h(t), hence sÙt Î h(sÙt).
s*t Î h(s*t) Í [s*t]: Note that h(s*t) = (h(s)h(t))^{C}, and let s Î h(s)h(t). Then s = gd, where g Î h(s) Í [s] and d Î h(t) Í [t]. Therefore g  s and d  t are provable, hence by *right gd  s*t is provable, and so s Î [s*t]. It follows that h(s)h(t) Í [s*t], and since [s*t] is closed, h(s*t) Í [s*t].
Suppose h(s)h(t) Í [g_d  u]. Then st Î [g_d  u] since s Î h(s) and t Î h(t). Thus gstd  u is provable, and by *left, gs*td  u is provable. This implies s*t Î [g_d  u], so by (*), it follows that s*t Î h(s*t).
s\t Î h(s\t) Í [s\t]: Here h(s\t) = h(s)\h(t) = {g Î M(p):h(s){g} Í h(t)}. Thus g Î h(s\t) implies sg Î h(t) Í [t], since we are assuming s Î h(s). This means sg  t is provable, so by \right g Î [s\t].
Suppose h(t) Í [g_d  u], then t Î h(t) implies gtd  u is provable. For any s Î h(s) Í [s] we have that s  s is provable, so from \left we get that ss\t Î [g_d  u]. By (*) it follows that ss\t Î h(t) whenever s Î h(s), hence h(s){s\t} Í h(t). This implies s\t Î h(s)\h(t) = h(s\t).
The case for s/t Î h(s/t) Í [s/t] is similar. Since we are assuming that h has been extended to a homomorphism from the term algebra to L, we have h(1) = 1 = {e}^{C}. Suppose {e} Í [g_d  u], then gd  u is provable, and by the 1left rule 1 Î [g_d  u]. Hence (*) implies 1 Î h(1). Finally, h(1) Í [1] holds since {e} Í [1] follows from 1right.
The second statement is a simple consequence: if e Î h(t) then e Î [t] which means e  t is provable.
Theorem 4 For any term p the following statements are equivalent:
(i) implies (ii) by Lemma 2, (ii) implies (iii) by Lemma 3, and (iii) implies (i) by a standard soundness argument using the observation that all the (quasiinclusions corresponding to) sequent rules are valid in RL.
Since it was observed earlier that condition (iii) is decidable, and since any equation can be reduced to this form, the equational theory of RL is decidable. Okada and Terui[] go on to prove that RL is generated by its finite members, and they also consider several subvarieties and expansions of RL. For example, to decide inclusions for bounded residuated lattices, one simply adds the two rules [/(g0d  u)] and [/(g  T)]. In fact their results are formulated for what amounts to bounded commutative residuated lattices, and the noncommutative case is only mentioned briefly at the end. However their method of proving decidability and the finite model property is very versatile and can perhaps be adapted to cover other subvarieties of RL, such as the varieties of distributive or of cancellative residuated lattices, or the variety generated by residuated chains.
^{1}In the literature on Gentzen systems this corresponds to cutfree provable since the Gentzen system presented here does not mention the socalled cutrule [(s  t \gammatd  u)/(gsd  u)].