Switch to: References

Add citations

You must login to add citations.
  1. Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
    A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.
    Direct download (4 more)  
    Export citation  
    Bookmark   63 citations  
  • On the Proof-Theory of Two Formalisations of Modal First-Order Logic.Yehuda Schwartz & George Tourlakis - 2010 - Studia Logica 96 (3):349-373.
    We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.
    Direct download (4 more)  
    Export citation  
    Bookmark   3 citations  
  • Modal Tableau Calculi and Interpolation.Wolfgang Rautenberg - 1983 - Journal of Philosophical Logic 12 (4):403 - 423.
  • The Modal Logic of Provability: Cut-Elimination. [REVIEW]Silvio Valentini - 1983 - Journal of Philosophical Logic 12 (4):471 - 476.
  • On Some Proof Theoretical Properties of the Modal Logic GL.Marco Borga - 1983 - Studia Logica 42 (4):453 - 459.
    This paper deals with the system of modal logicGL, in particular with a formulation of it in terms of sequents. We prove some proof theoretical properties ofGL that allow to get the cut-elimination theorem according to Gentzen's procedure, that is, by double induction on grade and rank.
    Direct download (4 more)  
    Export citation  
    Bookmark   10 citations  
  • The Modal Logic of Provability. The Sequential Approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
  • A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics.Feng Gao & George Tourlakis - 2015 - Bulletin of the Section of Logic 44 (3/4).
  • On the Proof-Theory of a First-Order Extension of GL.Yehuda Schwartz & George Tourlakis - 2014 - Logic and Logical Philosophy 23 (3).
    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 prove (...)
    Direct download (8 more)  
    Export citation  
    Bookmark   1 citation  
  • A Purely Syntactic and Cut-Free Sequent Calculus for the Modal Logic of Provability.Francesca Poggiolesi - 2009 - Review of Symbolic Logic 2 (4):593-611.
    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 (11 more)  
    Export citation  
    Bookmark   4 citations  
  • Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
    The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.
    Direct download (5 more)  
    Export citation  
    Bookmark   11 citations  
  • Valentini’s Cut-Elimination for Provability Logic Resolved.Rajeev Goré & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
    In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There is (...)
    Direct download (9 more)  
    Export citation  
    Bookmark   4 citations  
  • A System of Natural Deduction for GL.Gianluigi Bellin - 1985 - Theoria 51 (2):89-114.