Abstract
Substructural logics owe their name to the fact that an especially immediate and intuitive way to introduce them is by means of sequent calculi à la Gentzen where one or more of the structural rules (weakening, contraction, exchange, cut) are suitably restricted or even left out. We do not assume the reader to be familiar with the terminology of the preceding sentence, which will be subsequently explained in full detail — but if only she has some acquaintance with the history of twentieth century logic, at least the name of Gerhard Gentzen should not be completely foreign to her.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
See § 2 below.
We shall discuss in greater detail the informal meaning of sequents in § 3 below.
It is worth remarking that some authors (e.g. Girard et al. 1989; Wansing 1998) do not classify cut among structural rules, preferring to set it apart from this group of rules.
Cp. § 3.
All of this vague terminology will be made precise in Chapter 4, where display calculi will be dealt with in greater detail.
Visibility is one of the ideas underlying basic logic, a weak substructural logic to which we shall revert in Appendix B.
Good discussions of the distinction between sharing and non-sharing rules, as well as of different systems containing appropriate combinations of the former and the latter, can be found in Troelstra and Schwichtenberg (1996) and in Baaz, Ciabattoni et al. (1998).
The pair “additive/multiplicative” stems from Girard (1987) and is preferred by linear logicians, while the pair “extensional/intensional” is privileged in relevant circles. Our usage has therefore the advantage of granting us a position of neutrality in this terminological controversy.
Except for some hints in Appendix B.
This terminology is drawn from Casari (1997a), where an excellent discussion can be found of themes related to the present issue.
An amusing defence of the ambiguity of “and” and “or” in natural language, with examples drawn from a restaurant situation, can be found in Danos and Di Cosmo (200+).
For Epstein’s relatedness logic this is not wholly correct: while relatedness implication is not generally transitive, the relation of derivability, which is defined classically in that logic, is such. But since this relation does not mirror the behaviour of provable implication (the usual deduction theorem, in fact, does not hold), one could just as well say that the real derivability relation of relatedness logic is not unrestrictedly transitive.
The merit of questioning the correctness of weakening inferences, however, should not be credited to modern logic. As Casari (1997a) remarks, Sextus Empiricus already acknowledged that an argument can be inconclusive by redundancy (xatià napoAxrjv) “when something external and superfluous is adjoined to the premises” (Against the Mathematicians, VIII, 431).
The term “relevance logic” is more fashionable in the United States, while “relevant logic” is more often used by the British and the Australasian logical communities.
The introduction of the expression “paraconsistent logic” is usually credited to the Peruvian philosopher Francisco Miró Quesada.
The adjective “dialethic” was first used in this context by Richard Routley.
In fact, the algebraic strong completeness theorem holds for relevance logics only if the deducibility relation at issue is not the “relevant” deducibility relation, but a rephrasing of the classical one. On this subject, see also Chapters 2 and 6.
More reasons for dropping contraction are mentioned and discussed in Restall (1994a): according to him, in fact, contraction-free logics can be applied - inter alia - to an analysis of vagueness, to issues arising in the logic of actions, and to model a notion of “information flow”
De interpretation, 9, 19a.
See Chapter 2. There are however some exceptions: for instance the logic RM on which we shall return, is a substructural logic, but its disjunctions and conjunctions (both the lattice-theoretical and the group-theoretical ones) are idempotent.
For a philosophical defence of contraction-free systems of naive set theory, see Weir (1998).
Once again, some kind of distrust in the virtues of exchange can be traced back to the antiquity (Casari 1997a). Sextus Empiricus, in fact, came up with some counterexamples to premiss exchange in the context of his discussion of changing arguments (.sEtianf wtiovties λóyot).
We shall return to these issues in Appendix B. The original Lambek calculus placed further restrictions on the → R and ← R rules, which we shall disregard until then.
The expression “formulae-as-types” stems from the fact that in the Curry-Howard isomorphism proofs are named by terms of the λ-calculus, and formulae are viewed as the types of such terms: two terms with the same type are like two proofs of the same formula.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Paoli, F. (2002). The Role of Structural Rules in Sequent Calculi. In: Substructural Logics: A Primer. Trends in Logic, vol 13. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-3179-9_1
Download citation
DOI: https://doi.org/10.1007/978-94-017-3179-9_1
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6014-3
Online ISBN: 978-94-017-3179-9
eBook Packages: Springer Book Archive