Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Substructural Logics

First published Tue Jul 4, 2000; substantive revision Wed Jan 16, 2008

Substructural logics are non-classical logics weaker than classical logic, notable for the absence of structural rules present in classical logic. These logics are motivated by considerations from philosophy (relevant logics), linguistics (the Lambek calculus) and computing (linear logic). In addition, techniques from substructural logics are useful in the study of traditional logics such as classical and intuitionistic logic. This article provides a brief overview of the field of substructural logic. For a more detailed introduction, complete with theorems, proofs and examples, the reader can consult the books and articles in the Bibliography.

1. Residuation

Logic is about logical consequence. As a result, the conditional is a central notion in logic because of its intimate connection with logical consequence. This connection is neatly expressed in residuation condition:

p, q ⊢ r   if and only if   p ⊢ q → r

It says that r follows from p together with q just when q → r follows from p alone. The validity of the transition from q to r (given p) is recorded by the conditional q → r.

This connection between the conditional and consequence is called residuation by analogy with the case in mathematics. Consider the connection between addition and substraction. a + b = c if and only if a = c − b. The resulting a (which is c − b) is the residual, what is left of c when b is taken away. Another name for this connection is the deduction theorem.

However, there the connection between consequence and the conditional contains one extra factor. Not only is there the turnstile, for logical consequence, and the conditional, encoding consequence inside the language of propositions, there is also the comma, indicating the combination of premises. We have read “p, q ⊢ r” as “r follows from p together with q”. To combine premises is to have a way to take them together. But how can we take them together? It turns out that there are different ways to do so, and so, different substructural logics. The behaviour of premise combination varies as the behaviour of the conditional varies. In this introduction we will consider some examples of this.

1.1 Weakening

It is one thing for p to be true. It is another for the conditional q → p to be true. Yet, if ‘→’ is a material conditional, q → p follows from p. For many different reasons, we may wish to understand how a conditional might work in the absence of this inference. This is tied to the behaviour of premise combination, as can be shown by this demonstration.

p ⊢ p
p, q ⊢ p
p ⊢ q → p

From the axiomatic p ⊢ p (anything follows from itself) we deduce that p follows from p together with q, and then by residuation, p ⊢ q → p. If we wish to reject the inference from p to q → p, then we either reject residuation, or reject the identity axiom at the start of the proof, or we reject the first step of the proof. It is illuminating to consider what is involved in this last option. Here, we are to deny that p follows from p, q. In general, we are to reject the inference rule that has this form:

X ⊢ A
X, Y ⊢ A

This is called the rule of weakening. The rule steps from a stronger statement, that A follows from X to a possibly weaker one, that A follows from X together with Y.

People have offered different reasons for rejecting the rule of weakening, depending on the interpretation of consequence and premise combination. One of the early motivating examples comes from a concern for relevance. If the logic is relevant (if to say that p entails q is true is to say, at least, that q truly depends on p) then the comma need not not satisfy weakening. We may indeed have A following from X, without A following from X,Y, for it need not be the case that A depends on X and Y together.

In relevant logics the rule of weakening fails on the other side too, in that we wish this argument to be invalid too:

q ⊢ q
p, q ⊢ q
p ⊢ q → q

Again, q may follow from q, but this does not mean that it follows from p together with q, provided that “together with” is meant in an appropriately strong sense. So, in relevant logics, the inference from an arbitrary premise to a logical truth such as q → q may well fail.

1.2 Commutativity

If the mode of premise combination is commutative (if anything which follows from X, Y also follows from Y, X) then we can reason as follows, using just the identity axiom and residuation:

p → q ⊢ p → q
p → q, p ⊢ q
p, p → q ⊢ q
p ⊢ (p → q) → q

In the absence of commutativity of premise combination, this proof is not available. This is another simple example of the connection between the behaviour of premise combination and that of deductions involving the conditional.

There are many kinds of conditional for which this inference fails. If “→” has modal force (if it expresses a kind of entailment, in which p → q is true when in every related circumstance in which p holds, q does too), and if “⊢” expresses local consequence (p⊢q if and only if any model, at any circumstance at which p holds, so does q) it fails. It may be true that Greg is a logician (p) and it is true that Greg’s being a logician entails Greg’s being a philosopher (p → q – in related circunstances in which Greg is a logician, he is a philosopher) but this does not entail that Greg is a philosopher. (There are many circumstances in which the entailment (p → q) is true but q is not.) So we a circumstance in which p is true but (p → q) → q is not. The argument is invalid.

