Bunched sequential information

It is known that the logic BI of bunched implications is a logic of resources. Many studies have reported on the applications of BI to computer science. In this paper, an extension BIS of BI by adding a sequence modal operator is introduced and studied in order to formalize more fine-grained resource-sensitive reasoning. By the sequence modal operator of BIS, we can appropriately express “sequential information” in resource-sensitive reasoning. A Gentzen-type sequent calculus SBIS for BIS is introduced, and the cut-elimination and decidability theorems for SBIS are proved. An extension of the Grothendieck topological semantics for BI is introduced for BIS, and the completeness theorem with respect to this semantics is proved. The cut-elimination, decidability and completeness theorems for SBIS and BIS are proved using some theorems for embedding BIS into BI.     

Cut-elimination for Weak Grzegorczyk Logic Go

We present a syntactic proof of cut-elimination for weak Grzegorczyk logic Go. The logic has a syntactically similar axiomatisation to Gödel–Löb logic GL (provability logic) and Grzegorczyk’s logic Grz. Semantically, GL can be viewed as the irreflexive counterpart of Go, and Grz can be viewed as the reflexive counterpart of Go. Although proofs of syntactic cut-elimination for GL and Grz have appeared in the literature, this is the first proof of syntactic cut-elimination for Go. The proof is technically interesting, requiring a deeper analysis of the derivation structures than the proofs for GL and Grz. New transformations generalising the transformations for GL and Grz are developed here.     

Proof Theory of Paraconsistent Quantum Logic

Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is addressed.     

Synchronized Linear-Time Temporal Logic

A new combined temporal logic called synchronized linear-time temporal logic (SLTL) is introduced as a Gentzen-type sequent calculus. SLTL can represent the n-Cartesian product of the set of natural numbers. The cut-elimination and completeness theorems for SLTL are proved. Moreover, a display sequent calculus ??SLTL is defined.     

A linear conservative extension of Zermelo-Fraenkel set theory

In this paper, we develop the system LZF of set theory with the unrestricted comprehension in full linear logic and show that LZF is a conservative extension of ZF^– i.e., the Zermelo-Fraenkel set theory without the axiom of regularity. We formulate LZF as a sequent calculus with abstraction terms and prove the partial cut-elimination theorem for it. The cut-elimination result ensures the subterm property for those formulas which contain only terms corresponding to sets in ZF^–. This implies that LZF is a conservative extension of ZF^– and therefore the former is consistent relative to the latter. Hiroakira Ono     

Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic

Studia Logica - In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic...     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.     

A note on the proof theory the λII-calculus

The II-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the II-calculus and prove the cut-elimination theorem.The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus.We consider an application of the cut-free calculus, via the subformula property, to proof-search in the II-calculus. For this application, the normalization result for the natural deduction calculus alone is inadequate, a (cut-free) calculus with the subformula property being required.This paper was written whilst the author was affiliated to the University of Edinburgh, Scotland, U.K. and revised for publication whilst he was affiliated to the University of Birmingham, England, U.K.Presented byDaniele Mundici     

Substructural Implicational Logics Including the Relevant Logic E

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic logic. This revised version was published online in June 2006 with corrections to the Cover Date.     

Type Logics and Pregroups

We discuss the logic of pregroups, introduced by Lambek [34], and its connections with other type logics and formal grammars. The paper contains some new ideas and results: the cut-elimination theorem and a normalization theorem for an extended system of this logic, its P-TIME decidability, its interpretation in L1, and a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid. Special Issue Categorial Grammars and Pregroups Edited by Wojciech Buszkowski and Anne Preller     

Cut elimination for a logic with induction and co-induction

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof-theoretic (rather than set-theoretic) notion of definition (Hallnäs, 1991 [18], Eriksson, 1991 [11], Schroeder-Heister, 1993 [38], McDowell and Miller, 2000 [22]). Definitions are akin to logic programs, where the left and right rules for defined atoms allow one to view theories as “closed” or defining fixed points. The use of definitions and free equality makes it possible to reason intensionally about syntax. We add in a consistent way rules for pre- and post-fixed points, thus allowing the user to reason inductively and co-inductively about properties of computational system making full use of higher-order abstract syntax. Consistency is guaranteed via cut-elimination, where we give a direct cut-elimination procedure in the presence of general inductive and co-inductive definitions via the parametric reducibility technique.     

Indexed systems of sequents and cut-elimination

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 (cut-elimination) 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 of the systems considered can be presented as encodings of Kripke-style formulations.     

Proof Systems Combining Classical and Paraconsistent Negations

New propositional and first-order paraconsistent logics (called L _ω and FL _ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L _ω and FL _ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L _ω and FL _ω are proved. The cut-elimination theorems for L _ω and FL _ω are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems. Presented by Yaroslav Shramko and Heinrich Wansing     

Intuitionistic Games: Determinacy,Completeness, and Normalization

We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg’s implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player,  ?ros, is trying to construct a proof in normal form (positions in the game represent his progress in proof construction) while his opponent, ?phrodite,  attempts to build a counter-model (positions or plays can be seen as states in a Kripke model). The determinacy of the game (a proof-construction and a model-construction game in one) implies therefore both completeness and semantic cut-elimination.     

Gentzen-type formulation of the prepositional logic LQ

We give a Gentzen-type formulation GQ for the intermediate logic LQ and prove the cut-elimination theorem on it, where LQ is the propositional logic obtained from the intuitionistic propositional logic LI by adding the axioms of the form AV A.     

The Epsilon Calculus and Herbrand Complexity

Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator e _x . Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.     

Hybrid Probabilistic Logic Programs as Residuated Logic Programs

In this paper we show the embedding of Hybrid Probabilistic Logic Programs into the rather general framework of Residuated Logic Programs, where the main results of (definite) logic programming are validly extrapolated, namely the extension of the immediate consequences operator of van Emden and Kowalski. The importance of this result is that for the first time a framework encompassing several quite distinct logic programming semantics is described, namely Generalized Annotated Logic Programs, Fuzzy Logic Programming, Hybrid Probabilistic Logic Programs, and Possibilistic Logic Programming. Moreover, the embedding provides a more general semantical structure paving the way for defining paraconsistent probabilistic reasoning with a logic programming semantics.     

Gentzen-Style Sequent Calculus for Semi-intuitionistic Logic

The variety \({\mathcal{SH}}\) of semi-Heyting algebras was introduced by H. P. Sankappanavar (in: Proceedings of the 9th “Dr. Antonio A. R. Monteiro” Congress, Universidad Nacional del Sur, Bahía Blanca, 2008) [13] as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic HsH, known as semi-intuitionistic logic, which is equivalent to the one defined by a Hilbert style calculus in Cornejo (Studia Logica 98(1–2):9–25, 2011) [6]. In this article we introduce a Gentzen style sequent calculus GsH for the semi-intuitionistic logic whose associated logic GsH is the same as HsH. The advantage of this presentation of the logic is that we can prove a cut-elimination theorem for GsH that allows us to prove the decidability of the logic. As a direct consequence, we also obtain the decidability of the equational theory of semi-Heyting algebras.     

Sequent-systems and groupoid models. I

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.     

Sequent-systems and groupoid models. II

The purpose of this paper is to connect the proof theory and the model theory of a family of prepositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related to BCK 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, Hilbert-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.Below is the sequel to the first part of the paper, which appeared in the previous issue of this journal (vol. 47 (1988), pp. 353–386). The first part contained sections on sequent-systems and Hilbert-formulations, and here is the third section on groupoid models. This second part is meant to be read in conjunction with the first part.