The aim of the present book is to give a comprehensive account of the ‘state of the art’ of substructurallogics, focusing both on their proof theory and on their semantics (both algebraic and relational. It is for graduate students in either philosophy, mathematics, theoretical computer science or theoretical linguistics as well as specialists and researchers.
When discussing Logical Pluralism several critics argue that such an open-minded position is untenable. The key to this conclusion is that, given a number of widely accepted assumptions, the pluralist view collapses into Logical Monism. In this paper we show that the arguments usually employed to arrive at this conclusion do not work. The main reason for this is the existence of certain substructurallogics which have the same set of valid inferences as Classical Logic—although they are, in (...) a clear sense, non-identical to it. We argue that this phenomenon can be generalized, given the existence of logics which coincide with Classical Logic regarding a number of metainferential levels—although they are, again, clearly different systems. We claim this highlights the need to arrive at a more refined version of the Collapse Argument, which we discuss at the end of the paper. (shrink)
The new area of logic and computation is now undergoing rapid development. This has affected the social pattern of research in the area. A new topic may rise very quickly with a significant body of research around it. The community, however, cannot wait the traditional two years for a book to appear. This has given greater importance to thematic collections of papers, centred around a topic and addressing it from several points of view, usually as a result of a workshop, (...) summer school, or just a scientific initiative. Such a collection may not be as coherent as a book by one or two authors yet it is more focused than a collection of key papers on a certain topic. It is best thought of as a thematic collection, a study in the area of logic and computation. The new series Studies in Logic and Computation is intended to provide a home for such thematic collections. Substructurallogics are nonclassical logics, which arose in response to problems in foundations of mathematics and logic, theoretical computer science, mathematical linguistics, and category theory. They include intuitionistic logic, relevant logic, BCK logic, linear logic, and Lambek's calculus of syntactic categories. Substructurallogics differ from classical logics, and from each other, in their presuppositions about Gentzen's structural rules, although their presuppositions about the deductive role of logical constants are invariant. Substructurallogics have been a subject of study for logicians during the last sixty years. Specialists have often worked in isolation, however, largely unaware of the contributions of others. This book brings together new papers by some of the most eminent authorities in these varioustraditions to produce a unified view of substructurallogics. (shrink)
This book introduces an important group of logics that have come to be known under the umbrella term 'susbstructural'. Substructurallogics have independently led to significant developments in philosophy, computing and linguistics. _An Introduction to Substrucural Logics_ is the first book to systematically survey the new results and the significant impact that this class of logics has had on a wide range of fields.The following topics are covered: * Proof Theory * Propositional Structures * Frames * (...) Decidability * Coda Both students and professors of philosophy, computing, linguistics, and mathematics will find this to be an important addition to their reading. (shrink)
Substructurallogics extending the full Lambek calculus FL have largely benefited from a systematical algebraic approach based on the study of their algebraic counterparts: residuated lattices. Recently, a nonassociative generalization of FL has been studied by Galatos and Ono as the logic of lattice-ordered residuated unital groupoids. This paper is based on an alternative Hilbert-style presentation for SL which is almost MP -based. This presentation is then used to obtain, in a uniform way applicable to most substructural (...)logics, a form of local deduction theorem, description of filter generation, and proper forms of generalized disjunctions. A special stress is put on semilinear substructurallogics. Axiomatizations of the weakest semilinear logic over SL and other prominent substructurallogics are provided and their completeness with respect to chains defined over the real unit interval is proved. (shrink)
ABSTRACT My aim in this paper is to present a pluralist thesis about the inferential role of logical constants, which embraces classical, relevant, linear and ordered logic. That is, I defend that a logical constant c has more than one correct inferential role. The thesis depends on a particular interpretation of substructurallogics' vocabulary, according to which classical logic captures the literal meaning of logical constants and substructurallogics encode a pragmatically enriched sense of those connectives. (...) The paper is divided into four parts: first, I introduce the motivation for the pluralist thesis of the paper; second I introduce the calculus for the different logics endorsed in the pluralist thesis; third, I motivate how the different behaviors of the logical vocabulary of these logics can be pragmatically interpreted, and fourth, I motivate how the different inferential roles that each substructural logic attribute to logical constants can coexist, and how we should reason with a logical constant c given this plurality. (shrink)
A mechanism for combining any two substructurallogics (e.g. linear and intuitionistic logics) is studied from a proof-theoretic point of view. The main results presented are cut-elimination and simulation results for these combined logics called synthesized substructurallogics.
We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FLm (full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm (Lambek calculuswith restricted mingle).
The Craig interpolation property is investigated for substructurallogics whose algebraic semantics are varieties of semilinear pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R-mingle with unit” logic that have the Craig interpolation property. This latter characterization is obtained using a model-theoretic quantifier elimination strategy to determine the varieties (...) of Sugihara monoids admitting the amalgamation property. (shrink)
Hereditary structural completeness is established for a range of substructurallogics, mainly without the weakening rule, including fragments of various relevant or many-valued logics. Also, structural completeness is disproved for a range of systems, settling some previously open questions.
Substructurallogics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructurallogics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings (...) into analogues of S4 are obtained with the help of cut elimination for sequent formulations of our substructurallogics and their modal extensions. These results are proved for systems with equality too. (shrink)
In this paper, we establish the first-order definability of sequents with consistent variable occurrence on bi-approximation semantics by means of the Sahlqvist–van Benthem algorithm. Then together with the canonicity results in Suzuki (2011), this allows us to establish a Sahlqvist theorem for substructural logic. Our result is not limited to substructural logic but is also easily applicable to other lattice-based logics.
We introduce Kripke semantics for modal substructurallogics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructurallogics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics.
This essay is structured around the bifurcation between proofs and models: The first section discusses Proof Theory of relevant and substructurallogics, and the second covers the Model Theory of these logics. This order is a natural one for a history of relevant and substructurallogics, because much of the initial work — especially in the Anderson–Belnap tradition of relevant logics — started by developing proof theory. The model theory of relevant logic came some (...) time later. As we will see, Dunn’s algebraic models [76, 77] Urquhart’s operational semantics [267, 268] and Routley and Meyer’s relational semantics [239, 240, 241] arrived decades after the initial burst of activity from Alan Anderson and Nuel Belnap. The same goes for work on the Lambek calculus: although inspired by a very particular application in linguistic typing, it was developed first proof-theoretically, and only later did model theory come to the fore. Girard’s linear logic is a different story: it was discovered though considerations of the categorical models of coherence.. (shrink)
Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic. However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modified proof theory which more closely models relevant logics. In addition, we use this proof theory to show decidability for a large range of substructurallogics.
It is well known that classical propositional logic can be interpreted in intuitionistic propositional logic. In particular Glivenko's theorem states that a formula is provable in the former iff its double negation is provable in the latter. We extend Glivenko's theorem and show that for every involutive substructural logic there exists a minimum substructural logic that contains the first via a double negation interpretation. Our presentation is algebraic and is formulated in the context of residuated lattices. In the (...) last part of the paper, we also discuss some extended forms of the Kolmogorov translation and we compare it to the Glivenko translation. (shrink)
ABSTRACTIn an article dating back in 1992, Kosta Došen initiated a project of modal translations in substructurallogics, aiming at generalising the well-known Gödel–McKinsey–Tarski translation of intuitionistic logic into S4. Došen's translation worked well for BCI and stronger systems, but not for systems below BCI. Dropping structural rules results in logic systems without distribution. In this article, we show, via translation, that every substructural logic is a fragment of a corresponding sorted, residuated modal logic. At the conceptual (...) and philosophical level, the translation provides a classical interpretation of the meaning of the logical operators of various non-distributive propositional calculi. Technically, it allows for an effortless transfer of results, such as compactness and the Löwenheim-Skolem property and it opens up new directions for deducing properties of substructural logic systems by establishing appropriate transfer theorems. (shrink)
We characterize the non-trivial substructurallogics having the variable sharing property as well as its strong version. To this end, we find the algebraic counterparts over varieties of these logical properties. -/- .
We introduce modal propositional substructurallogics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.
This paper briefly overviews some of the results and research directions. In the area of substructurallogics from the last couple of decades. Substructurallogics are understood here to include relevance logics, linear logic, variants of Lambek calculi and some other logics that are motivated by the idea of omitting some structural rules or making other structural changes in LK, the original sequent calculus for classical logic.
The dissertation deals with problems in "logic", more precisely, it deals with particular formal systems aiming at capturing patterns of valid reasoning. Sequent calculi were proposed to characterize logical connectives via introduction rules. These systems customarily also have structural rules which allow one to rearrange the set of premises and conclusions. In the "structurally free logic" of Dunn and Meyer the structural rules are replaced by combinatory rules which allow the same reshuffling of formulae, and additionally introduce an explicit marker (...) for the application of the rule---the combinator. The dissertation gives syntactic extensions of such systems introducing conjunction and disjunction . Cut elimination is proved for these systems. ;Syntactic systems as a rule are accompanied by a semantics which interprets them. The extended systems are supplied with semantics using algebraic methods. First, the Lindenbaum algebras are formed, and then these algebras are represented in an algebra of sets. This gives a so called Kripke-style semantics for the systems. The representation for the distributive extension utilizes well-known techniques; it uses sets of prime filters and set theoretical operations on them to deal with conjunction and disjunction, plus a ternary accessibility relation to accommodate the intensional operators as fusion and implication. The representation theorem is proven generally, i.e., for arbitrary sets of combinators using the "squeeze lemma" of Routley and Meyer. ;The non-distributive calculi require a different representation since union and intersection are distributive. Two previous representations for lattices are overviewed, and a modification of the Hartonas-Dunn representation is successfully augmented with the intensional operations. Instead of sets of filters, sets of pairs of minimally inconsistent filters and ideals are used and the representation theorem is proven. The representation results provide soundness and completeness for the systems. The dissertation also investigates properties of dual combinators , proving a series of lemmas about dual combinatory systems not being Church-Rosser and being inconsistent. Combinatorially definable classes of lambda-terms are considered as well. (shrink)
We study filters in residuated structures that are associated with congruence relations (which we call -filters), and develop a semantical theory for general substructurallogics based on the notion of primeness for those filters. We first generalize Stone’s sheaf representation theorem to general substructurallogics and then define the primeness of -filters as being “points” (or stalkers) of the space, the spectrum, on which the representing sheaf is defined. Prime FL-filters will turn out to coincide with (...) truth sets under various well known semantics for certain substructurallogics. We also investigate which structural rules are needed to interpret each connective in terms of prime -filters in the same way as in Kripke or Routley-Meyer semantics. We may consider that the set of the structural rules that each connective needs in this sense reflects the difficulty of giving the meaning of the connective. A surprising discovery is that connectives , ⅋ of linear logic are linearly ordered in terms of the difficulty in this sense. (shrink)
The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL ew (namely, a certain variety of FL ew -algebras) are term equivalent. This answers a longstanding question of Nelson (...) [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL ew. (shrink)
Substructurallogics have received a lot of attention in recent years from the communities of both logic and algebra. We discuss the algebraization of substructurallogics over the full Lambek calculus and their connections to residuated lattices, and establish a weak form of the deduction theorem that is known as parametrized local deduction theorem. Finally, we study certain interpolation properties and explain how they imply the amalgamation property for certain varieties of residuated lattices.
Building on recent work, I present sequent systems for the non-classical logics LP, K3, and FDE with two main virtues. First, derivations closely resemble those in standard Gentzen-style systems. Second, the systems can be obtained by reformulating a classical system using nonstandard sequent structure and simply removing certain structural rules (relatives of exchange and contraction). I clarify two senses in which these logics count as “substructural.”.
This paper contributes to the theory of hybrid substructurallogics, i.e. weak logics given by a Gentzen-style proof theory in which there is only a limited possibility to use structural rules. Following the literature, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this ▽ as a modality, but rather as the meet of the marked formula with a special type (...) Q. In this way we can make the specific structural behaviour of marked formulas more explicit. The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructurallogics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the 'strong' system in the hybrid one. (shrink)
This volume presents the state of the art in the algebraic investigation into substructurallogics. It features papers from the workshop AsubL (Algebra & SubstructuralLogics - Take 6). Held at the University of Cagliari, Italy, this event is part of the framework of the Horizon 2020 Project SYSMICS: SYntax meets Semantics: Methods, Interactions, and Connections in Substructurallogics. -/- Substructurallogics are usually formulated as Gentzen systems that lack one or more (...) structural rules. They have been intensively studied over the past two decades by logicians of various persuasions. These researchers include mathematicians, philosophers, linguists, and computer scientists. Substructurallogics are applicable to the mathematical investigation of such processes as resource-conscious reasoning, approximate reasoning, type-theoretical grammar, and other focal notions in computer science. They also apply to epistemology, economics, and linguistics. The recourse to algebraic methods -- or, better, the fecund interplay of algebra and proof theory -- has proved useful in providing a unifying framework for these investigations. The AsubL series of conferences, in particular, has played an important role in these developments. -/- This collection will appeal to students and researchers with an interest in substructurallogics, abstract algebraic logic, residuated lattices, proof theory, universal algebra, and logical semantics. (shrink)
This paper contributes to the theory of hybrid substructurallogics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way (...) we can make the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructurallogics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)
We give a proof of the finite model property of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL.
Metacompleteness is used to prove properties such as the disjunction property and the existence property in the area of relevant logics. On the other hand, the disjunction property of several basic propositional substructurallogics over FL has been proved using the cut elimination theorem of sequent calculi and algebraic characterization. The present paper shows that Meyer’s metavaluational technique and Slaney’s metavaluational technique can be applied to basic predicate intuitionistic substructurallogics and basic predicate involutive (...) class='Hi'>substructurallogics, respectively. As a corollary of metacompleteness, the disjunction property, the existence property, and the admissibility of certain rules in such logics can be proved. (shrink)
Formal systems seem to come in two general kinds: useful and useless. This is painting things starkly, but the point is important. Formal structures can either be used in interesting and important ways, or they can languish unused and irrelevant. Lewis' modal logics are good examples. The systems S4 and S5 are useful in many different ways. They map out structures that are relevant to a number of different applications. S1, S2 and S3 however, are not so lucky. They (...) are little studied, and used even less. It has become dear that the structures described by S4 and S5 are important in different ways, while the structures described by S1 to S3 are not so important. In this paper, we will see another formal system with a number of different uses. We will examine a substructural logic which is important in a number of different ways. The logic of Peirce monoids, inspired by the logic of relations, is useful in the independent areas of linguistic types and information flow.In what follows I will describe the logic of Peirce monoids in its various guises, sketch out its main properties, and indicate why it is important. As proofs of theorems are readily available elsewhere in the literature, I simply sketch the relevant proofs here, and point the interested reader to where complete proofs can be found. (shrink)
The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew. The main result of Part I of this series [41] shows that the equivalent variety semantics of N and the equivalent variety semantics of NFL ew are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of (...) deductive systems to establish the definitional equivalence of the logics N and NFL ew. It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. (shrink)
Some of the basic substructurallogics are shown by Ono to have the disjunction property (DP) by using cut elimination of sequent calculi for these logics. On the other hand, this syntactic method works only for a limited number of substructurallogics. Here we show that Maksimova's criterion on the DP of superintuitionistic logics can be naturally extended to one on the DP of substructurallogics over FL. By using this, we show (...) the DP for some of the substructurallogics for which syntactic methods don't work well. (shrink)
Some apparently valid arguments crucially rely on context change. To take a kind of example first discussed by Frege, ‘Tomorrow, it’ll be sunny’ taken on a day seems to entail ‘Today, it’s sunny’ taken on the next day, but the first sentence taken on a day sadly does not seem to entail the second sentence taken on the second next day. Mid-argument context change has not been accounted for by the tradition that has extensively studied the distinctive logical properties of (...) context-dependent languages, for that tradition has focussed on arguments whose premises and conclusions are taken at the same context. I first argue for the desiderability of having a logic that accounts for mid-argument context change and I explain how one can informally understand such context change in a standard framework in which the relation of logical consequence holds among sentences. I then propose a family of simple temporal “intercontextual” logics that adequately model the validity of certain arguments in which the context changes. In particular, such logics validate the apparently valid argument in the Fregean example. The logics lack many traditional structural properties (reflexivity, contraction, commutativity etc.) as a consequence of the logical significance acquired by the sequence structure of premises and conclusions. The logics are however strong enough to capture in the form of logical truths all the valid arguments of both classical logic and Kaplan-style “intracontextual” logic. Finally, I extend the framework by introducing new operations into the object language, such as intercontextual conjunction, disjunction and implication, which, contrary to intracontextual conjunction, disjunction and implication, perfectly match the metalinguistic, intercontextual notions of premise combination, conclusion combination and logical consequence by representing their respective two operands as taken at different contexts. (shrink)
The paper provides an alternative interpretation of ‘pair points’, discussed in Beall et al., "On the ternary relation and conditionality", J. of Philosophical Logic 41(3), 595-612. Pair points are seen as points viewed from two different ‘perspectives’ and the latter are explicated in terms of two independent valuations. The interpretation is developed into a semantics using pairs of Kripke models (‘pair models’). It is demonstrated that, if certain conditions are fulfilled, pair models are validity-preserving copies of positive substructural models. (...) This yields a general soundness and completeness result for a variety of (positive) substructurallogics with respect to multimodal Kripke frames with binary accessibility relations. In addition, an epistemic interpretation of pair models is provided. (shrink)
The paper outlines a generalisation of the awareness-based epistemic semantics by Fagin and Halpern. Awareness is construed as a relation between agents and pieces of information instead of formulas. The main motive for introducing the generalisation is that it shows substructurallogics to be a natural component of information-based epistemic logic: substructurallogics can be seen as describing the logical behaviour of pieces of information. Substructural epistemic logics are introduced and some of their properties (...) are discussed. In addition, extensions of substructural epistemic logics invoking group-epistemic and dynamic modalities are sketched. (shrink)
