Results for 'cut elimination'

1000+ found
Order:
  1.  26
    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   1 citation  
  2.  30
    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   3 citations  
  3.  20
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4.  70
    Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
    A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   43 citations  
  5.  19
    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   4 citations  
  6.  23
    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   11 citations  
  7.  26
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  8.  27
    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  
     
    Export citation  
     
    Bookmark   6 citations  
  9.  12
    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   2 citations  
  10.  56
    Normalizability, Cut Eliminability and Paradox.Neil Tennant - 2016 - Synthese 199 (Suppl 3):597-616.
    This is a reply to the considerations advanced by Schroeder-Heister and Tranchini as prima facie problematic for the proof-theoretic criterion of paradoxicality, as originally presented in Tennant and subsequently amended in Tennant. Countering these considerations lends new importance to the parallelized forms of elimination rules in natural deduction.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  11. Cut Elimination in Categories.Kosta Došen - 1999 - Dordrecht, Netherland: Springer.
    Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory have not been explained systematically in terms of proof theory. Here it is shown that these notions, in particular the notion of adjunction, can be formulated in such as way as to be characterised by composition elimination. Among the benefits of these composition-free formulations are syntactical and simple model-theoretical, geometrical decision procedures for the commuting (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  12.  4
    Cut Elimination Theorem for Non-Commutative Hypersequent Calculus.Andrzej Indrzejczak - 2017 - Bulletin of the Section of Logic 46 (1/2).
    Hypersequent calculi can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut (...). (shrink)
    No categories
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  13.  24
    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   2 citations  
  14.  18
    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   6 citations  
  15.  21
    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   7 citations  
  16.  89
    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 (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  17.  12
    Cut Elimination for Propositional Dynamic Logic Without.Robert A. Bull - 1992 - Mathematical Logic Quarterly 38 (1):85-100.
  18.  29
    Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1.
  19.  17
    Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi.Richard Zach - 2021 - Review of Symbolic Logic 14 (3):645-686.
    Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot’s free deduction. The elimination rules are “general,” but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  20.  8
    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 includingKt4.3and 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 argument. In (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  29
    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  
  22.  26
    Cut Elimination for Propositional Dynamic Logic Without.Robert A. Bull - 1992 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 38 (1):85-100.
    Direct download  
     
    Export citation  
     
    Bookmark   10 citations  
  23.  31
    About Cut Elimination for Logics of Common Knowledge.Luca Alberucci & Gerhard Jäger - 2005 - Annals of Pure and Applied Logic 133 (1):73-99.
    The notions of common knowledge or common belief play an important role in several areas of computer science , in philosophy, game theory, artificial intelligence, psychology and many other fields which deal with the interaction within a group of “agents”, agreement or coordinated actions. In the following we will present several deductive systems for common knowledge above epistemic logics –such as K, T, S4 and S5 –with a fixed number of agents. We focus on structural and proof-theoretic properties of these (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  24.  20
    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 (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  22
    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  
  26.  17
    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  
  27. 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   1 citation  
  28.  7
    On Cut-Elimination Arguments for Axiomatic Theories of Truth.Daichi Hayashi - 2022 - Studia Logica 110 (3):785-818.
    As is mentioned in Leigh :845-865, 2015), it is an open problem whether for several axiomatic theories of truth, including Friedman–Sheard theory \ and Kripke–Feferman theory \ :690-716, 1976), there exist cut-elimination arguments that give the upper bounds of their proof-theoretic strengths. In this paper, we give complete cut-elimination results for several well-known axiomatic theories of truth. In particular, we treat the systems \, and \ \\) of Friedman and Sheard’s theories and \.
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  29.  42
    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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  30.  19
    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 (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  25
    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   3 citations  
  32.  59
    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  
  33.  30
    Cut Elimination in a Gentzen-Style Ε-Calculus Without Identity.Linda Wessels - 1976 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 23 (36):527-538.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  34. On Cut Elimination in the Presence of Perice Rule.Lev Gordeev - 1987 - Archive for Mathematical Logic 26 (1):147-164.
     
    Export citation  
     
    Bookmark   5 citations  
  35. Cut Elimination for Systems of Transparent Truth with Restricted Initial Sequents.Carlo Nicolai - manuscript
    The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  36.  42
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  37.  52
    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  
  38.  10
    Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - 2020 - Journal of Philosophical Logic 49 (6):1185-1212.
    Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems (...)
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   2 citations  
  39.  11
    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, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  40.  9
    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  
     
    Export citation  
     
    Bookmark   1 citation  
  41.  53
    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   1 citation  
  42.  14
    Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction.Jan von Plato & Sara Negri - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 269-290.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  43.  44
    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   1 citation  
  44. 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  
  45.  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   8 citations  
  46.  34
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  47.  49
    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. (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  48.  5
    Cut Elimination for a Logic with Induction and Co-Induction.Alwen Tiu & Alberto Momigliano - 2012 - Journal of Applied Logic 10 (4):330-367.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  49.  3
    Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic.Rajeev Goré, Linda Postniece & Alwen Tiu - 2010 - In Lev Beklemishev, Valentin Goranko & Valentin Shehtman (eds.), Advances in Modal Logic, Volume 8. CSLI Publications. pp. 156-177.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  50.  24
    The Correspondence Between Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
1 — 50 / 1000