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

- Residuation
- Logics in the Family
- Proof Systems
- Semantics
- Bibliography
- Other Internet Resources
- Related Entries

It says thatp,qrif and only ifpqr

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

pp

----------

p,qp

-------------

pqp

is called the rule of

XA

----------

X,YA

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,

qq

----------

p,qq

-------------

pqq

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.

pqpq

---------------------

pq,pq

-------------------

p,pqq

---------------------

p(pq)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:

For the left-to-right arrow we havep,qrif and only ifqrp

For the right-to-left arrow,pq,pq

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 uncoverp,qpq

This proof uses the

pq,pqrp,rp

---------------------------------

pq, (rp,r)q

--------------------------

(pq,rp),rq

----------------------------

pq,rprq

-----------------------------------

pq(rp) (rq)

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(pq)p(pq)pqpq

---------------------------------- -----------------------

p(pq),ppqpq,pq

------------------------------------------------

(p(pq),p),pq

--------------------------

p(pq),pq

-----------------------

p(pq)pq

and another to

X,AB

----------------

XAB

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.

XABYA

--------------------------

X,YB

This rule is more complex, but it has the same effect as the arrow elimination rule: It says that if

XAY(B)C

--------------------------

Y(AB,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*:

The natural proof of distribution in any proof system uses both weakening and contraction, so it is not available in the relevant logicp& (qr) (p&q) (p&r)

An argument isABis true atxif and only if for eachyandzwhereRxyz, ifAis true aty,Bis true atz.

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.

- Anderson, A.R., and Belnap, N.D., 1975,
*Entailment: The Logic of Relevance and Necessity*, Princeton, Princeton University Press, Volume I. - Anderson, A.R., Belnap, N.D. Jr., and Dunn, J.M., 1992,
*Entailment*, Volume II, Princeton, Princeton University Press

[This book and the previous one summarise the work in relevant logic in the Anderson--Belnap tradition. Some chapters in these books have other authors, such as Robert K. Meyer and Alasdair Urquhart.] - Dunn, J.M., 1986, "Relevance Logic and Entailment" in
F. Guenthner and D. Gabbay (eds.),
*Handbook of Philosophical Logic*, Volume 3, Dordrecht: Reidel pp 117--224.

[A summary of work in relevant logic in the Anderson--Belnap tradition. An updated version of this essay, co-authored with Restall, will appear in the new edition of the*Handbook of Philosophical Logic*.] - Moortgat, Michiel, 1988,
*Categorial Investigations: Logical Aspects of the Lambek Calculus*Foris, Dordrecht.

[Another introduction to the Lambek calculus.] - Morrill, Glyn, 1994,
*Type Logical Grammar: Categorial Logic of Signs*Kluwer, Dordrecht

[An introduction to the Lambek calculus.] - Read, S., 1988,
*Relevant Logic*, Oxford: Blackwell.

[An introduction to relevant logic from a distinct philosophical perspective.] - Restall, Greg, 2000,
*An Introduction to Substructural Logics*, Routledge. (online précis)

[A comprehensive introduction to the field of substructural logics.] - Routley, R., Meyer, R.K., Plumwood, V., and Brady, R., 1983,
*Relevant Logics and its Rivals*, Volume I, Atascardero, CA: Ridgeview.

[Another distinctive account of relevant logic, this time from an Australian philosophical perspective.] - Schroeder-Heister, Peter, and Dosen, Kosta, (eds), 1993,
*Substructural Logics*, Oxford University Press.

[An edited collection of essays on different topics in substructural logics, from different traditions in the field.] - Troestra, Anne, 1992,
*Lectures on Linear Logic*, CSLI Publications

[A quick, easy-to-read introduction to Girard's linear logic.]

- Ackermann, Wilhelm, 1956, "Begründung Einer Strengen
Implikation",
*Journal of Symbolic Logic***21**113-128. - Church, Alonzo, 1951, "The Weak Theory of Implication", in
*Kontroliertes Denken: Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften*, Kommissions-Verlag Karl Alber, edited by A. Menne, A. Wilhelmy and H. Angsil, 22-37. - Curry, Haskell B., 1977,
*Foundations of Mathematical Logic*, Dover (originally published in 1963). - Dunn, J.M., 1991, "Gaggle Theory: An Abstraction of Galois
Connections and Residuation with Applications to Negation and Various
Logical Operations", in
*Logics in AI, Proceedings European Workshop JELIA 1990*, Lecture notes in Computer Science, volume**476**Springer-Verlag. - Dunn, J.M., 1993, "Star and Perp,"
*Philosophical Perspectives***7**331-357. - Geach, P. T., 1955, "On Insolubilia,"
*Analysis***15**71-72. - Girard, Jean-Yves, 1987, "Linear Logic,"
*Theoretical Computer Science***50**1-101. - Lambek, Joachim, 1958, "The Mathematics of Sentence Structure",
*American Mathematical Monthly***65**154-170. - Lambek, Joachim, 1961, "On the Calculus of Syntactic Types", in
*Structure of Language and its Mathematical Aspects*, edited by R. Jakobson, (Proceedings of Symposia in Applied Mathematics, XII). - Moh Shaw-Kwei, 1950, "The Deduction Theorems and Two New Logical
Systems,"
*Methodos***2**56-75. - Slaney, John, 1994, "Finite Models for some Substructural Logics," Automated Reasoning Project Technical Report TR-ARP-04-94. Available as either a DVI or Postscript file.

- Restall, Greg, BibTeX Bibliography on Substructural Logic (sourcefile via ftp), from Restall 2000.
- Restall, Greg, 1994,
*On Logics Without Contraction*, Ph. D. Thesis, The University of Queensland. - Slaney, John, 1995, MaGIC: Matrix Generator for Implication Connectives, a software package for generating finite models for substructural logics.

*First published: July 4, 2000*

*Content last modified: May 16, 2002*