Search results for 'cut rule' (try it on Scholar)

1000+ found
Order:
  1.  12
    Wojciech Zielonka (2001). Cut-Rule Axiomatization of the Syntactic Calculus L. Journal of Logic, Language and Information 10 (2):339-352.
    In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L 0 of L. This modification, introduced in the early 1980s (see, (...)
    Direct download (10 more)  
     
    Export citation  
     
    My bibliography  
  2.  8
    Wojciech Zielonka (2000). Cut-Rule Axiomatization of the Syntactic Calculus NL. Journal of Logic, Language and Information 9 (3):339-352.
    An axiomatics of the product-free syntactic calculus L ofLambek has been presented whose only rule is the cut rule. It was alsoproved that there is no finite axiomatics of that kind. The proofs weresubsequently simplified. Analogous results for the nonassociativevariant NL of L were obtained by Kandulski. InLambek's original version of the calculus, sequent antecedents arerequired to be nonempty. By removing this restriction, we obtain theextensions L 0 and NL 0 ofL and NL, respectively. Later, the finiteaxiomatization problem (...)
    Direct download (10 more)  
     
    Export citation  
     
    My bibliography  
  3.  18
    Àngel J. Gil & Jordi Rebagliato (2000). Protoalgebraic Gentzen Systems and the Cut Rule. Studia Logica 65 (1):53-89.
    In this paper we show that, in Gentzen systems, there is a close relation between two of the main characters in algebraic logic and proof theory respectively: protoalgebraicity and the cut rule. We give certain conditions under which a Gentzen system is protoalgebraic if and only if it possesses the cut rule. To obtain this equivalence, we limit our discussion to what we call regular sequent calculi, which are those comprising some of the structural rules and some logical (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  4.  4
    Wojciech Zielonka (1988). Cut-Rule Axiomatization of Product-Free Lambek Calculus With the Empty String. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 34 (2):135-142.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  5.  1
    Wojciech Zielonka (1988). Cut‐Rule Axiomatization of Product‐Free Lambek Calculus With the Empty String. Mathematical Logic Quarterly 34 (2):135-142.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  6.  12
    Lev Gordeev (1987). On Cut Elimination in the Presence of Perice Rule. Archive for Mathematical Logic 26 (1):147-164.
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  7.  3
    Richard Zajac Sannerholm (2009). 5.'Cut-and-Paste'? Rule of Law Promotion and Legal Transplants in War to Peace Transitions. In Antonina Bakardjieva Engelbrekt (ed.), New Directions in Comparative Law. Edward Elgar
    Direct download  
     
    Export citation  
     
    My bibliography  
  8.  14
    Katalin Bimbó (2005). Admissibility of Cut in LC with Fixed Point Combinator. Studia Logica 81 (3):399 - 423.
    The fixed point combinator (Y) is an important non-proper combinator, which is defhable from a combinatorially complete base. This combinator guarantees that recursive equations have a solution. Structurally free logics (LC) turn combinators into formulas and replace structural rules by combinatory ones. This paper introduces the fixed point and the dual fixed point combinator into structurally free logics. The admissibility of (multiple) cut in the resulting calculus is not provable by a simple adaptation of the similar proof for LC with (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  9.  29
    Peter Schroeder-Heister (2012). Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning. Topoi 31 (1):77-85.
    From the point of view of proof-theoretic semantics, it is argued that the sequent calculus with introduction rules on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can cope with non-well-founded phenomena such as contradictory reasoning. The fact that, in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as a (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  10.  5
    Katalin Bimbó (2007). LEt ® , LR °[^( ~ )], LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.
    Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  11.  5
    Katalin Bimbó (2007). LEt ® LE^{T}{ \to } , LR °[^( ~ )]LR^{ \Circ }{{\Widehat{ \Sim }}}, LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.
    Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  12.  4
    Wojciech Zielonka (2002). On Reduction Systems Equivalent to the Lambek Calculus with the Empty String. Studia Logica 71 (1):31-46.
    The paper continues a series of results on cut-rule axiomatizability of the Lambek calculus. It provides a complete solution of a problem which was solved partially in one of the author''s earlier papers. It is proved that the product-free Lambek Calculus with the empty string (L 0) is not finitely axiomatizable if the only rule of inference admitted is Lambek''s cut rule. The proof makes use of the (infinitely) cut-rule axiomatized calculus C designed by the author (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  13.  15
    Athanassios Tzouvaras (1996). Aspects of Analytic Deduction. Journal of Philosophical Logic 25 (6):581 - 596.
    Let ⊢ be the ordinary deduction relation of classical first-order logic. We provide an "analytic" subrelation ⊢a of ⊢ which for propositional logic is defined by the usual "containment" criterion Γ ⊢a φ iff Γ⊢φ and Atom(φ) ⊆ Atom(Γ), whereas for predicate logic, ⊢a is defined by the extended criterion Γ⊢aφ iff Γ⊢aφ and Atom(φ) ⊆' Atom(Γ), where Atom(φ) ⊆' Atom(Γ) means that every atomic formula occurring in φ "essentially occurs" also in Γ. If Γ, φ are quantifier-free, then the (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  14.  8
    Jude Brighton (2016). Cut Elimination for GLS Using the Terminability of its Regress Process. 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  
     
    My bibliography  
  15.  4
    Arief Daynes (2006). A New Technique for Proving Realisability and Consistency Theorems Using Finite Paraconsistent Models of Cut‐Free Logic. Mathematical Logic Quarterly 52 (6):540-554.
    A new technique for proving realisability results is presented, and is illustrated in detail for the simple case of arithmetic minus induction. CL is a Gentzen formulation of classical logic. CPQ is CL minus the Cut Rule. The basic proof theory and model theory of CPQ and CL is developed. For the semantics presented CPQ is a paraconsistent logic, i.e. there are non-trivial CPQ models in which some sentences are both true and false. Two systems of arithmetic minus induction (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  16. Susanne Bobzien (1996). Stoic Syllogistic. Oxford Studies in Ancient Philosophy 14:133-92.
    ABSTRACT: For the Stoics, a syllogism is a formally valid argument; the primary function of their syllogistic is to establish such formal validity. Stoic syllogistic is a system of formal logic that relies on two types of argumental rules: (i) 5 rules (the accounts of the indemonstrables) which determine whether any given argument is an indemonstrable argument, i.e. an elementary syllogism the validity of which is not in need of further demonstration; (ii) one unary and three binary argumental rules which (...)
    Translate
      Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  17. Susanne Bobzien (1999). Logic: The Stoics (Part Two). In Keimpe Algra, Jonathan Barnes & et al (eds.), The Cambridge History of Hellenistic Philosophy. CUP
    ABSTRACT: A detailed presentation of Stoic theory of arguments, including truth-value changes of arguments, Stoic syllogistic, Stoic indemonstrable arguments, Stoic inference rules (themata), including cut rules and antilogism, argumental deduction, elements of relevance logic in Stoic syllogistic, the question of completeness of Stoic logic, Stoic arguments valid in the specific sense, e.g. "Dio says it is day. But Dio speaks truly. Therefore it is day." A more formal and more detailed account of the Stoic theory of deduction can be found (...)
    Translate
      Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  18.  13
    Neil Tennant (2016). Rule-Irredundancy and the Sequent Calculus for Core Logic. Notre Dame Journal of Formal Logic 57 (1):105-125.
    We explore the consequences, for logical system-building, of taking seriously the aim of having irredundant rules of inference, and a preference for proofs of stronger results over proofs of weaker ones. This leads one to reconsider the structural rules of REFLEXIVITY, THINNING, and CUT. REFLEXIVITY survives in the minimally necessary form $\varphi:\varphi$. Proofs have to get started. CUT is subject to a CUT-elimination theorem, to the effect that one can always make do without applications of CUT. So CUT is redundant, (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  19.  23
    Katalin Bimbó & J. Michael Dunn (2009). Symmetric Generalized Galois Logics. Logica Universalis 3 (1):125-152.
    Symmetric generalized Galois logics (i.e., symmetric gGl s) are distributive gGl s that include weak distributivity laws between some operations such as fusion and fission. Motivations for considering distribution between such operations include the provability of cut for binary consequence relations, abstract algebraic considerations and modeling linguistic phenomena in categorial grammars. We represent symmetric gGl s by models on topological relational structures. On the other hand, topological relational structures are realized by structures of symmetric gGl s. We generalize the weak (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  20.  7
    J. Von Plato (2003). Translations From Natural Deduction to Sequent Calculus. Mathematical Logic Quarterly 49 (5):435.
    Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut-free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut-free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  21.  7
    Gerhard Jäger & Thomas Studer (2011). A Buchholz Rule for Modal Fixed Point Logics. Logica Universalis 5 (1):1-19.
    Buchholz’s Ω μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result similar to that of Buchholz (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  22.  25
    Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1):47 - 72.
    In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  23.  65
    Henry Africk (1992). Classical Logic, Intuitionistic Logic, and the Peirce Rule. Notre Dame Journal of Formal Logic 33 (2):229-235.
    A simple method is provided for translating proofs in Grentzen's LK into proofs in Gentzen's LJ with the Peirce rule adjoined. A consequence is a simpler cut elimination operator for LJ + Peirce that is primitive recursive.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  24.  45
    Neil Tennant (2012). Cut for Core Logic. Review of Symbolic Logic 5 (3):450-479.
    The motivation for Core Logic is explained. Its system of proof is set out. It is then shown that, although the system has no Cut rule, its relation of deducibility obeys Cut with epistemic gain.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  25.  11
    Marcelo Finger & Dov Gabbay (2006). Cut and Pay. Journal of Logic, Language and Information 15 (3):195-218.
    In this paper we study families of resource aware logics that explore resource restriction on rules; in particular, we study the use of controlled cut-rule and introduce three families of parameterised logics that arise from different ways of controlling the use of cut. We start with a formulation of classical logic in which cut is non-eliminable and then impose restrictions on the use of cut. Three Cut-and-Pay families of logics are presented, and it is shown that each family provides (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  26.  31
    Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.
    We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G 0(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G 0are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  27.  7
    Mirjana Borisavljević (1999). A Cut-Elimination Proof in Intuitionistic Predicate Logic. 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 (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  28. Arnon Avron, A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.
    We provide a constructive, direct, and simple proof of the completeness of the cut-free part of the hypersequential calculus for G¨odel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions.
     
    Export citation  
     
    My bibliography  
  29. Marcelo Finger & Dov Gabbay (2007). Equal Rights for the Cut: Computable Non-Analytic Cuts in Cut-Based Proofs. Logic Journal of the IGPL 15 (5-6):553-575.
    This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof. We then concentrate on the problem of efficiently computing non-analytic cuts. (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  30.  25
    Rajeev Gore & Revantha Ramanayake (2012). Valentini's Cut-Elimination for Provability Logic Resolved. 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 (8 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  31. Rajeev Gore, Cut-Free Single-Pass Tableaux for the Logic of Common Knowledge.
    We present a cut-free tableau calculus with histories and variables for the EXPTIME-complete multi-modal logic of common knowledge. Our calculus constructs the tableau using only one pass, so proof-search for testing theoremhood of ϕ does not exhibit the worst-case EXPTIME-behaviour for all ϕ as in two-pass methods. Our calculus also does not contain a “finitized ω-rule” so that it detects cyclic branches as soon as they arise rather than by worst-case exponential branching with respect to the size of ϕ. (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  32. Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8 (6):733-750.
    It has been maintained by Smullyan that the importance of cut-free proofs does not stem from cut elimination per se but rather from the fact that they satisfy the subformula property. In accordance with such a viewpoint in this paper we introduce analytic cut trees, a system from which cuts cannot be eliminated but satisfying the subformula property. Like tableaux analytic cut trees are a refutation system but unlike tableaux they have a single inference rule and several branch closure (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  33.  32
    Chung-I. Lin (2012). Mohist Approach to the Rule-Following Problem. Comparative Philosophy 4 (1):41-66.
    Normal 0 false false false EN-US ZH-TW X-NONE /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-priority:99; mso-style-parent:""; mso-padding-alt:0in 5.4pt 0in 5.4pt; mso-para-margin:0in; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman";} The Mohist conceives the dao -following issue as “ how we can put dao in words and speeches into practice.” The dao -following issue is the Mohist counterpart of Wittgenstein’s rule-following problem. This paper aims to shed light on the rule-following issue in terms of the Mohist answer (...)
    No categories
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  34.  38
    Tyler Cowen (2011). Rule Consequentialism Makes Sense After All. Social Philosophy and Policy 28 (2):212-231.
    It is commonly claimed that rule consequentialism collapses into act consequentialism, because sometimes there are benefits from breaking the rules. I suggest this argument is less powerful than has been believed. The argument requires a commitment to a very particular account of feasibility and constraints. It requires the presupposition that thinking of rules as the relevant constraint is incorrect. Supposedly we should look at a smaller unit of choice—the single act—as the relevant choice variable. But once we see feasibility (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  35.  16
    Dov M. Gabbay & Nicola Olivetti (1998). Algorithmic Proof Methods and Cut Elimination for Implicational Logics Part I: Modal Implication. Studia Logica 61 (2):237-280.
    In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. We (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  36.  4
    Toshiyasu Arai (1998). Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection. 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 (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  37.  18
    Norihiro Kamide (2002). Substructural Logics with Mingle. Journal of Logic, Language and Information 11 (2):227-249.
    We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FLm (full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm (Lambek calculuswith restricted mingle).
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  38. Bayu Surarso & Hiroakira Ono (1996). Cut Elimination In Noncommutative Substructural Logics. Reports on Mathematical Logic:13-29.
    The present paper is concerned with the cut eliminability for some sequent systems of noncommutative substructural logics, i.e. substructural logics without exchange rule. Sequent systems of several extensions of noncommutative logics FL and LBB'I, which is sometimes called $\tw$, will be introduced. Then, the cut elimination theorem and the decision problem for them will be discussed in comparison with their commutative extensions.
     
    Export citation  
     
    My bibliography   1 citation  
  39.  21
    Greg Restall (2014). Normal Proofs, Cut Free Derivations and Structural Rules. Studia Logica 102 (6):1143-1166.
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  40.  24
    Jack Woods (forthcoming). Assertion, Denial, Content, and Form. Synthese:1-14.
    I discuss Greg Restall’s attempt to generate an account of logical consequence from the incoherence of certain packages of assertions and denials. I take up his justification of the cut rule and argue that, in order to avoid counterexamples to cut, he needs, at least, to introduce a notion of logical form. I then suggest a few problems that will arise for his account if a notion of logical form is assumed. I close by sketching what I take to (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  41. Katalin Bimbó (2009). Dual Gaggle Semantics for Entailment. Notre Dame Journal of Formal Logic 50 (1):23-41.
    A sequent calculus for the positive fragment of entailment together with the Church constants is introduced here. The single cut rule is admissible in this consecution calculus. A topological dual gaggle semantics is developed for the logic. The category of the topological structures for the logic with frame morphisms is proven to be the dual category of the variety, that is defined by the equations of the algebra of the logic, with homomorphisms. The duality results are extended to the (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  42.  1
    Kai Brünnler (2006). Locality for Classical Logic. Notre Dame Journal of Formal Logic 47 (4):557-580.
    In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they drop the restriction that rules only apply to the main connective of a formula: their rules apply anywhere deeply inside a formula. This allows to observe very clearly the symmetry between identity axiom and the cut rule. This symmetry allows to reduce the cut (...) to atomic form in a way which is dual to reducing the identity axiom to atomic form. We also reduce weakening and even contraction to atomic form. This leads to inference rules that are local: they do not require the inspection of expressions of arbitrary size. (shrink)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  43.  1
    Jack Woods (2016). Assertion, Denial, Content, and Form. Synthese 193 (6):1667-1680.
    I discuss Greg Restall’s attempt to generate an account of logical consequence from the incoherence of certain packages of assertions and denials. I take up his justification of the cut rule and argue that, in order to avoid counterexamples to cut, he needs, at least, to introduce a notion of logical form. I then suggest a few problems that will arise for his account if a notion of logical form is assumed. I close by sketching what (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  44.  39
    Norbert Gratzl (2010). A Sequent Calculus for a Negative Free Logic. Studia Logica 96 (3):331-348.
    This article presents a sequent calculus for a negative free logic with identity, called N . The main theorem (in part 1) is the admissibility of the Cut-rule. The second part of this essay is devoted to proofs of soundness, compactness and completeness of N relative to a standard semantics for negative free logic.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  45.  32
    Neil Tennant (2003). Frege's Content-Principle and Relevant Deducibility. Journal of Philosophical Logic 32 (3):245-258.
    Given the harmony principle for logical operators, compositionality ought to ensure that harmony should obtain at the level of whole contents. That is, the role of a content qua premise ought to be balanced exactly by its role as a conclusion. Frege's contextual definition of propositional content happens to exploit this balance, and one appeals to the Cut rule to show that the definition is adequate. We show here that Frege's definition remains adequate even when one relevantizes logic (...)
    Direct download (9 more)  
     
    Export citation  
     
    My bibliography  
  46.  6
    Kentaro Kikuchi & Ryo Kashima (2001). Sequent Calculi for Visser's Propositional Logics. Notre Dame Journal of Formal Logic 42 (1):1-22.
    This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  47.  4
    Norihiro Kamide & Heinrich Wansing (2010). Symmetric and Dual Paraconsistent Logics. Logic and Logical Philosophy 19 (1-2):7-30.
    Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL are introduced, and (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  48.  3
    Yehuda Schwartz & George Tourlakis (2013). On the Proof-Theory of a First-Order Extension of GL. Logic and Logical Philosophy.
    We introduce a first order extension of GL, called ML 3 , and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML 3 , as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  49.  37
    Katalin Bimbó, J. Michael Dunn & Roger D. Maddux (2009). Relevance Logics and Relation Algebras. Review of Symbolic Logic 2 (1):102-131.
    Relevance logics are known to be sound and complete for relational semantics with a ternary accessibility relation. This paper investigates the problem of adequacy with respect to special kinds of dynamic semantics (i.e., proper relation algebras and relevant families of relations). We prove several soundness results here. We also prove the completeness of a certain positive fragment of R as well as of the first-degree fragment of relevance logics. These results show that some core ideas are shared between relevance logics (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  50.  4
    Francesca Poggiolesi (forthcoming). Natural Deduction Calculi and Sequent Calculi for Counterfactual Logics. Studia Logica:1-34.
    In this paper we present labelled sequent calculi and labelled natural deduction calculi for the counterfactual logics CK + {ID, MP}. As for the sequent calculi we prove, in a semantic manner, that the cut-rule is admissible. As for the natural deduction calculi we prove, in a purely syntactic way, the normalization theorem. Finally, we demonstrate that both calculi are sound and complete with respect to Nute semantics [12] and that the natural deduction calculi can be effectively transformed into (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
1 — 50 / 1000