Abstract
We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.
Chapter PDF
Similar content being viewed by others
References
Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 292–307. Springer, Heidelberg (2001)
Bierman, G.M., de Paiva, V.: On an intuitionistic modal logic. Studia Logica 65(3), 383–416 (2000)
Brünnler, K.: Deep sequent systems for modal logic. Archive for Mathematical Logic 48(6), 551–577 (2009)
Brünnler, K., Straßburger, L.: Modular Sequent Systems for Modal Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 152–166. Springer, Heidelberg (2009)
Chaudhuri, K., Guenot, N., Straßburger, L.: The focused calculus of structures. In: Bezem, M. (ed.) CSL 2011. LIPIcs, vol. 12, pp. 159–173. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik (2011)
Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log. 57(3), 795–807 (1992)
Ewald, W.B.: Intuitionistic tense and modal logic. J. Symb. Log. 51 (1986)
Fitch, F.B.: Intuitionistic modal logic with quantifiers. Portugaliae Mathematica 7(2), 113–118 (1948)
Fitting, M.: Nested sequents for intuitionistic logic (2011) (preprint)
Fitting, M.: Prefixed tableaus and nested sequents. Annals of Pure and Applied Logic 163, 291–313 (2012)
Galmiche, D., Salhi, Y.: Label-free natural deduction systems for intuitionistic and classical modal logics. Journal of Applied Non-Classical Logics 20(4), 373–421 (2010)
Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Stanford University (2008)
Goré, R., Postniece, L., Tiu, A.: Cut-elimination and proof search for bi-intuitionistic tense logic. In: Shehtman, V., Beklemishev, L., Goranko, V. (eds.) Advances in Modal Logic, pp. 156–177. College Publications (2010)
Kashima, R.: Cut-free sequent calculi for some tense logics. Studia Logica 53(1), 119–136 (1994)
Lamarche, F.: On the algebra of structural contexts. Accepted at Mathematical Structures in Computer Science (2001)
Liang, C., Miller, D.: Focusing and Polarization in Intuitionistic Logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 451–465. Springer, Heidelberg (2007)
McLaughlin, S., Pfenning, F.: The focused constraint inverse method for intuitionistic modal logics. Draft manuscript (2010)
Mendler, M., Scheele, S.: Cut-free gentzen calculus for multimodal ck. Inf. Comput. 209(12), 1465–1490 (2011)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3) (2008)
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4), 511–540 (2001)
Plotkin, G.D., Stirling, C.P.: A framework for intuitionistic modal logic. In: Halpern, J.Y. (ed.) Theoretical Aspects of Reasoning About Knowledge (1986)
Poggiolesi, F.: The method of tree-hypersequents for modal propositional logic. In: Makinson, D., Malinowski, J., Wansing, H. (eds.) Towards Mathematical Philosophy. Trends in Logic, vol. 28, pp. 31–51. Springer (2009)
Prawitz, D.: Natural Deduction, A Proof-Theoretical. Almquist and Wiksell (1965)
Fischer Servi, G.: Axiomatizations for some intuitionistic modal logics. Rend. Sem. Mat. Univers. Politecn. Torino 42(3), 179–194 (1984)
Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Straßburger, L. (2013). Cut Elimination in Nested Sequents for Intuitionistic Modal Logics. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)