< Terug naar vorige pagina
Publicatie
A purely syntactic and cut-free sequent calculus for the modal logic of provability
Tijdschriftbijdrage - Tijdschriftartikel
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.
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.
Tijdschrift: Review of Symbolic Logic
ISSN: 1755-0203
Volume: 2
Pagina's: 593-611
Jaar van publicatie:2009
Trefwoorden:modal logic of provability, tree-hypersequent