This counterexample can also be understood in terms of behaviour of premise combination. Here when we say X,A ⊢ B is true, we are not just saying that B holds in any circumstance in which X and A both hold. If we are after a genuine entailment A → B, then we want B to be true in any (related) circumstance in which A is true. So, X,A ⊢ B says that in any possibility in which A is true, so is B. These possibilities might not satisfy all of X. (In classical theories of entailment, the possibilities are those in which all that is taken as necessary in X are true.)

If premise combination is not commutative, then residuation can go in two ways. In addition to the residuation condition giving the behaviour of →, we may wish to define a new arrow ← as follows:

p, q ⊢ r  if and only if  q ⊢ r ← p

For the left-to-right arrow we have modus ponens in this direction:

p → q, p ⊢ q

For the right-to-left arrow, modus ponens is provable with the premises in the opposite order:

p, q ← p ⊢ q

This is a characteristic of substructural logics. When we pay attention to what happens when we don't have the full complement of structural rules, then new possibilities open up. We uncover two conditionals underneath what was previously one (in intuitionistic or classical logic).

In the next section we will see another example motivating non-commutative premise combination and these two different conditionals.

1.3 Associativity

Here is another way that structural rules influence proof. The associativity of premise combination provides the following proof:

p → q, p ⊢ q     r → p, r ⊢ p
p → q, (r → p, r) ⊢ q
(p → q, r → p), r ⊢ q
p → q, r → p ⊢ r → q
p → q ⊢ (r → p) → (r → q)

This proof uses the cut rule at the topmost step. The idea is that inferences can be combined. If X ⊢ A and Y(A) ⊢ B (where Y(A) is a structure of premises possibly including A one or more times) then Y(X) ⊢ B too (where Y(X) is that structure of premises with those instances of A replaced by X). In this proof, we replace the p in p → q, p ⊢ q by r → p, r on the basis of the validity of r → p, r ⊢ p.

1.4 Contraction

A final important example is the rule of contraction which dictates how premises may be reused. Contraction is crucial in the inference of p → q from p → (p → q)

p → (p → q) ⊢ p → (p → q)       p → q ⊢ p → q
p → (p → q), p ⊢ p →q       p → q, p ⊢ q
  (p → (p → q), p), p ⊢ q  
  p → (p → q), p ⊢ q  
  p → (p → q) ⊢ p → q  

These different examples give you a taste of what can be done by structural rules. Not only do structural rules influence the conditional, but they also have their effects on other connectives, such as conjunction and disjunction (as we shall see below) and negation (Dunn 1993; Restall 2000).

1.5 Structure on the right of the turnstile

Since the introduction of Gentzen’s sequent calculus (Gentzen 1935), we have known that the difference between classical logic and intuitionistic logic can also be understood as a difference of structural rules. Instead of considering sequents of the form X ⊢ A, in which we have a collection of antecedents and a single consequent, for classical logic it is fruitful to consider sequents of the form

X ⊢ Y

where both X and Y are collections of statements. The intended interpretation is that from all of the X it follows that some of the Y. In other words, we cannot have all of the X and none of the Y obtaining.

Allowing sequents with multiple consequents and translating the rules into this expanded context, we are able to derive classical tautologies. For example, the derivation

p ⊢ p
p ⊢ q, p
⊢ p → q, p

shows that either p → q or p must hold. This is classically valid (if p fails, p is false, and conditionals with false antecedents are true), but invalid in intuitionistic logic. The difference between classical and intuitionistic logic, then, can be understood formally as a difference between the kinds of structural rules permitted, and the kinds of structures appropriate to use in the analysis of logical consequence.

2. Logics in the Family

There are many different formal systems in the family of substructural logics. These logics can be motivated in different ways.

2.1 Relevant Logics

Many people have wanted to give an account of logical validity which pays some attention to conditions of relevance. If X,A ⊢ B holds, then X must somehow be relevant to A. Premise combination is restricted in the following way. We may have X ⊢ A without also having X,Y ⊢ A . The new material Y might not be relevant to the deduction. In the 1950s, Moh (1950), Church (1951) and Ackermann (1956) all gave accounts of what a ‘relevant’ logic could be. The ideas have been developed by a stream of workers centred around Anderson and Belnap, their students Dunn and Meyer, and many others. The canonical references for the area are Anderson, Belnap and Dunn’s two-volume Entailment (1975 and 1992). Other introductions can be found in Read’s Relevant Logic, Dunn and Restall’s “Relevance Logic” (2002), and Mares’ Relevant Logic: a philosophical interpretation (2004).

