The Method of Tree-Hypersequents for Modal Propositional Logic

  • Francesca PoggiolesiEmail author
Part of the Trends in Logic book series (TREN, volume 28)


In this paper we present a method, that we call the tree-hypersequent method, for generating contraction-free and cut-free sequent calculi for modal propositional logics. We show how this method works for the systems K, KD, K4 and KD4, by giving a sequent calculus for these systems which are normally presented in the Hilbert style, and by proving all the main results in a purely syntactical way.


contraction-free cut-free hypersequents modal logic sequent calculus tree-hypersequents 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Avron, A., ‘The method of hypersequents in the proof theory of propositional non-classical logic’, in Steinhorn, C., Strauss, J., Hodges, W., Hyland, M. (eds.), Logic: from Foundations to Applications, Oxford University Press, Oxford, 1996. Google Scholar
  2. [2]
    Brünnler, T., ‘Deep sequent systems for modal logic’, Advances in Modal Logic AiML, 6: 107–119, 2006. Google Scholar
  3. [3]
    Goble, L., ‘Gentzen systems for modal logic’, Notre Dame Journal of Formal Logic, 15: 455–461, 1974. zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    Indrzejczak, A., ‘Generalised sequent calculus for propositional modal logics’, Logica Trianguli, 1: 15–31, 1997. zbMATHMathSciNetGoogle Scholar
  5. [5]
    Kashima, R., ‘Cut-free sequent calculi for some tense logics’, Studia Logica, 53: 119–135, 1994. zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    Matsumoto, M., Ohnishi, K., ‘Gentzen method in modal calculi’, Osaka Mathematical Journal, 9 and 11: 115–120, 1959. MathSciNetGoogle Scholar
  7. [7]
    Mints, G., ‘Indexed systems of sequents and cut-elimination’, Journal of Philosophical Logic, 26: 671–696, 1997. zbMATHCrossRefMathSciNetGoogle Scholar
  8. [8]
    Negri, S., ‘Proof analysis in modal logic’, Journal of Philosophical Logic, 34, 2005. Google Scholar
  9. [9]
    Poggiolesi, F., ‘A cut-free simple sequent calculus for modal logic s5’, Submitted to the Review of Symbolic Logic, June 2007. Google Scholar
  10. [10]
    Poggiolesi, F., ‘Sequent calculus for modal logic’, Logic Colloquium, 2006. Google Scholar
  11. [11]
    Sambin, G., Valentini, S., ‘The modal logic of provability. The sequential approach’, Journal of Philosophical Logic, 11: 311–342, 1982. zbMATHCrossRefMathSciNetGoogle Scholar
  12. [12]
    Wansing, H., ‘Sequent calculi for normal modal propositional logics’, Journal of Logic and Computation, 4: 125–142, 1994. zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.Department of PhilosophyUniversity of Florence, IHPST, University of Paris 1FlorenceItaly

Personalised recommendations