Substructural logics are non-classical logics notable for theabsence of one or morestructural rules present in classicallogic. Initial interest in substructural logics developedindependently in the second half of the twentieth century, throughconsiderations from philosophy (relevant logics), from linguistics(the Lambek calculus) and from the mathematics of proof theory (linearlogic). Since the 1990s, these independent lines of inquiry have beenunderstood to be different aspects of a unified field, and techniquesfrom substructural logics are useful in the study of traditionallogics such as classical and intuitionistic logic. This articleprovides a brief overview of the field of substructural logic. For amore detailed introduction, complete with theorems, proofs andexamples, the reader can consult the books and articles in theBibliography.

• 1. Structural Rules
• 2. Different Logics
• 3. Proof Theory
• 4. Model Theory
• 5. Quantifiers
• 6. Logics without Cut or Identity
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Structural Rules

Substructural logics are a family of logical systems characterised interms of theirstructural rules. A structural rule is alogical rule that applies indiscriminately to all propositions withoutregard to their form. The familiar inference rule ofmodusponens (from \(p\to q\) and \(p\) to infer \(q\)) is not astructural rule because the first premise of the rule must be aconditional. This is a rule not about the inferential behaviour of allpropositions, but a rule about conditionals. The syllogismBarbara (fromall Fs are G andall Gs are Hto inferall Fs are H) is similarly not a structural rule: itis a rule specifically applying to universal claims.Modusponens,Barbara and other familiar rules such as theLaw of Non-Contradiction areoperational rulesgoverning or describing the logical features of particular concepts,such as the conditional, universal generalisation, negation, etc. Notall logical rules are operational rules. Some rules govern the ambientbehaviour of logical consequenceas such, and these are thestructural rules.

TheCut rule can be stated like this: if from some premises(call them \(X\)) we can prove the conclusion \(A\), and if from \(A\)together with more premises (call them \(Y\)) we can prove \(B\) thenwe can prove the conclusion \(B\) from the premises \(X\) and \(Y\)taken together. \[ \cfrac{X\vdash A\qquad Y,A\vdash B}{X,Y\vdash B} \] Here, there is no restriction on the formof any of the particular judgements featuring in the rule. Theparticular premises and conclusions are completely general, soCut is a structural rule.

In this example, the structural rule is stated in terms of what onecanprove, and one way to motivate structural rules like thisis by way of considerations of how proofs may be formed and combined.After all, the proof from \(X\) together with \(Y\) to the conclusion\(B\) may be constructed by first proving \(A\) from \(X\) and thenusing this \(A\) together with \(Y\) to prove \(B\).

Structural rules can also be motivated by characterising logicalvalidity by way ofmodels. If an argument from some premisesto a conclusion is understood to bevalid when there is nomodel of the premises that is not also a model of the conclusion (sucha model would be acounterexample to the argument), then theCut rule may likewise be motivated: if every model of everymember of \(X\) is a model of \(A\), and every model of every member\(Y\) and of \(A\) is also a model of \(B\), then every model of eachmember of \(X\) and each member of of \(Y\) is (by virtue of being amodel of every member of \(X\)) a model of \(A\), and so (since it isalso a model of every member of \(Y\)), it is a model of \(B\). Inthis reasoning, we did not have to appeal to the truth conditions forany formulas in models: the rule is not beholden to any particularscheme concerning how formulas are evaluated. Provided that validityis defined in terms of preservation of “holding in amodel” (however that is to be understood), the logicalconsequence relation satisfies theCut rule.

So, regardless of whether we think of validity in terms of proofs orin terms of models, the structural rules are facts about validity thathold irrespective of the logical form of the components of thearguments. They arise from the general definition of validity and itsstructural features, rather than the rules governing particularconnectives, quantifiers or other items of vocabulary.

Nonetheless, different logical systems differ in the rules governingparticular logical concepts. Intuitionistic logic famously differsfrom classical logic in its treatment of negation. The structuralrules are an essential part of any explanation of the behaviour ofindividual logical concepts, because we use the ambient context oflogical consequence to characterise the behaviour of those concepts.For example, one way to characterise the behaviour of the conditional\(p\rightarrow q\) (read as “if \(p\) then \(q\)”) cantake this form:

This says that \(q\) follows from \(X\) together with \(p\) just when\(p \rightarrow q\) follows from \(X\) alone. The validity of thetransition from \(p\) to \(q\) (given \(X)\) is recorded by theconditional \(p \rightarrow q\). We characterise validity concerningconditionals in terms of a statement about validity involving thecomponents of those conditionals.

(This connection between the conditional and consequence is calledresiduation by analogy with the case in mathematics. Considerthe connection between addition and substraction. \(a + b = c\) if andonly if \(a = c - b\). The resulting \(a\) (which is \(c - b)\) is theresidual, what is left of \(c\) when \(b\) is taken away.Another name for this connection is thedeductiontheorem.)

