Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-22T16:12:44.875Z Has data issue: false hasContentIssue false
  • English
  • Français

A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5

Published online by Cambridge University Press:  01 June 2008

FRANCESCA POGGIOLESI
FRANCESCA POGGIOLESI*
Affiliation:
University of Florence and University of Paris 1
*
*DEPARTMENT OF PHILOSOPHY, UNIVERSITY OF FLORENCE, 50139 FLORENCE, ITALY. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 1 , Issue 1 , June 2008 , pp. 3 - 15
Copyright
Copyright © Association for Symbolic Logic 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

BIBLIOGRAPHY

Avron, A. (1996). The method of hypersequents in the proof theory of propositional non-classical logic. In Hodges, W., Hyland, M., Steinhorn, C., & Truss, J., editors. Logic: From Foundations to Applications. Oxford University Press, pp. 1–32.Google Scholar
Blumey, S., & Humberstone, L. (1991). A perspective on modal sequent logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University, 27, 763–782.CrossRefGoogle Scholar
Braüner, T. (2000). A cut-free Gentzen formulation of the modal logic S5. Logic Journal of the IGPL, 8, 629–643.CrossRefGoogle Scholar
Brünnler, K. (2006). Deep sequent systems for modal logic. Advances in Modal Logic AiML, 6, 107–119.Google Scholar
Cerrato, C. (1993). Cut-free modal sequents for normal modal logics. Notre-Dame Journal of Formal Logic, 34, 564–582.CrossRefGoogle Scholar
Došen, K. (1985). Sequent systems for modal logic. Journal of Symbolic Logic, 50, 149–159.CrossRefGoogle Scholar
Indrezejczak, A. (1997). Generalised sequent calculus for propositional modal logics. Logica Trianguli, 1, 15–31.Google Scholar
Matsumoto, K., & Ohnishi, M. (1959). Gentzen method in modal calculi. Osaka Mathematical Journal, 11, 115–120.Google Scholar
Mints, G. (1997). Indexed systems of sequents and cut-elimination. Journal of Philosophical Logic, 26, 671–696.CrossRefGoogle Scholar
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34, 507–534.CrossRefGoogle Scholar
Poggiolesi, F. (2006). Sequent calculus for modal logic. Logic Colloquium.Google Scholar
Poggiolesi, F. (2007, submitted). Two cut-free sequent calculi for modal logic S5. Proceedings of SILFS Conference.Google Scholar
Poggiolesi, F. (2008). Sequent calculi for modal logic. Ph.D Thesis, p. 1–224, Florence.Google Scholar
Poggiolesi, F. (2008, to appear). The method of tree-hypersequent for modal propositional logic. Trends in Logic IV, Studia Logica Library.Google Scholar
Restall, G. (2006, to appear). Sequents and circuits for modal logic. Proceedings of Logic Colloquium.Google Scholar
Sato, M. (1980). A cut-free Gentzen-type system for the modal logic s5. Journal of Symbolic Logic, 45, 67–84.CrossRefGoogle Scholar
Wansing, H. (1994). Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, 4, 125–142.CrossRefGoogle Scholar