A Gentzen system and decidability for residuated lattices

Peter Jipsen

May 27, 2000

Abstract

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₁s₂¼s_n |- t is that the inclusion s₁*s₂*¼*s_n £ t holds in RL. The empty sequence e is interpreted as the multiplicative unit 1. Using this notation, we list below some quasi-inclusions s₁ £ t₁ & ¼& s_n £ t_nÞs £ t in the style of Gentzen rules:

s1 |- t1 ¼ sn |- tn s |- t name of rule.

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

t |- t  Id       gd |- u g1 d |- u  1-left       e |- 1  1-right

gs td |- u gs*t d |- u  *left       g |- s   d |- t gd |- s*t  *right

s |- s   gtd |- u gss\td |- u  \left       sg |- t g |- s\t  \right

s |- s   gtd |- u gst/sd |- u  /left       gs |- t g |- t/s  /right

gsd |- u   gtd |- u gsÚ td |- u Úleft       g |- s g |- sÚt Úright1       g |- t g |- sÚt Úright2

gsd |- u gsÙ td |- u Ùleft1       gtd |- u gsÙ td |- u Ùleft2       g |- s   g |- t g |- sÙt Ùright

A proof-tree is a tree in which each node is a sequent, and if s₁ |- t₁,..., s_n |- t_n are all the child nodes of node s |- t, then n Î {0,1,2} and the rule [(s₁ |- t₁ ¼ 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 1-right. A sequent is said to be provable¹ if there exists a proof-tree with this sequent as the root. A subtree of a proof-tree is again a proof-tree, hence all the nodes in a proof-tree 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 proof-tree 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

x*(yÚz) |- x*yÚx*z and x\(yÙz) |- x\yÙx\z

are provable, whereas xÙ(yÚz) |- (xÙy)Ú(xÙz) is not. For lattice theorists it is also interesting to note that the 6 rules for Ú and Ù are essentially equivalent to Whitman's method for deciding if s £ t holds in all lattices, where s,t are lattice terms, and g,d in the rules are taken to be empty sequences. A different method for deciding lattice inclusions, due to Skolem, is described by Burris in [].

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 quasi-inclusions) in RL. The reverse implication is completeness, which is proved by defining a semantics for residuated lattices, based on a non-commutative 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 non-commutative 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

(P1) L is closed under arbitrary intersections and
(P2) for all X Í M, Y Î L we have X\Y and Y/X Î L,

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

XC = Ç {Z Î L:X Í Z}    the closure of X

XÚY = (XÈY)C       XÙY = XÇY       X*Y = (XY)C    1 = {e}C

Lemma 1 For any non-commutative 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

XYC Í X(X\(XY)C)C = X(X\(X*Y)) Í X*Y

where the middle equality makes use of the fact that X\(XY)^C is closed by (P2). Similarly X^CY Í X*Y, hence X^CY^C Í X^C*Y = (X^CY)^C Í (X*Y)^C = X*Y. Since we also have XY Í X^CY^C, it follows that (XY)^C = (X^CY^C)^C. Now (X*Y)*Z=((XY)^CZ)^C=((XY)^C^CZ^C)^C=((XY)Z)^C
=(X(YZ))^C=(X^C(YZ)^C)^C=X*(Y*Z), and 1*X = ({e}^CX)^C = ({e}^CCX^C)^C = ({e}X)^C = X^C = X for X Î L.

In logic it is common to refer to a structure with an assignment as a model. Let X be a set of variables. A non-commutative phase model M = (M,L,h) is a non-commutative 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

[g_d |- u] = {s Î M(p):gsd |- u is provable}.

The notation [u] is shorthand for [e_e |- u], called the value of u. Further let L_0={[_u]:, M(p), u S(p)}
L(p)={ K: K L_0}
h(x)=[x]  for any variable x in p.

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 non-commutative 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

s Î X\Y iffs Î Ç {[gr_d |- u]:r Î X and Y Í [g_d |- u]},

which implies that X\Y Î L, and Y/X is similar.

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₁ 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₁ 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 1-left rule 1 Î [g_d |- u]. Hence (*) implies 1 Î h(1). Finally, h(1) Í [1] holds since {e} Í [1] follows from 1-right.

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:

1. RL\models 1 £ p
2. e Î h(p) in M(p)
3. e |- p is provable.

(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 (quasi-inclusions 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 non-commutative 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.

References

[]

S. Burris, Polynomial time uniform word problems Math. Logic Quarterly 41 (1995), 173-182.

[]

M. Okada and K. Terui, The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic, 64(2) (1999) 790-802.

Footnotes:

¹In the literature on Gentzen systems this corresponds to cut-free provable since the Gentzen system presented here does not mention the so-called cut-rule [(s |- t   \gammatd |- u)/(gsd |- u)].