This is a file in the archives of the Stanford Encyclopedia of Philosophy. 
how to cite 
Stanford Encyclopedia of Philosophy 
content revised

p, q r if and only if p q rIt 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. (It is called residuation by analogy with residuation 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.)
However, there is one extra factor in the equation. 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. The behaviour of premise combination is also important in determining the behaviour of the conditional. As the comma's behaviour varies, so does the conditional. In this introduction we will see how this comes about.
From the axiomatic p p (anything follows from itself) we deduce that p follows from p together with q, and then by the residuation condition, p q p. Given that we accept the residuation condition, and the identity axiom at the start of the proof, we must reject the first step in the proof if we are to deny that q p follows from p. This rule, which has the general form:
p p

p, q p

p q p
is called the rule of weakening. We step from a stronger statement, that A follows from X to a possibly weaker one, that A follows from X together with Y.
X A

X, Y A
This rule may fail, given different notions of premise combination (the notion encoded by the comma in X,Y). If the conditional is relevant (if to say that p q is true is to say, at least, that q truly depends on p) then the comma will 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:
Again, q may follow from q, but this doesn't 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.
q q

p, q q

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 the conditional.
p q p q

p q, p q

p, p q q

p (p q) q
There are many kinds of conditional for which this inference fails. If has modal force (read it as entails) then we may have p without also having (p q) q. 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) but this does not entail that Greg is a philosopher. (There are many possibilities in which the entailment (p q) is true but q is not.) So we have p true but (p q) q is not true.
This makes sense when we consider premise combination. Here when we say X,A B is true, we are not just saying that B follows when we put X and A together. If we are after a genuine entailment A B, then we want B to be true in any (related) possibility in which A is true. So, X,A B says that in any possibility in which A is true, so is B. These possibilities mightn't 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 pFor the lefttoright arrow we have modus ponens in this direction:
p q, p qFor the righttoleft arrow, modus ponens is provable with the premises in the opposite order:
p, q p qThis 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).
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.
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)
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).
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
and another to eliminate it.
X, A B

X A 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 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 B Y A

X, Y B
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.
X A Y(B) C

Y(A B, X) C
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.
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. For logics like as the Lambek calculus, the interpretation of the semantics is straightforward. We can take the points to be linguistic units, and the ternary relation to be the relation of composition (Rxyz if and only if x concatenated with y results in z). 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. Some of this work is reported in the article on relevant logic in this Encyclopedia.
First published: July 4, 2000
Content last modified: May 17, 2002