Review of Symbolic Logic 2 (4):593-611 (2009)
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 is used in the sequent calculus and all the results are proved in a purely syntactic way.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
The Modal Logic of Provability: Cut-Elimination. [REVIEW]Silvio Valentini - 1983 - Journal of Philosophical Logic 12 (4):471 - 476.
On the Proof Theory of the Modal Logic for Arithmetic Provability.Daniel Leivant - 1981 - Journal of Symbolic Logic 46 (3):531-538.
Citations of this work BETA
Valentini's Cut-Elimination for Provability Logic Resolved.Rajeev Gore & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
Similar books and articles
Proof-Theoretic Modal PA-Completeness II: The Syntactic Countermodel.Paolo Gentilini - 1999 - Studia Logica 63 (2):245-268.
Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.Linda Postniece - unknown
Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
A Cut-Free Simple Sequent Calculus for Modal Logic S5.Francesca Poggiolesi - 2008 - Review of Symbolic Logic 1 (1):3-15.
Added to index2009-12-31
Total downloads30 ( #167,472 of 2,153,830 )
Recent downloads (6 months)1 ( #398,274 of 2,153,830 )
How can I increase my downloads?