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: 180.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: 180.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: 120.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. 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  
  5. Katalin Bimbó (2005). Admissibility of Cut in LC with Fixed Point Combinator. Studia Logica 81 (3):399 - 423.score: 90.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  
  6. 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  
  7. 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  
  8. Wojciech Zielonka (1988). Cut‐Rule Axiomatization of Product‐Free Lambek Calculus With the Empty String. Mathematical Logic Quarterly 34 (2):135-142.score: 90.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. 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  
  10. 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  
  11. 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  
  12. 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  
  13. Lev Gordeev (1987). On Cut Elimination in the Presence of Perice Rule. Archive for Mathematical Logic 26 (1):147-164.score: 72.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  14. 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: 72.0
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  15. 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  
  16. 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  
  17. 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  
  18. Henry Africk (1992). Classical Logic, Intuitionistic Logic, and the Peirce Rule. Notre Dame Journal of Formal Logic 33 (2):229-235.score: 54.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  
  19. Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1):47 - 72.score: 54.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  
  20. Gerhard Jäger & Thomas Studer (2011). A Buchholz Rule for Modal Fixed Point Logics. Logica Universalis 5 (1):1-19.score: 54.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  
  21. Neil Tennant (2012). Cut for Core Logic. Review of Symbolic Logic 5 (3):450-479.score: 48.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  
  22. Carlo Cellucci (2000). Analytic Cut Trees. Logic Journal of the IGPL 8:733-750.score: 48.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  
  23. Arnon Avron, A Simple Proof of Completeness and Cut-Elimination for Propositional G¨ Odel Logic.score: 48.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  
  24. Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.score: 48.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  
  25. Marcelo Finger & Dov Gabbay (2006). Cut and Pay. Journal of Logic, Language and Information 15 (3):195-218.score: 48.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. 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  
  27. Chung-I. Lin (2012). Mohist Approach to the Rule-Following Problem. Comparative Philosophy 4 (1).score: 42.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 (3 more)  
     
    My bibliography  
     
    Export citation  
  28. 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  
  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: 42.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: 42.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: 42.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. 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  
  33. 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  
  34. 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  
  35. Birgit Elbl (2001). Cut Elimination for a Calculus with Context-Dependent Rules. Archive for Mathematical Logic 40 (3):167-188.score: 40.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  
  36. Kazushige Terui (2007). Which Structural Rules Admit Cut Elimination? An Algebraic Criterion. Journal of Symbolic Logic 72 (3):738 - 754.score: 40.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  
  37. 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  
  38. 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  
  39. 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  
  40. 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  
  41. 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  
  42. Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.score: 30.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  
  43. 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  
  44. 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  
  45. Wojciech Zielonka (1989). A Simple and General Method of Solving the Finite Axiomatizability Problems for Lambek's Syntactic Calculi. Studia Logica 48 (1):35 - 39.score: 30.0
    In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  46. Athanassios Tzouvaras (2003). The Logic of Multisets Continued: The Case of Disjunction. Studia Logica 75 (3):287 - 304.score: 30.0
    We continue our work [5] on the logic of multisets (or on the multiset semantics of linear logic), by interpreting further the additive disjunction . To this purpose we employ a more general class of processes, called free, the axiomatization of which requires a new rule (not compatible with the full LL), the cancellation rule. Disjunctive multisets are modeled as finite sets of multisets. The -Horn fragment of linear logic, with the cut rule slightly restricted, is sound (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  47. M. Baaz & A. Leitsch (forthcoming). Cut-Elimination: Syntax and Semantics. Studia Logica:1-28.score: 30.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  
  48. Wojciech Zielonka (1990). Linear Axiomatics of Commutative Product-Free Lambek Calculus. Studia Logica 49 (4):515 - 522.score: 30.0
    Axiomatics which do not employ rules of inference other than the cut rule are given for commutative product-free Lambek calculus in two variants: with and without the empty string. Unlike the former variant, the latter one turns out not to be finitely axiomatizable in that way.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  49. Mojtaba Aghaei & Mohammad Ardeshir (2003). A Gentzen-Style Axiomatization for Basic Predicate Calculus. Archive for Mathematical Logic 42 (3):245-259.score: 30.0
    We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. Our new axiomatization is an improvement of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  50. Tor Sandqvist (2012). Acceptance, Inference, and the Multiple-Conclusion Sequent. Synthese 187 (3):913-924.score: 28.0
    This paper offers an interpretation of multiple-conclusion sequents as a kind of meta-inference rule: just as single-conclusion sequents represent inferences from sentences to sentences, so multiple-conclusion sequents represent a certain kind of inference from single-conclusion sequents to single-conclusion sequents. The semantics renders sound and complete the standard structural rules of reflexivity, monotonicity (or thinning), and transitivity (or cut). The paper is not the first one to attempt to account for multiple-conclusion sequents without invoking notions of truth or falsity—but unlike (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000