There is a natural story about what logic is that sees it as tied up with two operations: a ‘throw things into a bag’ operation and a ‘closure’ operation. In a pair of recent papers, Jc Beall has fleshed out the account of logic this leaves us with in more detail. Using Beall’s exposition as a guide, this paper points out some problems with taking the second operation to be closure in the usual sense. After pointing out these problems, I (...) then turn to fixing them in a restricted case and modulo a few simplifying assumptions. In a followup paper, the simplifications and restrictions will be removed. (shrink)

Hyperlogic is a hyperintensional system designed to regiment metalogical claims (e.g., “Intuitionistic logic is correct” or “The law of excluded middle holds”) into the object language, including within embedded environments such as attitude reports and counterfactuals. This paper is the first of a two-part series exploring the logic of hyperlogic. This part presents a minimal logic of hyperlogic and proves its completeness. It consists of two interdefined axiomatic systems: one for classical consequence (truth preservation under a classical interpretation of the (...) connectives) and one for “universal” consequence (truth preservation under any interpretation). The sequel to this paper explores stronger logics that are sound and complete over various restricted classes of models as well as languages with hyperintensional operators. (shrink)

This paper recalls some applications of two-dimensional modal logic from the 1980s, including work on the logic of Actually and on a somewhat idealized version of the indicative/subjunctive distinction, as well as on absolute and relative necessity. There is some discussion of reactions this material has aroused in commentators since. We also survey related work by Leslie Tharp from roughly the same period.

In this paper, I distinguish different kinds of pluralism about logical consequence. In particular, I distinguish the pluralism about logic arising from Carnap’s Principle of Tolerance from a pluralism which maintains that there are different, equally “good” logical consequence relations on the one language. I will argue that this second form of pluralism does more justice to the contemporary state of logical theory and practice than does Carnap’s more moderate pluralism.

I discuss paradoxes of implication in the setting of a proof-conditional theory of meaning for logical constants. I argue that a proper logic of implication should be not only relevant, but also constructive and nonmonotonic. This leads me to select as a plausible candidate LL, a fragment of linear logic that differs from R in that it rejects both contraction and distribution.

In this paper, a family of paraconsistent propositional logics with constructive negation, constructive implication, and constructive co-implication is introduced. Although some fragments of these logics are known from the literature and although these logics emerge quite naturally, it seems that none of them has been considered so far. A relational possible worlds semantics as well as sound and complete display sequent calculi for the logics under consideration are presented.

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and (...) contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural (...) rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated in terms (...) of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

This paper deals with a collection of concerns that, over a period of time, led the author away from the Routley–Meyer semantics, and towards proof- theoretic approaches to relevant logics, and indeed to the weak relevant logic MC of meaning containment.

We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic (...) logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers ∀ new and ∃ new which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels. (shrink)

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

In some logics, anything whatsoever follows from a contradiction; call these logics explosive. Paraconsistent logics are logics that are not explosive. Paraconsistent logics have a long and fruitful history, and no doubt a long and fruitful future. To give some sense of the situation, I’ll spend Section 1 exploring exactly what it takes for a logic to be paraconsistent. It will emerge that there is considerable open texture to the idea. In Section 2, I’ll give some examples of techniques for (...) developing paraconsistent logics. In Section 3, I’ll discuss what seem to me to be some promising applications of certain paraconsistent logics. In fact, however, I don’t think there’s all that much to the concept ‘paraconsistent’ itself; the collection of paraconsistent logics is far too heterogenous to be very productively dealt with under a single label. Perhaps that will emerge as we go. (shrink)

The standard inferentialist approaches to modal logic tend to suffer from not being able to uniquely characterize the modal operators, require that introduction and elimination rules be interdefined, or rely on the introduction of possible-world like indexes into the object language itself. In this paper I introduce a hypersequent calculus that is flexible enough to capture many of the standard modal logics and does not suffer from the above problems. It is therefore an ideal candidate to underwrite an inferentialist theory (...) of meaning for modal operators. Here I treat specifically the modal logics K, D, T, S4, B, and S5. I show that the calculi are adequate for each set of models, and show that they meet a large set of criteria that are generally thought necessary for a calculus to underwrite a theory of meaning. (shrink)

In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems (...) for classical logic and Girard's proofnets for linear logic. (shrink)

Dave Ripley has recently argued against the plausibility of multiset consequence relations and of contraction-free approaches to paradox. For Ripley, who endorses a nontransitive theory, the best arguments that buttress transitivity also push for contraction—whence it is wiser for the substructural logician to go nontransitive from the start. One of Ripley’s allegations is especially insidious, since it assumes the form of a trivialisation result: it is shown that if a multiset consequence relation can be associated to a closure operator in (...) the expected way, then it necessarily contracts. We counter Ripley’s objection by presenting an approach to multiset consequence that escapes this trap. This approach is multiple-conclusioned in a heterodox way, for multiple succedents are given a conjunctive, rather than a disjunctive reading. Finally, we address a further objection by French and Ripley to the effect that the informational interpretation of sequents in linear logic does not motivate cut. (shrink)

Information is a notion of wide use and great intuitive appeal, and hence, not surprisingly, different formal paradigms claim part of it, from Shannon channel theory to Kolmogorov complexity. Information is also a widely used term in logic, but a similar diversity repeats itself: there are several competing logical accounts of this notion, ranging from semantic to syntactic. In this chapter, we will discuss three major logical accounts of information.

Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which differs again (...) in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented as (...) encodings of Kripke-style formulations. (shrink)