The residuation equivalence between \(X,p\vdash q\) and \(X\vdash p\toq\) is not the only way to characterise the behaviour of theconditional. Sometimes it is helpful to study rules in which theinferential behaviour of a connective is described in terms of theconditions under which you can infer a sentence involving thatconnective (here, the left-to-right direction from \(X,p\vdash q\) to\(X\vdash p\to q\) answers that question) and also describes what onecan inferfrom a sentence involving that connective. Theresiduation condition for \(p\to q\) only answers this questionimplicitly, by way of an appeal to theCut rule, and theassumption that \(p\to q\vdash p\to q\). For then we can reason asfollows: \[ \cfrac{ \cfrac{ \begin{matrix}\\ {Y\vdash p} \end{matrix} \quad \cfrac{p\rightarrow q\vdash p\rightarrow q}{p\rightarrow q,p\vdash q} } {p\rightarrow q,Y\vdash q} \quad \begin{matrix}\\ {X,q\vdash C} \end{matrix} } {X,p\to q,Y\vdash C} \] So, from the two premises \(Y\vdash p\) and\(X,q\vdash C\) we can conclude \(X,p\to q,Y\vdash C\). This is aleft sequent rule for the conditional, presenting conditionsunder which it is appropriate to infer some conclusion \(C\) from\(p\to q\) used as a premise. This is sometimes used as an alternativeto the right-to-left half of the residuation equivalence (from\(X\vdash p\to q\) to \(X,p\vdash q\) since it, like the left-to-righthalf of the residuation eqiuvalence characterises the behaviour of theconditional in terms of the inferential behaviour of itscomponents.

Whether we use the residuation rules or the left/right sequent rulesfor the conditional, the connections between consequence and theconditional involve a number of distinct concepts. Not only is therethe turnstile, for logical validity, and the conditional, encodingconsequence inside the language of propositions, there is also thecomma, indicating thecombination of premises. Wehave read “\(X, p \vdash q\)” as “\(q\) follows from\(X\)together with \(p\)”. To combine premises is tohave a way to take themtogether. But how can we take themtogether? It turns out that there are different ways to do so, whichhave different logical properties, and so, we have differentsubstructural logics with different purely structural rules. Thebehaviour of premise combination may vary, and as a result, thebehaviour of the conditional and other logical connectives vary as aresult. In this introduction we will consider some examples of thisphenomenon.

1.1 Weakening

It is one thing for \(p\) to betrue. It is another for theconditional \(q \rightarrow p\) to be true. Yet, if‘\(\rightarrow\)’ is a material conditional, \(q\rightarrow p\) follows from \(p\). For many different reasons, we maywish to understand how a conditional might work in theabsence of this inference. This is tied to the behaviour ofpremise combination, as can be shown by this demonstration.

From the axiomatic \(p \vdash p\) (anything follows fromitself) we deduce that \(p\) follows from \(p\) together with\(q\), and then by residuation, \(p \vdash q \rightarrow p\). If wewish to reject the inference from \(p\) to \(q \rightarrow p\), thenwe either reject residuation, or reject the identity axiom at thestart of the proof, or we reject the first step of the proof. It isilluminating to consider what is involved in this last option. Here,we are to deny that \(p\) follows from \(p, q\). In general, we are toreject the inference rule that has this form:

This is the rule ofweakening: it steps from a strongerstatement, that \(A\) follows from \(X\) to a possibly weaker one,that \(A\) follows from \(X\) together with \(Y\). In this rule, themembers of \(X\), and \(Y\) and the conclusion \(A\) are arbitrary, soit is a purelystructural rule.

People have offered different reasons for rejecting the rule ofweakening, depending on the interpretation of consequence and premisecombination. One of the early motivating examples comes from a concernfor relevance. If the logic isrelevant (if to say that \(p\)entails \(q\) is true is to say, at least, that \(q\) trulydepends on \(p)\) then weakening need not hold. We may indeedhave \(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 theotherside of the comma too, in that we also wishthis argument tobe invalid:

Again, \(q\) may follow from \(q\), but this does not mean that itfollows 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 alogical truth such as \(q \rightarrow q\) may well fail.

1.2 Commutativity

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

In the absence of commutativity of premise combination, this proof isnot available. This is another simple example of the connectionbetween the behaviour of premise combination and that of deductionsinvolving the conditional.

There are many kinds of conditional for which this inference fails. Ifa conditional hasmodal force (if it expresses a kind ofentailment, in which \(p \rightarrow q\) is true when in every relatedcircumstance in which \(p\) holds, \(q\) does too), and if“\(\vdash\)” expresses local consequence \((p\vdash q\) ifand only if any model, at any circumstance at which \(p\) holds, sodoes \(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’sbeing a philosopher \((p \rightarrow q\) – in relatedcircunstances in which Greg is a logician, he is a philosopher) butthis does notentail that Greg is a philosopher. (There aremany circumstances in which the entailment \((p \rightarrow q)\) istrue but \(q\) is not.) So we have a circumstance in which \(p\) istrue but \((p \rightarrow q) \rightarrow q\) is not. The argument isinvalid.

This counterexample can also be understood in terms of behaviour ofpremise combination. Here when we say \(X,A \vdash B\) is true, we arenot just saying that \(B\) holds in any circumstance in which \(X\)and \(A\) both hold. If we are after a genuineentailmentA \(\rightarrow\) B, then we want \(B\) to be true in any(related) circumstance in which \(A\) is true. So, \(X,A \vdash B\)says that inany possibility in which \(A\) is true, so is\(B\). These possibilities might not satisfy all of \(X\). (Inclassical theories of entailment, the possibilities are those in whichall that is taken asnecessary in \(X\) are true.)

If premise combination is not commutative, then residuation can go intwo ways. In addition to the residuation condition giving thebehaviour of \(\rightarrow\), we may wish to define a new arrow\(\leftarrow\) as follows:

For the left-to-right arrow we havemodus ponens in thisdirection:

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

This is a characteristic of substructural logics. When we payattention to what happens when we don’t have the full complementof structural rules, then new possibilities open up. We uncovertwo conditionals underneath what was previously one (inintuitionistic or classical logic).

In the next section we will seeanother example motivating non-commutative premise combination and these twodifferent conditionals.

1.3 Associativity

Here is another kind of structural assumption present in proofs. Sofar, you might have assumed that the premises in a sequent are orderedin a list, and that the premise list \(p,q,r\) could be equallyunderstood as the list \(p,q\), to which \(r\) has been added on theright, or the list \(q,r\) to which \(p\) has been added on the left.If so, you take it that the premise structures \((p,q),r\) and\(p,(q,r)\) are identical, and that premise combination (representedhere by the comma) isassociative. The associativity ofpremise combination is another structural rule which has an impact onwhat inferences are valid.

To get a clear picture of how this follows, it will help to return tothe formulation of theCut rule, to see how we might clearlystate it without prejudging whether premise combination isassociative. Its more general form goes like this:

Whenever we can prove \(A\) from \(X\), and we can prove \(B\) fromsome assumptions including \(A\) somewhere, we can prove \(B\) fromthose assumptions where we replace those appeals to \(A\) (in thoseplaces) with appeals to \(X\) instead. Here, there is no implicitreordering or reshuffling of how premises are combined. We surgicallyreplace the appeal to \(A\) with the appeal to whetever it is that weused to justify \(A\).

In a similar way, the conditional rules can be understood withoutappeal to associativity: the equivalence between \(X,p\vdash q\) and\(X\vdash p\rightarrow q\) marks the fact that the comma can be readasapplication: the assumptions \(X\) deliver a conditionalif and only if whenever when we apply those assumptions to theantecedent, this delivers the consequent. There is nothing in thenotion of applicationper se that assumes associativity.

With this understanding, theleft rule for the conditionalhas the following shape:

This says that if we appeal to \(q\) as a part of some justificationof \(C\) and if we have some justification \(Y\) of another claim\(p\), then instead of directly appealing to \(q\) in thatjustification of \(C\) we can appeal to \(p\to q\) applied to \(Y\).Again, this formulation is careful to respect the order ofapplication, and no implicit reshuffling has taken place.

With all that understood, we can see the following proof, in which wefirst apply the left rule twice, introducing \(r\to p\) and \(p\to q\)to show that \(p\to q,(r\to p,r)\) together justify \(q\). To use thisto conclude something about \(r\to q\) we would like to discharge theassumption \(r\), but to do this, we must rearrange the order in whichthe premises are combined.

So, this proof appeals to the associativity of premise combination,while contraction and weakening are not used. In the absence ofassociativity, we should not expect the inference from \(p\to q\) to\((r\to p)\to(r\to q)\) to be valid.

1.4 Contraction

A final important example is the rule ofcontraction whichdictates how premises may be reused. Contraction is crucial in theinference of \(p \rightarrow q\) from \(p \rightarrow (p \rightarrowq)\)

In this proof, at the second-to-last step we use the principle that ifwe can derive some conclusion by way of applying some assumptiontwice (here, \(p\)), it can be justified when we apply thatassumptiononce instead. (Note: in this proof on the thirdline the assumptions are bracketed because this proof does not appealto the associativity of premise combination, so if we wish todistinguish \((A,B),C\) from \(A,(B,C\), we may do so.)

These different examples can give a sense of the role of structuralrules in determining the behaviour of a concept such asconditionality. Not only do structural rules influence theconditional, but they also have their effects on other connectives,such as conjunction and disjunction (as we shall see below) andnegation (Dunn 1993; Restall 2000).

1.5 Structure on the right of the turnstile

Gentzen’s pioneering work on the sequent calculus (Gentzen 1935) shows that the difference betweenclassical logic andintuitionistic logic can also be understood as a differencenot of the behaviour of one logical connective oranother—whether negation, disjunction or theconditional—but as a matter of the ambient structure of sequentsin which those connectives are defined, and the structural rulessatisfied in that setting. Gentzen’s sequent calculusLJ for intuitionistic logic is formulated in terms ofsequents of the form \(X \vdash A\), in which we have a collection ofantecedents and a single consequent. These are the kinds of sequentswe have focussed on so far. Gentzen’sLK calculus forclassical logic formulates sequents in a more general form

where we allow a number of formulas on the right of the sequent, justas we do on the left, so both \(X\) and \(Y\) are collections offormulas. The intended interpretation is that fromall of the\(X\) some of the \(Y\) follow In other words, we cannot have all ofthe \(X\) andnone of the \(Y\) obtaining. (See the entriesonProof Theory (Section 2) andPropositional Logic (Section 2.3.2) for more on the sequent calculus.)

Allowing sequents with multiple consequents and translating thefamiliar connective rules into this wider context, we are able toderive classical tautologies. For example, the derivation

shows that either \(p \rightarrow q\) or \(p\) must hold. This isclassically valid (if \(p\) fails, \(p\) isfalse, andconditionals with false antecedents are true), but invalid inintuitionistic logic. Similarly, the intuitionist derivation of thelaw of non-contradiction can be naturally ‘dualised’ intoa classical proof of the law of the excluded middle, as follows:\[ \cfrac{p\vdash p}{\cfrac{p,\neg p\vdash} {p\amp\neg p\vdash}} \qquad\qquad \cfrac{p\vdash p}{\cfrac{\vdash p,\neg p}{\vdash p\lor\neg p}} \] The difference between classical and intuitionisticlogic, then, can be understood as a difference arising from the kindsof structural rules permitted, and the kinds of structures appropriateto use in the analysis of logical consequence, rather than adifference due to the behaviour of one or more different logicalconstants.

1.6 Cut and Identity

Each of the structural rules considered here (weakening,commutativity, associativity, contraction) essentially involves thebehaviour of premise combination, or in the case of classicalsequents, premise andconclusion combination. The structuralrule we first saw, theCut rule, in its simplest form, hasnothing to do with combination of premises. In its most stripped-downform, theCut rule takes this shape: \[ \cfrac{A\vdash B\qquad B\vdash C}{A\vdash C} \] whichinvolves no taking together of formulas on the left or the right ofthe sequent at all. TheCut rule, at its heart, is not aboutthe distinctive behaviour of how premises or conclusions are combined,but about the relationship between what is needed toderive aformula (here, the so-called ‘Cut’ formula,\(B\)) occuring on theright of a sequent and then what onecando with that formula, as it occurs on theleft.To use the economic metaphor: if we can ‘pay’ \(A\) toreceive \(B\), and we could pay \(B\) to receive \(C\), then ourinitial payment of \(A\) should suffice to provide \(C\). Speakingmore abstractly, theCut rule states that a \(B\) on theright of a sequent is at least as powerful as a \(B\) on the left:anything we can prove from a \(B\) on theleft (here, \(C\))could be proved by anything that entails a \(B\) on theright.

There is one more structural rule which deserves mention. TheIdentity rule matches formulas on the left and on the rightin the opposite way: \[ B\vdash B \] This identity rule tells us that\(B\) on the left is strong enough to deliver \(B\) on the right. So,Cut andIdentity as structural rules involve therelationship between occurrences of formulas in the left and right ofsequents, while the other structural rules govern the ways thatformulas may be manipulated inside the left or the right ofsequents.

2. Different Logics

A range of substructural logics have been developed, independently, inthe second half of the 20th Century, and into the 21st. These logicscan be motivated in different ways.

2.1 Relevant Logics

It is natural to think that there is some connection between logicalconsequence an relevance. If \(X \vdash A\) holds, then one might hopethat the premises of our deduction (\(X\)) must somehow berelevant to the conclusion \(A\). With this understanding ofrelevance in mind, it is natural to restrict premise combination: Wemay have \(X \vdash A\) without also having \(X,Y \vdash A\), sincethe new material \(Y\) might not be relevant to the deduction of\(A\). Relevant logics, understood in this way, aresubstructural because relevance is understood as a propertyof logical consequence itself (and the structural rules governingconsequence), rather than a property of any one connective.

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 aroundAnderson and Belnap, their students Dunn and Meyer, and many others.The canonical references for the area are Anderson, Belnap andDunn’s two-volumeEntailment (1975 and1992). Other introductions can be found in Read’sRelevantLogic (1988), Dunn and Restall’sRelevance Logic (2000), and Mares’Relevant Logic:a philosophicalinterpretation (2004).

2.2 Linear Logic and other contraction-free logics

This is not the only way to restrict premise combination. Girard (1987) introducedlinear logic as a model for processes andresource use. The idea in this account of deduction is that resourcesmust be used (so premise combination satisfies the relevancecriterion) and they do not extendindefinitely. Premisescannot bere-used. So, I might have \(X,X \vdash A\), whichsays that I can use \(X\) twice to get \(A\). I might not have \(X\vdash A\), which says that I can use \(X\) once alone to get \(A\). Ahelpful introduction to linear logic is given in Troelstra’sLectures on Linear Logic (1992).

There are other formal logics in which thecontraction rule(from \(X,X \vdash A\) to \(X \vdash A)\) is absent. Most famous amongthese are Łukasiewicz’s many-valued logics. There has beena sustained interest in logics without contraction because it has beennoticed that the contraction rule features in paradoxical derivationssuch as the liar paradox, Curry’s paradox, and other semanticparadoxes (Curry 1977,Geach 1955; see alsoField 2008,Restall 1994 andZardini 2021).

2.3 The Lambek Calculus

Independently of either of these traditions, Joachim Lambek consideredmathematical models of language and syntax (Lambek 1958,1961). The idea here is that premise combination correspondsto 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 thenumber of premises used count butso does theirorder. Good introductions to the Lambekcalculus (also calledcategorial grammar) can be found inbooks by Moortgat (1988) Morrill (1994), and Moot and Retoré (2012).

2.4 ST and TS

Each substructural logic considered so far restricts the behaviour ofpremise combination in some way, by banning weakening, contraction, orexchange. Another family of substructural logics keeps all of thosestructural rules, but restricts one of the cross-sequent rules:Cut andidentity. These substructural logics differfrom classical logic either very little, or enormously, depending onwhich structural rule is rejected. Classical logic without theCut rule is, at one level, indistinguishable from classicallogic, because as Gentzen has shown (1935), theCut rule is eliminable: any sequent that can be provedusing cut can also be proved without it. So, the substructural variantof classical logic that goes without the cut rule is, as far as validsequents is concerned, classical logic itself.

On the other hand, if we remove theIdentity rule fromstandard presentations of classical logic, the result is a proofsystem that is far different. Classical logic without identity hasno valid sequents at all. Nothing is provable, becausederivations have nowhere to start.

Since the 2000s, there has been sustained attention on logics in whichthe rules of cut or identity are jettisoned for the purposes oftreatment of the various semantic phenomena, including vagueness andthe semantic paradoxes. Zardini (2008)’s “A Model for Tolerance” and van Rooij’s (2011)’s “Vagueness, Tolerance and Non-Transitive Entailment” eachutilised a cut-free (non-transitive) consequence relation to modelvague predicates satisfying a natural tolerance condition, to theeffect that anything sufficiently \(F\)-close to something that is\(F\) is also \(F\). If the conditional expressing this toleranceclaim (and the underlying consequence relation) is not transitive,then the sorites paradox is, in some sense, averted. Cobreros,etal. (2012) showed that this logic has simple models in terms of strict andtolerant semantic evaluation, which will be discussed below inSection 6, and Ripley (2012) showed that this logic provides the means to model a truth predicate\(T\) for which \(T\langle A\rangle\) is equivalent to \(A\), and forwhich a liar sentence \(\lambda\) (for which \(\lambda=\negT\lambda\)) gives rise to inconsistency, but not triviality. We canderive \(\vdash T\lambda\) and \(\vdash\neg T\lambda\) (and hence\(T\lambda \vdash \bot\)), by the standard liar-paradoxical reasoning,but the failure of the cut rule for \(T\)-sentences means that the wecannot proceed from \(\vdash T\lambda\) and \(T\lambda\vdash \bot\) tothe expected trivialising consequence \(\vdash\bot\). (Alan Weir (2005) earlier also utilised a Cut-free logic in the analysis of theparadoxes arising from a naïve truth predicate, however theresulting logic is notST, as the usual connective rules forthe conditional and negation are modified, along with the rejection ofCut.)

For reasons that will become manifest inSection 6, this logic is calledST (for Strict/Tolerantconsequence), and its cousin,TS (for Tolerant/Strictconsequence) is the logic of the classical sequent calculus withouttheidentity rule.

3. Proof Theory

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

and another toeliminate it.

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

This rule is more complex, but it has the same effect as the arrowelimination rule: It says that if \(X\) suffices for \(A\), and if youuse \(B\) (in some context \(Y)\) to prove \(C\) then you could justas well have used \(A \rightarrow B\) together with \(X\) (in thatsame context \(Y)\) to prove \(C\), since \(A \rightarrow B\) togetherwith \(X\) gives you \(B\).

Gentzen systems, with their introduction rules on the left and theright, have very special properties which are useful in studyinglogics. Since connectives are alwaysintroduced in a proof(read from top to bottom) proofs neverlose structure. If aconnective does not appear in the conclusion of a proof, it will notappear in the proof at all, since connectives cannot beeliminated.

In certain substructural logics, such as linear logic and the Lambekcalculus, and in the fragment of the relevant logic \(\mathbf{R}\)without disjunction, a Gentzen system can be used to show that thelogic isdecidable, in that an algorithm can be found todetermine whether or not an argument \(X \vdash A\) is valid. This isdone by searching for proofs of \(X \vdash A\) in a Gentzen system.Since premises of this conclusion must feature no language not in thisconclusion, and they have no greater complexity (in these systems),there are only a finite number of possible premises. An algorithm cancheck if these satisfy the rules of the system, and proceed to lookfor 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 \(\mathbf{R}\) is not decidable.This is partly because its proof theory is more complex than that ofother substructural logics. \(\mathbf{R}\) differs from linear logicand the Lambek calculus in having a straightforward treatment ofconjunction and disjunction. In particular, conjunction anddisjunction satisfy the rule ofdistribution:

The natural proof of distribution in any proof system uses bothweakening and contraction, so it is not available in the relevantlogic \(\mathbf{R}\), which does not contain weakening. As a result,proof theories for \(\mathbf{R}\) either contain distribution as aprimitive rule, or contain a second form of premise combination (socalledextensional combination, as opposed to theintensional premise combination we have seen) which satisfiesweakening and contraction.

In recent years, a great deal of work has been done on the prooftheory ofclassical logic, inspired and informed by researchinto substructural logics. Classical logic has the full complement ofstructural rules, and is historically prior to more recent systems ofsubstructural logics. However, when it comes to attempting tounderstand the deep structure ofclassical proof systems (andin particular, when two derivations that differ in some superficialsyntactic way arereally different ways to represent the oneunderlying ‘proof’) it is enlightening to think ofclassical logic as formed by a basic substructural logic, in whichextra structural rules are imposed as additions. In particular, it hasbecome clear that what distinguishes classical proof from its siblingsis the presence of the structural rules of contraction and weakeningin their complete generality (see, for example,Bellinet al. 2006 and the literature cited therein).

4. Model Theory

While the relevant logic \(\mathbf{R}\) has a proof system morecomplex than the substructural logics such as linear logic, which lackdistribution of (extensional) conjunction over disjunction, itsmodel theory is altogether more simple. A Routley-Meyermodel for the relevant logic \(\mathbf{R}\) is comprised of aset ofpoints \(P\) with a three-place relation \(R\) on\(P\). A conditional \(A \rightarrow B\) is evaluated at a world asfollows:

\(A \rightarrow 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 isvalid in a model just when in any point atwhich the premises are true, so is the conclusion. The argument \(A\vdash B \rightarrow B\) is invalid because we may have a point \(x\)at which \(A\) is true, but at which \(B \rightarrow B\) is not. Wecan have \(B \rightarrow 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 themode of premise combination in the proof theory for a substructurallogic. For different logics, different conditions can be placed on\(R\). For example, if premise combination is commutative, we place asymmetry condition on \(R\) like this: \(Rxyz\) if and onlyif \(Ryxz\). Ternary relational semantics gives us great facility tomodel the behaviour of substructural logics. (The extent ofthe correspondence between the proof theory and algebra ofsubstructural logics and the semantics is charted in Dunn’s workonGaggle Theory (1991) and is summarised in Restall’sIntroduction toSubstructural Logics (2000).

Furthermore, if conjunction and disjunction satisfy the distributionaxiom mentioned in the previous section, they can be modelledstraightforwardly too: a conjunction is true at a point just when bothconjuncts are true at that point, and a disjunction is true at a pointjust when at least one disjunct is true there. For logics, such aslinear logic,without the distribution axiom, the semanticsmust be more complex, with a different clause for disjunction requiredto invalidate the inference of distribution.

It is one thing to use a semantics as a formal device to model alogic. It is another to use a semantics as aninterpretivedevice toapply a logic. The literature on substructurallogics provides us with a number of different ways that the ternaryrelational semantics can be applied to describe the logical structureof some phenomena in which the traditional structural rules do notapply.

For logics like the Lambek calculus, the interpretation of thesemantics is straightforward. We can take the points to be linguisticitems, 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 isassociative.

The contemporary literature on linguistic classification extends thebasic Lambek Calculus with richer forms of combination, in which moresyntactic features can be modelled (seeMoortgat 1995).

Another application of these models is in the treatment of thesemantics offunction application. We can think of the pointsin a model structure as bothfunctions anddata, andhold that \(Rxyz\) if and only if \(x\) (considered as a function)applied to \(y\) (considered as data) is \(z\). Traditional accountsof functions do not encourage this dual use, since functions are takento be of a ‘higher’ than their inputs or outputs (on thetraditional set-theoretic model of functions, a function \(is\) theset of itsinput-output pairs, and so, it can never takeitself as an input, since sets cannot contain themselves asmembers). However, systems of functions modelled by the untyped\(\lambda\)-calculus, for example, allow for self-application. Giventhis reading of points in a model, a point is of type \(A \rightarrowB\) just if whenever it takes inputs of type \(A\), it takes outputsof type \(B\). The inference rules of this system are then principlesgoverning types of functions: the sequent

tells us that whenever a function takes \(A\)s to \(B\)s and \(A\)s to\(C\)s, then it takes \(A\)s to things that are both \(B\) and\(C\).

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

For the relevant logic \(\mathbf{R}\) and its interpretation ofnatural language conditionals, more work must be done in identifyingwhat features of reality the formal semantics models. This has been amatter of some controversy, since not only is the ternary relationunfamiliar to those whose exposure is primarily to modal logics with asimplerbinary accessibility relation between possibleworlds, but also because of the novelty of the treatment ofnegation in models for relevant logics. It is not our placeto discuss this debate in much detail here, Some of this work isreported in the article onrelevant logic in this Encyclopedia, and a book-length treatment of relevant logicin this light is Mares’Relevant Logic:aphilosophical interpretation (2004).

5. Quantifiers

The treatment of quantifiers in models for substructural logics hasproved to be quite difficult, but advances have been made in the early2000s. The difficulty came in what seemed to be a mismatch between theproof theory and model theory for quantifiers. Appropriate axioms orrules for the quantifiers are relatively straightforward. Theuniversal quantifier elimination axiom \[ \forall xA \rightarrow A[t/x] \] states that aninstance follows (in the relevant sense) from its universalgeneralisation. The introduction rule \[ \cfrac{\vdash A\rightarrow B} {\vdash A\rightarrow \forall xB} \] (where the provisothat \(x\) is not free in \(A\) holds) tells us that if we can provean instance of the generalisation \(\forall xB\), as a matter oflogic, from some assumption which makes no particular claim about thatinstance, we can also prove the generalisation from that assumption.This axiom and rule seems to fit nicely with any interpretation of thefirst-order quantifiers in a range of substructural logics, from theweakest systems, to strong systems like \(\mathbf{R}\).

While the proof theory for quantifiers seems well behaved, thegeneralisation to model theory for substructural logics has proveddifficult. Richard Routley (1980) showed that adding the rules for the quantifiers to a very weaksystem of substructural logic \(\mathbf{B}\) fits appropriately withthe ternary relational semantics, where quantifiers are interpreted asranging over a domain of objects, constant across all of the points inthe model. This fact doesnot apply for stronger logics, inparticular, the relevant logic \(\mathbf{R}\). Kit Fine (1989) showed that there exists a complex formula which holds in allconstant domain frame models for \(\mathbf{R}\) but which is notderivable from the axioms. The details of Fine’s argument arenot important for our purposes, but the underlying cause for themismatch is relatively straightforward to explain. In the constantdomain semantics, the universal generalisation \(\forall x Fx\) hasexactly the same truth conditions—at every point in themodel—as the family of instances \(Fx_1\), \(Fx_2\),\(Fx_3,\ldots\), \(Fx_\lambda,\ldots\), where the objects of thedomains are enumerated by the values of the terms \(x_i\). So, thequantified expression \(\forall x Fx\) is semanticallyindistinguishable from the (possibly infinite) conjunction \(Fx_1\landFx_2\land Fx_3\land\cdots \). However, no conjunction of instances(even an infinite one) could berelevantly equivalent to theuniversally quantified claim \(\forall x Fx\), because the instancescould be true in a circumstance (or could be made true by acircumstance) without also making true the generalisation—ifthere had been more things than those. So, constant domain models seemill-suited to the project of a relevant theory of quantification.

Robert Goldblatt and Edwin Mares (2006) have shown that there is a natural alternative semantics for relevantquantification, and this approach turns out to be elegant andrelatively straightforward. The crucial idea is to modify the ternaryrelational semantics just a little, so that not every set of pointsneed count as a ‘proposition’. That is, not every set ofpoints is the possible semantic value for a sentence. So, while thereis a set of worlds determined by the infinite conjunction of instancesof \(\forall xFx\): \(Fx_1\land Fx_2\land Fx_3\land\cdots \), thatprecise set of worlds may not count as a proposition. (Perhaps thereis no way to single out those particular objects in such a way as todraw them together in the one judgement.) What wecan say isthe generalisation \(\forall xFx\) and that is a proposition thatentails each of the instances (that is the universal quantifierelimination axiom), and if a proposition entails each instance, itentails the generalisation (that is the introduction rule), so theproposition expressed by \(\forall xFx\) is thesemanticallyweakest proposition that entails each instanceFa. Thisis precisely the modelling condition for the universal quantifier inGoldblatt & Mares’ models, and it matches the axiomsexactly.

6. Logics without Cut or Identity

As we saw inSection 1, structural rules come in two kinds, those that constrain thebehaviour of premise or conclusion combination on one side of asequent (commutativity, contraction, weakening) and those thatessentially involve the connection between one side of the sequent andthe other (identity, and cut): our treatment of proofs and models forsubstructural logics have focussed on substructural logics withdistinctive choices of structural rules of the first kind. In thislast section, it is time to focus on more recent work on substructurallogics that reject eitherCut oridentity.

Logics without theCut rule have non-transitive consequencerelations. In the philosophical literature, there are a number ofdifferent reasons cited for rejecting transitivity of consequence ingeneral. One reason is to focus onmaterial consequence (seeBrandom 2000) ordefault consequence (seeReiter 1980, and the entry onNon-Monotonic Logic) rather than necessary and formale consequence. (From Tweety being abird, the default inference that Tweety flies is appropriate. And,from Tweety being a penguin, we can infer that Tweety is a bird.However, it is in appropriate to cut out the middle step and to inferthat Tweety flies from the premise that Tweety is a penguin.)

Another reason to reject transitivity of validity is on grounds ofrelevance. Neil Tennant has championed a relevant logic thatrejects the unrestrictedCut rule on relevance grounds (2017). In Tennant’score logic, both \(\neg p\vdash \negp\lor q\) and \(p,\neg p\lor q\vdash q\) hold, but we cannot useCut to derive \(p,\neg p\vdash q\), for here, the \(q\) isirrelevant and a logical free-rider. In core logic, \(p,\neg p\vdash\) holds (since \(p\) and its negation are jointly inconsistent) butwe cannot use weakening to conclude \(p,\neg p\vdash q\). In thislogic, the cut rule does not hold in full generality, but arestriction of itdoes hold. If \(X\vdash A,Y\) and\(X',A\vdash Y'\), then there aresubsets \(X^*\subseteqX\cup X'\) and \(Y^*\subseteq Y\cup Y'\) where \(X^*\vdash Y^*\).RestrictingCut on core logic grounds would be of no help tothe logician who wants to respond to the semantic paradoxes byadmitting \(\vdash T\lambda\) and \(\vdash T\lambda\vdash\bot\) whilerejecting \(\vdash\bot\).

The cut-free logicST of strict/tolerant validitymentioned above is a very different kind of cut-free logic than either a logic ofmaterial or default inference or Tennant’s core logic. For onematter, at the level of valid sequents, it justis classicallogic, for it is given by Gentzen’s sequent calculus without theCut rule, and as Gentzen has shown (1935), theCut rule is eliminable.

The model theory forST is remarkably simple. Weevaluate formulas with respect to atripartite evaluation.(This could be understood as a function assigning to each formula oneof the values \(0\), \(i\) and \(1\), or equivalently as apartial function assigning to each formula either \(0\) or\(1\), but perhaps failing to assign a value in soem cases.) Weevaluate complex formulas using the standard classicaltruth-conditions, naturally modified to allow for partial valuations:\(v(\neg A)=1\) iff \(v(A)=0\), and \(v(\neg A)=0\) iff \(v(A)=1\);\(v(A\amp B)=1\) iff \(v(A)=1\) and \(v(B)=1\), and \(v(A\amp B)=0\)iff \(v(A)=0\) or \(v(B)=0\), and so on. (This is one definition ofvaluations forKleene’s strong three-valued logic.) We will say that such a valuation counts as anST-counterexample to a sequent \(X\vdash Y\) if andonly if it assigns \(1\) to every formula in \(X\) and \(0\) to everyformula in \(Y\). If we think of the formulas assigned \(1\) asstrictly true (or has assertible when we hold ourselves tostrict standards) and those that are not assigned \(0\) astolerantly true (or as assertible when we hold ourselves tomore tolerant standards), then the valid arguments are those for whichwhenever the premises arestrictly true, the conclusion is atleasttolerantly true. Hence then name,ST.Since validity is not preservation of a fixed value (the consequentstandards are lower than the antecedent standards), theCutrule can, in general, fail.

It is not too difficult to see how this substructural logic is anattractive site to consider the semantic paradoxes. Given the liarsentence \(\lambda\) the derivation of \(\vdash T\lambda\) tells usthat the liar is at least tolerantly true. The derivation of\(T\lambda\vdash\bot\) tells us that the liar cannot bestrictly true. It is fixed in the middle, with both it andits negation remaining tolerantly true, but not strictly true.

In a similar way, each of the conditional claims in asorites paradoxical argument of the form \(p_n\rightarrow p_{n+1}\) can be taken to be at leasttolerantly true, since with a sufficiently slow variationbetween cases, there will never be an instance where \(p_n\) isstrictly true and \(p_{n+1}\) is strictly false.

Once theST response to the paradoxes was considered,rejecting theremaining structural rule,identitywas natural to consider. Hence, Fjellstand (2015) and French (2016) have examined the logic of the sequent calculus withoutidentity. This, too, has a natural semantics in partialvaluations. If we retainCut but discard identity, then thenatural logic isTS: a sequent \(X\vdash Y\) has aTS-counterexample when there is a valuation thatsends every member of \(X\)away from \(0\) (i.e., they areat least tolerantly true) and every member of \(Y\)away from\(1\) (i.e., they are not strictly true). A valuation thatassigns \(p\) neither \(0\) nor \(1\) is thereby a counterexample tothe sequent \(p\vdash p\) and so, we have the means to invalidate therule of identity.

These substructural logics: those without cut and identity, raise thequestion of their nature aslogics in a way that the firstgeneration of substructural logics did not.ST hasexactly the same provable sequents in the logical vocabulary asclassical logic, andTS has none. IsST identical to classical logic? IsTS identical to any other logic with no derivablesequents? To flatly answer “yes” to these questions wouldbe to miss the distinctive behaviour of these logical systems.ST differs from classical logic not at the level ofsequents but at the level of the relations between sequents.TheCut rule, which can be understood as an inference rulerelating sequents, is valid under any class of two-valued valuations,but is invalid inST. Similarly, although at thelevel of sequents the logicTS is empty, at the levelof relationships between sequents, it is rich. From this observationhas arisen the recent study ofmeta-inferences (seeBarrioet al 2014, andBarrioet al 2019). Reflection on the natural way to understand meta-inferences betweensequents in logics likeST andTSwhich use two different distinguished values has raised a naturalquestion. If we have two different grades of validity (strict andtolerant) at the level of an individual formula, then why restrictourselves to a single validity verdict when it comes to a sequent? Infact, two natural grades of validity for (level 2) meta-inferences areavailable to us. AST validity is a much moretolerant criterion thanTS validity. We can say thata sequent-to-sequent meta-inference isTS/ST valid ifwhenever the premise sequents areTS valid, then theconclusion sequent isST valid. It turns out, then,that the meta-inference ofCut is indeedTS/ST meta-valid, and theTS/STvalid meta-inferences are exactly the family of meta-inferencestraditionally valid in classical logic, and this result naturallygeneralises up the hierarchy ofn-level meta-inferences foralln (Barrioet al 2019).

The connection between the cut-free sequent calculus and three-valuedlogics has a long history, pre-dating its incorporation into recentwork on substructural logics. Schütte (1960) used a non-deterministic three-valued semantics for the cut-freeclassical sequent calculus, and this work was extensively used byGirard (1987b, Chapter 3), in his analysis of the semantics of the cut-free sequentcaclulus. The application of three-valued methods to the classicalsequent calculus in the absence of the structural rule ofidentity was also considered in Hösli and Jäger (1994). This work has application to understanding phenomena in logicprogramming (Jäger, 1993).

Bibliography

A comprehensive bibliography on relevant logic was put together byRobert Wolff and can be found in Anderson, Belnap and Dunn 1992. Thebibliography in Restall 2000 is not as comprehensive as Wolff’s,but it does include material up to the end of the 20th Century.

Books on Substructural Logic and Introductions to the Field

• 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 logicin the Anderson–Belnap tradition. Some chapters in these bookshave other authors, such as Robert K. Meyer and AlasdairUrquhart.]
• Barrio, E. and Égré (2022)“Substructural Logics and Metainferences”Journal ofPhilosophical Logic, 51: 1215–1231.
  [A summary of recent work on reflexivity and theCut rule andcharacterising different logics in terms of the metainferences theyadmit.]
• Bimbó, K. and Dunn, J. M., 2008,Generalised Galois Logics: Relational Semantics of NonclassicalLogical Calculi, CSLI Lecture Notes, v. 188, CSLI, Stanford.
  [A systematic treatment of the ternary relational semantics and itsgeneralisations for substructural logics.]
• Dunn, J. M. and Restall, G., 2000,“Relevance Logic” in F. Guenthner and D. Gabbay (eds.),Handbook of Philosophical Logic second edition; Volume 6,Kluwer, pp 1–136.
  [A summary of work in relevant logic in the Anderson–Belnaptradition.]
• Galatos, N., P. Jipsen, T.Kowalski, and H. Ono, 2007,Residuated Lattices: An AlgebraicGlimpse at Substructural Logics (Studies in Logic: Volume 151),Amsterdam: Elsevier, 2007.
• Mares, Edwin D., 2004,Relevant Logic:a philosophical interpretation Cambridge University Press.
  [An introduction to relevant logic, proposing an information theoreticunderstanding of the ternary relational semantics.]
• Moortgat, Michael, 1988,CategorialInvestigations: Logical Aspects of the Lambek Calculus Foris,Dordrecht.
  [An introduction to the Lambek calculus.]
• Moot, Richard and RetoréChristian (2012)The Logic of Categorical Grammars, Springer,Berlin.
  [An introduction to the Lambek calculus, including its non-associativevariant, multimodal calculi, linear logic and proof nets.]
• Morrill, Glyn, 1994,Type Logical Grammar:Categorial Logic of Signs Kluwer, Dordrecht
  [An introduction to the Lambek calculus.]
• Ono, Hiroakira, 2019,Proof Theory and Algebrain Logic Springer, Singapore
  [Not exclusively on substructural logics, this treatment of therelationship between proof theory and algebra treats logical systemsquite generally, and includes substructural logics in its remit.]
• Paoli, Francesco, 2002,SubstructuralLogics:A Primer Kluwer, Dordrecht
  [A general introduction to substructural logics.]
• Read, S., 1988,Relevant Logic, Oxford:Blackwell.
  [An introduction to relevant logic motivated by considerations in thetheory of meaning. Develops a Lemmon-style proof theory for therelevant logic \(\mathbf{R}\).]
• Restall, Greg, 2000,An Introduction toSubstructural Logics, Routledge. (online précis)
  [A general introduction to the field of substructural logics.]
• Routley, R., Meyer, R.K.,Plumwood, V., and Brady, R., 1983,Relevant Logics and theirRivals, Volume I, Atascardero, CA: Ridgeview.
  [Another distinctive account of relevant logic, this time from anAustralian philosophical perspective.]
• Schroeder-Heister, Peter, andDošen, Kosta, (eds), 1993,Substructural Logics,Oxford University Press.
  [An edited collection of essays on different topics in substructurallogics, from different traditions in the field.]
• Troestra, Anne, 1992,Lectures on LinearLogic, CSLI Publications
  [A quick, easy-to-read introduction to Girard’s linearlogic.]
• Zardini, Elia, 2021, “SubstructuralApproaches to Paradox,”Synthese, 199: 493–525.
  [A summary of recent work on substructural approaches toparadox.]

Other Works Cited

• Ackermann, Wilhelm, 1956,“Begründung Einer Strengen Implikation,”Journalof Symbolic Logic, 21: 113–128.
• Avron, Arnon, 1988, “The Semantics and ProofTheory of Linear Logic,”Theoretical Computer Science,57(2–3): 161–184.
• Barrio, Eduardo; LucasRosenblatt, and Diego Tajer, 2014, “The Logics ofStrict-Tolerant Logic,”Journal of Philosophical Logic,44:5, 551–571.
• Barrio, Eduardo; Federico Pailos,and Damian Szmuc, 2019, “A Hierarchy of Classical andParaconsistent Logics,”Journal of Philosophical Logic,49:1, 93–120.
• Bellin, Gianluigi; MartinHyland, Edmund Robinson, and Christian Urban, 2006, “CategoricalProof Theory of Classical Propositional Calculus,”Theoretical Computer Science, 364: 146–165.
• Brandom, Robert, 2000ArticulatingReasons, Harvard University Press.
• Church, Alonzo, 1951, “The Weak Theory ofImplication,” inKontrolliertes Denken: Untersuchungen zumLogikkalkül und zur Logik der Einzelwissenschaften, A.Menne, A. Wilhelmy and H. Angsil (eds.), Kommissions-Verlag KarlAlber, 22–37.
• Cobreros, Pablo; PaulÉgré, David Ripley and Robert van Rooij, 2012,‘Tolerant, Classical, Strict’Journal of PhilosophicalLogic, 21:347–385.
• Curry, Haskell B., 1977,Foundations ofMathematical Logic, New York: Dover (originally published in1963).
• Dunn, J.M., 1991, “Gaggle Theory: AnAbstraction of Galois Connections and Residuation with Applications toNegation and Various Logical Operations,” inLogics in AI,Proceedings European Workshop JELIA 1990 (Lecture notes inComputer Science, Volume 476), Berlin: Springer-Verlag.
• –––, 1993, “Star andPerp,”Philosophical Perspectives, 7:331–357.
• Field, H., 2008,Saving Truth fromParadox, Oxford: Oxford University Press.
• Fine, K., 1989, “Incompleteness forQuantified Relevance Logics,” in J. Norman and R. Sylvan (eds.),Directions in Relevant Logic, Dordrecht: Kluwer, pp.205–225.
• Fjellstand, Andreas, 2015. “How aSemantics for Tonk Should Be,”Review of SymbolicLogic, 8:488–505.
• French, Rohan, 2016. “StructuralReflexivity and the Paradoxes of Self-Reference,”,Ergo, 3 No. 05. doi:10.3998/ergo.12405314.0003.005
• Geach, P. T., 1955, “On Insolubilia,”Analysis, 15: 71–72.
• Gentzen, Gerhard, 1935, “Untersuchungenüber das logische Schließen,”MathematischeZeitschrift, 39: 176–210 and 405–431.
  [An English translation is found in Gentzen 1969.]
• –––, 1969,The CollectedPapers of Gerhard Gentzen, M. E. Szabo (ed.), Amsterdam: NorthHolland, 1969.
• Girard, Jean-Yves, 1987, “LinearLogic,”Theoretical Computer Science, 50:1–101.
• –––, 1987b,Proof Theoryand Logical Complexity, Volume 1, Bibliopolis, Naples.
• Goldblatt, R., and E. Mares, 2006,“An Alternative Semantics for Quantified Relevant Logic,”Journal of Symbolic Logic, 71(1): 163–187.
• Hösli, Brigitte and Gerhard Jäger,1994. “About Some Symmetries of Negation,”Journal ofSymbolic Logic 59(2):473–485.
• Jäger, Gerhard, 1993, “Someproof-theoretic aspects of logic programming,” p. 113–142inLogic and Algebra of Specification, F. Bauer, W. Brauerand H. Schwichtenberg (ed.), Springer.
• Lambek, Joachim, 1958, “The Mathematics ofSentence Structure,”American Mathematical Monthly, 65:154–170.
• –––, 1961, “On theCalculus of Syntactic Types, ” inStructure of Language andits Mathematical Aspects (Proceedings of Symposia in AppliedMathematics, XII), R. Jakobson (ed.), Providence, RI: AmericanMathematical Society.
• Moh Shaw-Kwei, 1950, “The Deduction Theoremsand Two New Logical Systems,”Methodos, 2:56–75.
• Moortgat, Michael, 1995, “MultimodalLinguistic Inference,”Logic Journal of the IGPL, 3:371–401.
• Ono, Hiroakira, 2003, “Substructural Logicsand Residuated Lattices – an Introduction,” in V.Hendricks and J. Malinowski (eds.),Trends in Logic: 50 Years ofStudia Logica, Dordrecht: Kluwer, 2003, pp. 193–228.
• Reiter, Raymond, 1980. “A Logic for DefaultReasoning,”Artificial Intelligence,13:81–132.
• Ripley, David, 2012, “ConservativelyExtending Classical Logic with Transparent Truth’The Reviewof Symbolic Logic, 5:354–378.
• Rooij, Robert van, 2011, “Vagueness,tolerance and non-transitive entailment,’ in P. Cintula, C.Fermüller, L. Godo, and P. Hajek (eds.),Reasoning UnderVagueness: Logical, Philosophical and Linguistic Perspectives,College Publications, pp. 205–222.
• Routley, R., 1980. “Problems and Solutionsin Semantics in Quantified Relevant Logics,” in A. Arruda, R.Chuaqui, and N.C.A. Da Costa (eds.),Mathematical Logic in LatinAmerica, Amsterdam: North Holland, 1980, pp. 305–340.
• Schütte, Kurt, 1960. “Syntactical andSemantical Properties of Simple Type Theory,”Journal ofSymbolic Logic, 25:305–326.
• Tennant, Neil, 2017.Core Logic, OxfordUniversity Press.
• Troelstra, A.S., 1992, “Lectures onLinear Logic”,CSLI Lecture Notes (Number 29),Stanford: CSLI Publications.
• Weir, Alan, 2005. “Naive Truth andSophisticated Logic” in Jc Beall and B. Armour-Garb (eds.),Deflationism and Paradox, pages 218–249.
• Zardini, Elia, 2008. “A Model ofTolerance,”Studia Logica 90(3), 337–368.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• 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 substructurallogics.

Related Entries

connectives: sentence connectives in formal logic |logic: linear |logic: modal |logic: paraconsistent |logic: propositional |logic: relevance |proof theory