2.2 Resource Consciousness

This is not the only way to restrict premise combination. Girard (1987) introduced linear logic as a model for processes and resource use. The idea in this account of deduction is that resources must be used (so premise combination satisfies the relevance criterion) and they do not extend indefinitely. Premises cannot be re-used. So, I might have X,X ⊢ A, which says that I can use X twice to get A. I might not have X ⊢ A, which says that I can use X once alone to get A. A helpful introduction to linear logic is given in Troelstra’s Lectures on Linear Logic (1992). There are other formal logics in which the contraction rule (from X,X ⊢ A to X ⊢ A) is absent. Most famous among these are Łukasiewicz’s many-valued logics. There has been a sustained interest in logics without this rule because of Curry's paradox (Curry 1977, Geach 1995; see also Restall 1994 in Other Internet Resources).

3. Order

Independently of either of these traditions, Joachim Lambek considered mathematical models of language and syntax (Lambek 1958, 1961). The idea here is that premise combination corresponds to composition of strings or other linguistic units. Here X,X differs in content from X, but in addition, X,Y differs from Y,X. Not only does the number of premises used count but so does their order. Good introductions to the Lambek calculus (also called categorial grammar) can be found in books by Moortgat (1988) and Morrill (1994).

3. Proof Systems

We have already seen a fragment of one way to present substructural logics, in terms of proofs. We have used the residuation condition, which can be understood as including two rules for the conditional, one to introduce a conditional

X, A ⊢ B
X ⊢ A → B

and another to eliminate it.

X ⊢ A → B        Y ⊢ A
X, Y ⊢ B

Rules like these form the cornerstone of a natural deduction system, and these systems are available for the wide sweep of substructural logics. But proof theory can be done in other ways. Gentzen systems operate not by introducing and eliminating connectives, but by introducing them both on the left and the right of the turnstile of logical consequence. We keep the introduction rule above, and replace the elimination rule by one introducing the conditional on the left:

X ⊢ A        Y(B) ⊢ C
Y(A → B, X) ⊢ C

This rule is more complex, but it has the same effect as the arrow elimination rule: It says that if X suffices for A, and if you use B (in some context Y) to prove C then you could just as well have used A → B together with X (in that same context Y) to prove C, since A → B together with X gives you B.

Gentzen systems, with their introduction rules on the left and the right, have very special properties which are useful in studying logics. Since connectives are always introduced in a proof (read from top to bottom) proofs never lose structure. If a connective does not appear in the conclusion of a proof, it will not appear in the proof at all, since connectives cannot be eliminated.

In certain substructural logics, such as linear logic and the Lambek calculus, and in the fragment of the relevant logic R without disjunction, a Gentzen system can be used to show that the logic is decidable, in that an algorithm can be found to determine whether or not an argument X ⊢ A is valid. This is done by searching for proofs of X ⊢ A in a Gentzen system. Since premises of this conclusion must feature no language not in this conclusion, and they have no greater complexity (in these systems), there are only a finite number of possible premises. An algorithm can check if these satisfy the rules of the system, and proceed to look for premises for these, or to quit if we hit an axiom. In this way, decidability of some substructural logics is assured.

However, not all substructural logics are decidable in this sense. Most famously, the relevant logic R is not decidable. This is partly because its proof theory is more complex than that of other substructural logics. R differs from linear logic and the Lambek calculus in having a straightforward treatment of conjunction and disjunction. In particular, conjunction and disjunction satisfy the rule of distribution:

p & (q ∨ r) ⊢ (p & q) ∨ (p & r)

The natural proof of distribution in any proof system uses both weakening and contraction, so it is not available in the relevant logic R, which does not contain weakening. As a result, proof theories for R either contain distribution as a primitive rule, or contain a second form of premise combination (so called extensional combination, as opposed to the intensional premise combination we have seen) which satisfies weakening and contraction.

In recent years, a great deal of work has been done on the proof theory of classical logic, inspired and informed by research into substructural logics. Classical logic has the full complement of structural rules, and is historically prior to more recent systems of substructural logics. However, when it comes to attempting to understand the deep structure of classical proof systems (and in particular, when two derivations that differ in some superficial syntactic way are really different ways to represent the one underlying ‘proof’) it is enlightening to think of classical logic as formed by a basic substructural logic, in which extra structural rules are imposed as additions. In particular, it has become clear that what distinguishes classical proof from its siblings is the presence of the structural rules of contraction and weakening in their complete generality (see, for example, Bellin et al. 2006 and the literature cited therein).