In this paper we compare grammatical inference in the context of simple and of mixed Lambek systems. Simple Lambek systems are obtained by taking the logic of residuation for a family of multiplicative connectives /,,\, together with a package of structural postulates characterizing the resource management properties of the connective.Different choices for Associativity and Commutativity yield the familiar logics NL, L, NLP, LP. Semantically, a simple Lambek system is a unimodal logic: the connectives get a Kripke style interpretation in terms (...) of a single ternary accessibility relation modeling the notion of linguistic composition for each individual system.The simple systems earch have their virtues in linguistic analysis. But none of them in isolation provides a basis for a full theory of grammar. In the second part of the paper, we consider two types of mixed Lambek systems. (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 substructural logics.

This paper presents an overview of the methods of hypersequents and display sequents in the proof theory of non-classical logics. In contrast with existing surveys dedicated to hypersequent calculi or to display calculi, our aim is to provide a unified perspective on these two formalisms highlighting their differences and similarities and discussing applications and recent results connecting and comparing them.

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)

The aim of this paper is to provide a proof-theoretic characterization of relevant logics including fusion and fission connectives, as well as Ackermann’s truth constant. We achieve this by employing the well-established methodology of labelled sequent calculi. After having introduced several systems, we will conduct a detailed proof-theoretic analysis, show a cut-admissibility theorem, and establish soundness and completeness. The paper ends with a discussion that contextualizes our current work within the broader landscape of the proof theory of relevant logics.

Dialogical logic is a game-theoretical approach to logic. Logic is studied with the help of certain games, which can be thought of as idealized argumentations. Two players, the Proponent, who puts forward the initial thesis and tries to defend it, and the Opponent, who tries to attack the Proponent’s thesis, alternately utter argumentative moves according to certain rules. For a long time the dialogical approach had been worked out only for classical and intuitionistic logic. The seven papers of this dissertation (...) show that this narrowness was uncalled for. The initial paper presents an overview and serves as an introduction to the other papers. Those papers are related by one central theme. As each of them presents dialogical formulations of a different non-classical logic, they show that dialogical logic constitutes a powerful and flexible general framework for the development and study of various logical formalisms and combinations thereof. As such it is especially attractive to logical pluralists that reject the idea of “the single correct logic”. The collection contains treatments of free logic, modal logic, relevance logic, connexive logic, linear logic, and multi-valued logic. (shrink)

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and (...) proof normalization. We have implemented our work in the Isabelle Logical Framework. (shrink)

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

In this paper we introduce and compare four different syntactic methods for generating sequent calculi for the main systems of modal logic: the multiple sequents method, the higher-arity sequents method, the tree-hypersequents method and the display method. More precisely we show how the first three methods can all be translated in the fourth one. This result sheds new light on these generalisations of the sequent calculus and raises issues that will be examined in the last section.

In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly (...) beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination. (shrink)

Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and (...) provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents. (shrink)

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of p roofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

This paper deals with the question of the logicality of modal logics from a proof-theoretic perspective. It is argued that if Dos̆en’s analysis of logical constants as punctuation marks is embraced, it is possible to show that all the modalities in the cube of normal modal logics are indeed logical constants. It will be proved that the display calculus for each displayable modality admits a purely structural presentation based on double-line rules which, following Dos̆en’s analysis, allows us to claim that (...) the corresponding modal operators are logical constants. (shrink)

Restall :279–291, 2014) proposes a new, proof-theoretic, logical pluralism. This is in contrast to the model-theoretic pluralism he and Beall proposed in Beall and Restall :475–493, 2000) and in Beall and Restall. What I will show is that Restall has not described the conditions on being admissible to the proof-theoretic logical pluralism in such a way that relevance logic is one of the admissible logics. Though relevance logic is not hard to add formally, one critical component of Restall’s pluralism is (...) that the relevance logic that gets added must have connectives which mean the same thing as the connectives in the already admitted logic. This is what I will show is not possible. (shrink)

In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There is (...) often an underly ing assumption that the move to a proof of cut elimination for sequents built from multisets is easy. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of GLSV with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut elimination for GL in a multiset setting. Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut elimination for sequents built from multisets. The formal setting is particularly important for sequents built from multisets, in order to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is diffi cult to verify the correctness of his induction argument based on “width”. In our formulation however, verification of the induction argument is straight forward. Finally, the multiset setting also introduces a new complication in the the case of contractions above cut when the cut formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments. Finally, we show that the algorithm purporting to show the non termi nation of Valentini’s arguments is not a faithful representation of the original arguments, but is instead a transformation already known to be insufficient. (shrink)

The paper is a brief survey of some sequent calculi which do not follow strictly the shape of sequent calculus introduced by Gentzen. We propose the following rough classification of all SC: Systems which are based on some deviations from the ordinary notion of a sequent are called generalised; remaining ones are called ordinary. Among the latter we distinguish three types according to the proportion between the number of primitive sequents and rules. In particular, in one of these types, called (...) Gentzen’s type, we have a subtype of standard SC due to Gentzen. Hence by nonstandard ones we mean all these ordinary SC where other kinds of rules are applied than those admitted in standard Gentzen’s sequent calculi. We describe briefly some of the most interesting or important nonstandard SC belonging to the three abovementioned types. (shrink)

It is shown that the constructive four-valued logic N4 can be faithfully embedded into the modal logic S4. This embedding is used to obtain complete, cut-free display sequent calculi for N4 and C4, the modal logic of consistency over N4. C4 is a natural monotonic base system for semantics-based non-monotonic reasoning.