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

1000+ found
Sort by:
  1. Wojciech Zielonka (2001). Cut-Rule Axiomatization of the Syntactic Calculus L. Journal of Logic, Language and Information 10 (2):339-352.score: 240.0
    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)  
     
    My bibliography  
     
    Export citation  
  2. Wojciech Zielonka (2000). Cut-Rule Axiomatization of the Syntactic Calculus NL. Journal of Logic, Language and Information 9 (3):339-352.score: 240.0
    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)  
     
    My bibliography  
     
    Export citation  
  3. Àngel J. Gil & Jordi Rebagliato (2000). Protoalgebraic Gentzen Systems and the Cut Rule. Studia Logica 65 (1):53-89.score: 180.0
    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)  
     
    My bibliography  
     
    Export citation  
  4. Wojciech Zielonka (1988). Cut‐Rule Axiomatization of Product‐Free Lambek Calculus With the Empty String. Mathematical Logic Quarterly 34 (2):135-142.score: 150.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Lev Gordeev (1987). On Cut Elimination in the Presence of Perice Rule. Archive for Mathematical Logic 26 (1):147-164.score: 120.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. 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.score: 120.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  7. Katalin Bimbó (2005). Admissibility of Cut in LC with Fixed Point Combinator. Studia Logica 81 (3):399 - 423.score: 102.0
    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 (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Peter Schroeder-Heister (2012). Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning. Topoi 31 (1):77-85.score: 90.0
    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)  
     
    My bibliography  
     
    Export citation  
  9. Katalin Bimbó (2007). LEt ® , LR °[^( ~ )], LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.score: 90.0
    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)  
     
    My bibliography  
     
    Export citation  
  10. Katalin Bimbó (2007). LEt ® LE^{T}{ \to } , LR °[^( ~ )]LR^{ \Circ }{{\Widehat{ \Sim }}}, LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.score: 90.0
    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)  
     
    My bibliography  
     
    Export citation  
  11. Wojciech Zielonka (2002). On Reduction Systems Equivalent to the Lambek Calculus with the Empty String. Studia Logica 71 (1):31-46.score: 90.0
    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)  
     
    My bibliography  
     
    Export citation  
  12. Susanne Bobzien (1999). Logic: The Stoics (Part Two). In Keimpe Algra, Jonathan Barnes & et al (eds.), The Cambridge History of Hellenistic Philosophy. CUP.score: 74.0
    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 to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  13. Susanne Bobzien (1996). Stoic Syllogistic. Oxford Studies in Ancient Philosophy 14:133-92.score: 72.0
    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 to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  14. Athanassios Tzouvaras (1996). Aspects of Analytic Deduction. Journal of Philosophical Logic 25 (6):581 - 596.score: 72.0
    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)  
     
    My bibliography  
     
    Export citation  
  15. Henry Africk (1992). Classical Logic, Intuitionistic Logic, and the Peirce Rule. Notre Dame Journal of Formal Logic 33 (2):229-235.score: 66.0
    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)  
     
    My bibliography  
     
    Export citation  
  16. Katalin Bimbó & J. Michael Dunn (2009). Symmetric Generalized Galois Logics. Logica Universalis 3 (1):125-152.score: 66.0
    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)  
     
    My bibliography  
     
    Export citation  
  17. Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1):47 - 72.score: 66.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  18. Gerhard Jäger & Thomas Studer (2011). A Buchholz Rule for Modal Fixed Point Logics. Logica Universalis 5 (1):1-19.score: 66.0
    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)  
     
    My bibliography  
     
    Export citation  
  19. Neil Tennant (2012). Cut for Core Logic. Review of Symbolic Logic 5 (3):450-479.score: 60.0
    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.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  20. Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the Igpl 8:733-750.score: 60.0
    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 <span class='Hi'>analytic</span> cut trees, a system from which cuts cannot be eliminated but satisfying the subformula property. Like tableaux <span class='Hi'>analytic</span> cut trees are a refutation system but unlike tableaux they have a single inference rule (a form (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  21. Norihiro Kamide (2002). Substructural Logics with Mingle. Journal of Logic, Language and Information 11 (2):227-249.score: 60.0
    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)  
     
    My bibliography  
     
    Export citation  
  22. Arnon Avron, A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.score: 60.0
    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.
     
    My bibliography  
     
    Export citation  
  23. Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.score: 60.0
    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)  
     
    My bibliography  
     
    Export citation  
  24. Birgit Elbl (2001). Cut Elimination for a Calculus with Context-Dependent Rules. Archive for Mathematical Logic 40 (3):167-188.score: 60.0
    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.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  25. Marcelo Finger & Dov Gabbay (2006). Cut and Pay. Journal of Logic, Language and Information 15 (3):195-218.score: 60.0
    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)  
     
    My bibliography  
     
    Export citation  
  26. J. Von Plato (2003). Translations From Natural Deduction to Sequent Calculus. Mathematical Logic Quarterly 49 (5):435.score: 60.0
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  27. Kazushige Terui (2007). Which Structural Rules Admit Cut Elimination? An Algebraic Criterion. Journal of Symbolic Logic 72 (3):738 - 754.score: 60.0
    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 (4 more)  
     
    My bibliography  
     
    Export citation  
  28. Chung-I. Lin (2012). Mohist Approach to the Rule-Following Problem. Comparative Philosophy 4 (1).score: 54.0
    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)  
     
    My bibliography  
     
    Export citation  
  29. 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.score: 54.0
    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)  
     
    My bibliography  
     
    Export citation  
  30. Rajeev Gore & Revantha Ramanayake (2012). Valentini's Cut-Elimination for Provability Logic Resolved. Review of Symbolic Logic 5 (2):212-238.score: 54.0
    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. (...)
    No categories
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  31. Rajeev Gore, Cut-Free Single-Pass Tableaux for the Logic of Common Knowledge.score: 54.0
    We present a cut-free tableau calculus with histories and variables for the EXPTIME-complete multi-modal logic of common knowledge (LCK). 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  
     
    My bibliography  
     
    Export citation  
  32. Norbert Gratzl (2010). A Sequent Calculus for a Negative Free Logic. Studia Logica 96 (3):331-348.score: 42.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  33. Neil Tennant (2003). Frege's Content-Principle and Relevant Deducibility. Journal of Philosophical Logic 32 (3):245-258.score: 42.0
    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 by (...)
    Direct download (10 more)  
     
    My bibliography  
     
    Export citation  
  34. Kentaro Kikuchi & Ryo Kashima (2001). Sequent Calculi for Visser's Propositional Logics. Notre Dame Journal of Formal Logic 42 (1):1-22.score: 42.0
    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)  
     
    My bibliography  
     
    Export citation  
  35. Kai Brünnler (2006). Locality for Classical Logic. Notre Dame Journal of Formal Logic 47 (4):557-580.score: 42.0
    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)  
     
    My bibliography  
     
    Export citation  
  36. Katalin Bimbó (2009). Dual Gaggle Semantics for Entailment. Notre Dame Journal of Formal Logic 50 (1):23-41.score: 42.0
    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)  
     
    My bibliography  
     
    Export citation  
  37. Gilles Dowek (2000). Axioms Vs. Rewrite Rules: From Completeness to Cut Elimination. In. In Dov M. Gabbay & Maarten de Rijke (eds.), Frontiers of Combining Systems. Research Studies Press. 62--72.score: 40.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  38. Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.score: 38.0
    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)  
     
    My bibliography  
     
    Export citation  
  39. M. Baaz & A. Leitsch (forthcoming). Cut-Elimination: Syntax and Semantics. Studia Logica:1-28.score: 38.0
    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 (cut-elimination by resolution) 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 (this (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  40. Yehuda Schwartz & George Tourlakis (forthcoming). On the Proof-Theory of a First-Order Extension of GL. Logic and Logical Philosophy.score: 36.0
    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)  
     
    My bibliography  
     
    Export citation  
  41. Norihiro Kamide & Heinrich Wansing (2010). Symmetric and Dual Paraconsistent Logics. Logic and Logical Philosophy 19 (1-2):7-30.score: 36.0
    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)  
     
    My bibliography  
     
    Export citation  
  42. Gillman Payette & Peter K. Schotch (forthcoming). Remarks on the Scott–Lindenbaum Theorem. Studia Logica:1-18.score: 34.0
    In the late 1960s and early 1970s, Dana Scott introduced a kind of generalization (or perhaps simplification would be a better description) of the notion of inference, familiar from Gentzen, in which one may consider multiple conclusions rather than single formulas. Scott used this idea to good effect in a number of projects including the axiomatization of many-valued logics (of various kinds) and a reconsideration of the motivation of C.I. Lewis. Since he left the subject it has been vigorously prosecuted (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  43. Katalin Bimbó, J. Michael Dunn & Roger D. Maddux (2009). Relevance Logics and Relation Algebras. Review of Symbolic Logic 2 (1):102-131.score: 30.0
    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)  
     
    My bibliography  
     
    Export citation  
  44. Francesca Poggiolesi (2009). A Purely Syntactic and Cut-Free Sequent Calculus for the Modal Logic of Provability. Review of Symbolic Logic 2 (4):593-611.score: 30.0
    In this paper we present a sequent calculus for the modal propositional logic GL (the logic of provability) obtained by means of the tree-hypersequent method, a method in which the metalinguistic strength of hypersequents is improved, so that we can simulate trees shapes. We prove that this sequent calculus is sound and complete with respect to the Hilbert-style system GL, that it is contraction free and cut free and that its logical and modal rules are invertible. No explicit semantic element (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  45. Mojtaba Aghaei & Mohammad Ardeshir (2001). Gentzen-Style Axiomatizations for Some Conservative Extensions of Basic Propositional Logic. Studia Logica 68 (2):263-285.score: 30.0
    We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  46. Grigori Mints (2006). Cut Elimination for S4c: A Case Study. Studia Logica 82 (1):121 - 132.score: 30.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  47. Melvin Fitting (1995). Tableaus for Many-Valued Modal Logic. Studia Logica 55 (1):63 - 87.score: 30.0
    We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  48. Sara Negri & Jan Von Plato (1998). Cut Elimination in the Presence of Axioms. Bulletin of Symbolic Logic 4 (4):418-435.score: 30.0
    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 (5 more)  
     
    My bibliography  
     
    Export citation  
  49. Linda Postniece, Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.score: 30.0
    Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  50. Katalin Bimbó (2007). $LE^{T}{Rightarrow}$ , $LR^{Circ}{Wedgesim}$ , LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557 - 570.score: 30.0
    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 (2 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000