The Method of Tree-Hypersequents for Modal Propositional Logic
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.
Keywordscontraction-free cut-free hypersequents modal logic sequent calculus tree-hypersequents
Unable to display preview. Download preview PDF.
- 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
- Brünnler, T., ‘Deep sequent systems for modal logic’, Advances in Modal Logic AiML, 6: 107–119, 2006. Google Scholar
- Negri, S., ‘Proof analysis in modal logic’, Journal of Philosophical Logic, 34, 2005. Google Scholar
- Poggiolesi, F., ‘A cut-free simple sequent calculus for modal logic s5’, Submitted to the Review of Symbolic Logic, June 2007. Google Scholar
- Poggiolesi, F., ‘Sequent calculus for modal logic’, Logic Colloquium, 2006. Google Scholar