Residuation Theory and Substructural Logics

Hiroakira Ono

                             ono@jaist.ac.jp

School of Information Science, JAIST

1 Introduction

For these years, the author has been working at an algebraic study of substructural logics, in particular of logics over FL_{ew} ( see e.g. [6] ). Here, by FL_{ew} we mean the logic obtained from the intuitionistic logic by deleting the contraction rule, if it is formulated as a sequent system. The corresponding algebraic structures are residuated lattices. An important aspect of algebraic study of these logics will come from the fact that algebraic methods enable us to discuss various logics and related algebraic structures within a uniform framework. For instance, by discussing algebraic structures for Łukasiewicz’s many-valued logics and also for fuzzy logics together with hoops and pocrims from universal algebra, it becomes possible to see strong interrelations behind them.

In this paper, we will show the importance of the notion of residuation in the study of substructural logics, and thus residuated structures based on residuation theory offer us algebraic structures which are suitable for substructural logics.

A part of the content of the present paper was presented also at University of Torino, September, 2000. After this, T. Kowalski informed me of the Ph.D thesis [3] by K. Blount and of a book on residuation theory [4] by T.S. Blyth and M.F. Janowitz. Then the author has realized that roles played by the residuation in substructural logics can be stated more explicitly by the help of residuation theory.

2 Residuated maps

In this section, we will give a brief survey of basic facts in residuation theory. For more information, see e.g. [4]. See also [3].

Let P and Q be posets. A map f: P → Q is residuated if there exists a map f^{∗}: Q → P such that the following holds for any p ∈ P and any q ∈ Q:

f(p) ≤ q ⟺ p ≤ f^{∗}(q).

In the above case, we say that f and f^{∗} form a residuated pair, ( or, an adjunction in category theory ) and that f^{∗} is a residual of f. We can show the following results.

Lemma 2.1 If f and f^{∗} form a residuated pair, both f and f^{∗} are monotone increasing.

Lemma 2.2 Maps f: P → Q and f^{∗}: Q → P form a residuated pair if and only if both id_{P} ≤ f^{∗} ∘ f and f ∘ f^{∗} ≤ id_{Q} hold.

Lemma 2.3 If a map f is residuated then its residual is determined uniquely by f.

Hereafter, f^{∗} denotes the residual of a map f when f is residuated. Similarly to Lemma 2.3, we can show that f is determined uniquely by f^{∗} when f and f^{∗} form a residuated pair. In fact, the following holds;

1. f^{∗}(q) = max{p ∈ P; f(p) ≤ q},

2. f(p) = min{q ∈ Q; p ≤ f^{∗}(q)}.

Proposition 2.4 Suppose that f and f^{∗} form a residuated pair between P and Q, and that X ⊆ P and Y ⊆ Q. If sup X exists then sup f(X) ( = sup{f(p); p ∈ X} ) exists and f(sup X) = sup f(X). Also if inf Y exists then inf f^{∗}(Y) exists and f^{∗}(inf Y) = inf f^{∗}(Y).

When both P and Q are lattices in the above proposition, we have the following.

Corollary 2.5 Suppose that f and f^{∗} form a residuated pair between lattices L and M. Then f(a∪b) = f(a) ∪ f(b) for all a, b ∈ L, and f^{∗}(c ∩ d) = f^{∗}(c) ∩ f^{∗}(d) for all c, d ∈ M.

If both L and M are moreover complete, we have the converse of Proposition 2.4.

Proposition 2.6 Suppose that both L and M are complete lattices and that f is a map from L to M. Then, f is residuated if and only if f preserves all ( possibly infinite ) joins. Dually, a map f^{∗} : M → L is the residual of a map f : L → M if and only if f^{∗} preserves all ( possibly infinite ) meets.

3 Residuated structures

Now we will apply results in the previous section to the case where posets are ordered groupoids. Then, we will discuss particular classes of ordered groupiods which originate from algebras for substructural logics.

A structure G = ⟨G, ·, ≤⟩ is an ordered groupoid if · is a binary operation on a poset ⟨G, ≤⟩ which satisfies the following monotonicity ( see [4] ) :

x ≤ x′ and y ≤ y′ imply x · y ≤ x′ · y′

Only for the simplicity’s sake, we assume moreover the commutativity of · in the rest of this section. For each x ∈ G, define a map f_{x} : G → G by f_{x}(y) = x · y. When f_{x} is residuated for any x ∈ G, we say that the ordered commutative groupoid G is residuated. The residual f^{∗}_{x} of f_{x} is expressed as f^{∗}_{x}(y) = x → y. ( One may call such an operation ·, a fusion, and →, an implication. ) Then, the following must hold:

f_{x}(y) ≤ z ⟺ y ≤ f^{∗}_{x}(z),
i.e. x · y ≤ z ⟺ y ≤ x → z

which is called the law of residuation.

When G has also a lattice structure, we have the following equations by Corollary 2.5: For all a, b, c ∈ G

1. (a ∪ b) · c = (a · c) ∪ (b · c),

2. a → (b ∩ c) = (a → b) ∩ (a → c).

In particular, suppose that G is a Heyting algebra. In this case, ∩ and → form a residuation pair. Thus, the above 1 becomes the distributive law. This gives the well-known fact that any Heyting algebra is distributive. Similarly, when G is a complete lattice, by using Proposition 2.6 we have the following.

1. (⋃_{i} a_{i}) · c = ⋃_{i}(a_{i} · c),

2. a → (⋂_{i} c_{i}) = ⋂_{i}(a → c_{i}).

