Results for 'Cut-Elimination'

999 found
Order:
  1.  15
    Cut Elimination for GLS Using the Terminability of its Regress Process.Jude Brighton - 2016 - Journal of Philosophical Logic 45 (2):147-153.
    The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  2.  21
    Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.
    A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3.  13
    The Role of Quantifier Alternations in Cut Elimination.Philipp Gerhardy - 2005 - Notre Dame Journal of Formal Logic 46 (2):165-171.
    Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  4.  24
    Cut-Elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  10
    Cut-Elimination: Syntax and Semantics.M. Baaz & A. Leitsch - 2014 - Studia Logica 102 (6):1217-1244.
    In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  23
    A Proof-Theoretic Treatment of Λ-Reduction with Cut-Elimination: Λ-Calculus as a Logic Programming Language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
    We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  16
    Effective Cut-Elimination for a Fragment of Modal Mu-Calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
    A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  81
    Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
    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.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  17
    Cut‐Elimination Theorem for the Logic of Constant Domains.Ryo Kashima & Tatsuya Shimura - 1994 - Mathematical Logic Quarterly 40 (2):153-172.
    The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  10.  14
    Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
    This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  34
    A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
    We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  12.  8
    Cut-Elimination Theorems of Some Infinitary Modal Logics.Yoshihito Tanaka - 2001 - Mathematical Logic Quarterly 47 (3):327-340.
    In this article, a cut-free system TLMω1 for infinitary propositional modal logic is proposed which is complete with respect to the class of all Kripke frames.The system TLMω1 is a kind of Gentzen style sequent calculus, but a sequent of TLMω1 is defined as a finite tree of sequents in a standard sense. We prove the cut-elimination theorem for TLMω1 via its Kripke completeness.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  13.  24
    Hypersequent Calculi for S5: The Methods of Cut Elimination.Kaja Bednarska & Andrzej Indrzejczak - 2015 - Logic and Logical Philosophy 24 (3):277–311.
  14.  10
    Cut Elimination for Propositional Dynamic Logic Without.Robert A. Bull - 1992 - Mathematical Logic Quarterly 38 (1):85-100.
  15.  38
    Algebraic Aspects of Cut Elimination.Francesco Belardinelli, Peter Jipsen & Hiroakira Ono - 2004 - Studia Logica 77 (2):209 - 240.
    We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  16.  49
    Algebraic Proofs of Cut Elimination.Jeremy Avigad - manuscript
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  17. Cut-Elimination and Quantification in Canonical Systems.Anna Zamansky & Arnon Avron - 2006 - Studia Logica 82 (1):157-176.
    Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  18.  22
    Interpolants, Cut Elimination and Flow Graphs for the Propositional Calculus.Alessandra Carbone - 1997 - Annals of Pure and Applied Logic 83 (3):249-299.
    We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  19.  46
    Valentini’s Cut-Elimination for Provability Logic Resolved.Rajeev Goré & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
    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 (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  20.  17
    Cut Elimination and Strong Separation for Substructural Logics: An Algebraic Approach.Nikolaos Galatos & Hiroakira Ono - 2010 - Annals of Pure and Applied Logic 161 (9):1097-1133.
    We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  21.  27
    Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection.Toshiyasu Arai - 1998 - Annals of Pure and Applied Logic 95 (1-3):93-184.
    We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  22.  15
    Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate.Paolo Maffezioli & Eugenio Orlandelli - 2019 - Bulletin of the Section of Logic 48 (2):137-158.
    In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and overcome the failure of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23.  20
    Which Structural Rules Admit Cut Elimination? An Algebraic Criterion.Kazushige Terui - 2007 - Journal of Symbolic Logic 72 (3):738 - 754.
    Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  24.  13
    Syntactic Cut-Elimination for Common Knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.
    We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  25.  18
    Sufficient Conditions for Cut Elimination with Complexity Analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1):81-99.
    Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  26.  31
    Towards a Semantic Characterization of Cut-Elimination.Agata Ciabattoni & Kazushige Terui - 2006 - Studia Logica 82 (1):95-119.
    We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  27.  17
    Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus.Kai Brünnler & Thomas Studer - 2012 - Annals of Pure and Applied Logic 163 (12):1838-1853.
    For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  28.  16
    Quick Cut-Elimination for Strictly Positive Cuts.Toshiyasu Arai - 2011 - Annals of Pure and Applied Logic 162 (10):807-815.
    In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  29.  21
    Cut Elimination for Entailment Relations.Davide Rinaldi & Daniel Wessel - 2019 - Archive for Mathematical Logic 58 (5-6):605-625.
    Entailment relations, introduced by Scott in the early 1970s, provide an abstract generalisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  30.  12
    Cut Elimination for a Simple Formulation of Epsilon Calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
    A simple cut elimination proof for arithmetic with the epsilon symbol is used to establish the termination of a modified epsilon substitution process. This opens a possibility of extension to much stronger systems.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  31.  4
    Call-by-Name Reduction and Cut-Elimination in Classical Logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1-3):38-65.
    We present a version of Herbelin’s image-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λμ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β,μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the “ cut=redex” paradigm. We show that the underlying untyped calculus (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  32.  12
    A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
    A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  33.  43
    Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
    We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  34.  13
    Completeness and Cut-Elimination Theorems for Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2011 - Annals of Pure and Applied Logic 162 (10):816-835.
    A sequent calculus for Odintsov’s Hilbert-style axiomatization of a logic related to the trilattice SIXTEEN3 of generalized truth values is introduced. The completeness theorem w.r.t. a simple semantics for is proved using Maehara’s decomposition method that simultaneously derives the cut-elimination theorem for . A first-order extension of and its semantics are also introduced. The completeness and cut-elimination theorems for are proved using Schütte’s method.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35.  20
    A Cut-Elimination Proof in Intuitionistic Predicate Logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
    In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  36.  8
    On the Non-Confluence of Cut-Elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.
    We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37.  7
    Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.Norihiro Kamide & Yoni Zohar - forthcoming - Studia Logica:1-23.
    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 known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  38.  50
    Cut Elimination Inside a Deep Inference System for Classical Predicate Logic.Kai Brünnler - 2006 - Studia Logica 82 (1):51-71.
    Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  39.  40
    Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66.
    We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  40.  45
    Cut Elimination for S4C: A Case Study.Grigori Mints - 2006 - Studia Logica 82 (1):121-132.
    S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  41.  12
    Epsilon Substitution for $$\Textit{ID}_1$$ ID 1 Via Cut-Elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.
    The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42.  39
    Cut Elimination for a Calculus with Context-Dependent Rules.Birgit Elbl - 2001 - Archive for Mathematical Logic 40 (3):167-188.
    Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  43.  2
    Cut Elimination in Hypersequent Calculus for Some Logics of Linear Time.Andrzej Indrzejczak - 2019 - Review of Symbolic Logic 12 (4):806-822.
    This is a sequel article to [10] where a hypersequent calculus for some temporal logics of linear frames including Kt4.3 and its extensions for dense and serial flow of time was investigated in detail. A distinctive feature of this approach is that hypersequents are noncommutative, i.e., they are finite lists of sequents in contrast to other hypersequent approaches using sets or multisets. Such a system in [10] was proved to be cut-free HC formalization of respective logics by means of semantical (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44.  4
    Strong Cut-Elimination for Constant Domain First-Order S5.Heinrich Wansing - 1995 - Logic Journal of the IGPL 3 (5):797-810.
    We consider a labelled tableau presentation of constant domain first-order S5 and prove a strong cut-elimination theorem.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  45.  5
    Cut Elimination for the Unified Logic.Jacqueline Vauzeilles - 1993 - Annals of Pure and Applied Logic 62 (1):1-16.
    Vauzeilles, J., Cut elimination for the Unified Logic, Annals of Pure and Applied Logic 62 1-16. In the paper entitled “On the Unity of Logic” Girard introduced and motivated the system LU. In Girard's article, the cut-elimination result for LU is stated and used as a key lemma, but not supported by any rigourous proof. In the present paper, we prove that LU enjoys cut elimination under minimal hypotheses: a notion of degree for a formula is introduced, which depends (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  46. Strong Cut-Elimination In Display Logic.Heinrich Wansing - 1995 - Reports on Mathematical Logic:117-131.
    It is shown that every displayable propositional logic enjoys strong cut-elimination. This result strengthens Belnap's general cut-elimination theorem for Display Logic.
     
    Export citation  
     
    Bookmark   1 citation  
  47.  6
    Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics.Adam Přenosil - 2017 - Studia Logica 105 (6):1255-1289.
    We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  48.  4
    Strong Cut-Elimination in Sequent Calculus Using Klop's Ι-Translation and Perpetual Reductions.Heine Sørensen Morten & Urzyczyn Paweł - 2008 - Journal of Symbolic Logic 73 (3):919-932.
    There is a simple technique, due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop’s ι-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings; it (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  49. Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.Arnon Avron - unknown
    An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...)
     
    Export citation  
     
    Bookmark  
  50. A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.Arnon Avron & Anna Zamansky - unknown
    An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...)
     
    Export citation  
     
    Bookmark  
1 — 50 / 999