4. Model Theory

While the relevant logic R has a proof system more complex than the substructural logics such as linear logic, which lack distribution of (extensional) conjunction over disjunction, its model theory is altogether more simple. A Routley-Meyer model for the relevant logic R is comprised of a set of points P with a three-place relation R on P. A conditional A → B is evaluated at a world as follows:

A → B is true at x if and only if for each y and z where Rxyz, if A is true at y, B is true at z.

An argument is valid in a model just when in any point at which the premises are true, so is the conclusion. The argument A ⊢ B → B is invalid because we may have a point x at which A is true, but at which B → B is not. We can have B → B fail to be true at x simply by having Rxyz where B is true at y but not at z.

The three place relation R follows closely the behaviour of the mode of premise combination in the proof theory for a substructural logic. For different logics, different conditions can be placed on R. For example, if premise combination is commutative, we place a symmetry condition on R like this: Rxyz if and only if Ryxz. Ternary relational semantics gives us great facility to model the behaviour of substructural logics. (The extent of the correspondence between the proof theory and algebra of substructural logics and the semantics is charted in Dunn’s work on Gaggle Theory (1991) and is summarised in Restall’s Introduction to Substructural Logics (2000).)

Furthermore, if conjunction and disjunction satisfy the distribution axiom mentioned in the previous section, they can be modelled straightforwardly too: a conjunction is true at a point just when both conjuncts are true at that point, and a disjunction is true at a point just when at least one disjunct is true there. For logics, such as linear logic, without the distribution axiom, the semantics must be more complex, with a different clause for disjunction required to invalidate the inference of distribution.

It is one thing to use a semantics as a formal device to model a logic. It is another to use a semantics as an interpretive device to apply a logic. The literature on substructural logics provides us with a number of different ways that the ternary relational semantics can be applied to describe the logical structure of some phenomena in which the traditional structural rules do not apply.

For logics like the Lambek calculus, the interpretation of the semantics is straightforward. We can take the points to be linguistic items, and the ternary relation to be the relation of concatenation (Rxyz if and only if x concatenated with y results in z). In these models, the structural rules of contraction, weakening and permutation all fail, but premise combination is associative.

The contemporary literature on linguistic classification extends the basic Lambek Calculus with richer forms of combination, in which more syntactic features can be modelled (see Moortgat 1995).

Another application of these models is in the treatment of the semantics of function application. We can think of the points in a model structure as both functions and data, and hold that Rxyz if and only if x (considered as a function) applied to y (considered as data) is z. Traditional accounts of functions do not encourage this dual use, since functions are taken to be of a ‘higher’ than their inputs or outputs (on the traditional set-theoretic model of functions, a function is the set of its input-output pairs, and so, it can never take itself as an input, since sets cannot contain themselves as members). However, systems of functions modelled by the untyped λ-calculus, for example, allow for self-application. Given this reading of points in a model, a point is of type A → B just if whenever it takes inputs of type A, it takes outputs of type B. The inference rules of this system are then principles governing types of functions: the sequent

(A → B) & (A → C) ⊢ A → (B & C)

tells us that whenever a function takes As to Bs and As to Cs, then it takes As to things that are both B and C.

This example gives us a model in which the appropriate substructural logic is extremely weak. None of the usual structural rules (not even associativity) are satisfied in this model. This example of a ternary relational model is discussed in (Restall 2000, Chapter 11).

For the relevant logic R and its interpretation of natural language conditionals, more work must be done in identifying what features of reality the formal semantics models. This has been a matter of some controversy, since not only is the ternary relation unfamiliar to those whose exposure is primarily to modal logics with a simpler binary accessibility relation between possible worlds, but also because of the novelty of the treatment of negation in models for relevant logics. It is not our place to discuss this debate in much detail here, Some of this work is reported in the article on relevant logic in this Encyclopedia, and a book-length treatment of relevant logic in this light is Mares’ Relevant Logic: a philosophical interpretation (2004).

Bibliography

A comprehensive bibliography on relevant logic was put together by Robert Wolff and can be found in Anderson, Belnap and Dunn 1992. The bibliography in Restall 2000 (see Other Internet Resources) is not as comprehensive as Wolff’s, but it does include material up to the present day.

Books on Substructural Logic and Introductions to the Field

Other Works Cited

Other Internet Resources

Related Entries

logic: modal | logic: paraconsistent | logic: relevance