There are many residuated structures related to logic and universal algebra. We have already mentioned Heyting algebras in the above. A pocrim is a ( partially ) ordered commutative residuated groupoid which is also an integral monoid, i.e. a monoid whose unit is the greatest element. If a pocrim has moreover a lattice structure, it is called a residuated lattice. Pocrims and residuated lattices are algebraic structures for ( the implication-fusion fragment ) of logics without contraction rule ( more precisely, logics over FL_{ew} ). See e.g. [2, 6] for the details. Note here that in the definition of “residuated lattices” in [3] neither the commutativity nor the integrality are assumed and therefore they are related to extensions of Lambek calculus.

In the folllowing, we will take two more examples of residuated structures from logic.

1. Commutative quantales A structure A = ⟨A, ∩, ∪, ·⟩ is a commutative quantale if

1. ⟨A, ∩, ∪⟩ is a complete lattice ( and hence is bounded ),

2. ⟨A, ·⟩ is a commutative semigroup,

3. (⋃_{i} x_{i}) · y = ⋃_{i}(x_{i} · y) for x_{i}, y ∈ A.

By Proposition 2.6, A is residuated. If ⟨A, ·⟩ has moreover the unit element, A becomes an intuitionistic phase structure. See [5].

2. Triangular norms in fuzzy logic A triangular norm ( or, simply, a t-norm ) T is a map from [0, 1]^{2} to [0, 1] which satisfies the following conditions:

1. T (x, T (y, z)) = T (T (x, y), z),

2. T (x, y) = T (y, x),

3. T (x, 1) = x,

4. x ≤ y implies T (x, z) ≤ T (y, z).

Define ∗ by x ∗ y = T (x, y). The above conditions mean that ⟨[0, 1], ∗, 1⟩ is a partially-ordered commutative integral monoid. It is obvious that ⟨[0, 1], min, max, 0, 1⟩ forms a complete lattice. Typical examples of t-norms are min{x, y} ( Heyting ), x × y ( product ) and max{x + y − 1, 0} ( Łukasiewicz ).

Now, a question is when the above structure becomes residuated. By Proposition 2.6, it is residuated if and only if

T (⋃_{i} x_{i}, y) = ⋃_{i} T (x_{i}, y).

This condition is equivalent to the following. For x, y

T (x, y) = lim_{z→x−0} T (z, y),

i.e. T is left-continuous. Note that any of t-norms given above is left-continuous.

Thus, we can say that every left-continuous t-norm determines a residuated lattice and therefore determines a substructural logic over FL_{ew}.

4 Concluding remark: why and how far the framework of substructural logics works well

Ten years have passed after a study of nonclassical logics under the name “substructural logics” started. The study seems to be quite promising, as so many different kinds of nonclassical logics introduced so far can be discussed within this framework. On the other hand, it seems to be not clear yet why it works so well, or more precisely why restrictions on “structural rules” play key roles in it. Here we will give an explanation of it by using the notion of residuation.

One will agree that the “implication” is the most important logical connective. At the same time, it is not so easy to analyze its functions and meanings from both mathematical and philosophical points of view. Suppose here that our implication satisfies the following relation in a sequent system of a given logic L under consideration:

⊢ Γ, A ⟹ B if and only if ⊢ Γ ⟹ A → B,

where ⊢ means the provability in the logic L. The above relation holds when we have both introduction rule and elimination rule for →. Now, we introduce a new logical connective ∗, called fusion, to represent commas ( in the left-hand side ) of sequents. Then, the above relation means that implication is the residual of fusion. From the mathematical point of view, fusion may be much more manageable than implication. In such a case, we can shift our attention from implication to fusion, since residuation theory tells us that each fusion determines uniquely an implication and vice versa.

It is easy to see that some of basic properties of fusions ( as groupoid operations ) can be expressed by structural rules. For example, the commutativity of fusions is expressed by exchange rules. This might be the main but hidden reason why the study of substructural logics has begun with restrictions on structural rules.

So our conclusion is that the essense of substructural logics comes from residuation between fusion and implication, rather than from their structural rules.

Of course, the above explanation may oversimplifies the problem. For example, it is not clear for a given implicational logic whether or not it is possible to introduce fusion as a new connective, whose residual is exactly a given implication. As an example, consider the logic BCK. In this case, an appropriate fusion can be introduced. In fact, this is proved either by using the cut elimination theorem of a sequent system of BCK with the fusion, or by showing the embedding theorem of BCK-algebras into BCK-algebras with the fusion ( see e.g. [2, 7] for the latter ). In order to apply residuation theory, we need to make sure of the existence of such a fusion. But, we cannot assume this always. For instance, in [1] authors introduce the “basic logic” B and consider its extensions without the deductive face, i.e. logics in which the law of residuation does not hold. In algebraic terms, each algebraic structure for B is a ( partially ) ordered commutative monoid but without assuming the law of residuation. It might be necessary here to consider once again what is a proper definition of substructural logics.

References

[1] Battilotti, G. and G. Sambin, Basic logic and the cube of its extensions, draft, 1995.

[2] Blok, W.J. and J.G. Raftery, On the quasivariety of BCK-algebras and its subvarieties, Algebra Univerisalis 33, (1995) pp.68-90.

[3] Blount, K., On the structure of residuated lattice, Ph. D. thesis, Vanderbilt University, 1999.

[4] Blyth, T.S. and M.F. Janowitz, Residuation Theory, Pergamon Press, 1972.

[5] Ono, H., Semantics for substructural logics, Substructural Logics, eds. by K. Došen and P. Schroeder-Heister, Studies in Logic and Computation 2, Oxford University Press 1993, pp.259-291.

[6] Ono, H., Logics without contraction rule and residuated lattices I, to appear.

[7] Ono, H. and Y. Komori, Logics without the contraction rule, Journal of Symbolic Logic 50 (1985) pp.169-201.