A Modified Subformula Property for the Modal Logic S4.2
DOI:
https://doi.org/10.18778/0138-0680.48.1.02Keywords:
modal logic S4.2, sequent calculus, subformula propertyAbstract
The modal logic S4.2 is S4 with the additional axiom ◊□A ⊃ □◊A. In this article, the sequent calculus GS4.2 for this logic is presented, and by imposing an appropriate restriction on the application of the cut-rule, it is shown that, every GS4.2-provable sequent S has a GS4.2-proof such that every formula occurring in it is either a subformula of some formula in S, or the formula □¬□B or ¬□B, where □B occurs in the scope of some occurrence of □ in some formula of S. These are just the K5-subformulas of some formula in S which were introduced by us to show the modied subformula property for the modal logics K5 and K5D (Bull Sect Logic 30(2): 115–122, 2001). Some corollaries including the interpolation property for S4.2 follow from this. By slightly modifying the proof, the finite model property also follows.
References
M. Fitting, Subformula results in some propositional modal logics, Studia Logica 37 (1978), pp. 387–391.
Google Scholar
G. E. Hughes and M. J. Cresswell, A New Introduction to Modal Logic, Routledge, London and New York (1996).
Google Scholar
M. Takano, A modified subformula property for the modal logics K5 and K5D, Bulletin of the Section of Logic 30 (2001), pp. 115–122.
Google Scholar
M. Takano, A semantical analysis of cut-free calculi for modal logics, Reports on Mathematical Logic 53 (2018), pp. 43–65.
Google Scholar
G. Takeuti, Proof Theory, Second Edition (Studies in Logic and the Foundations of Mathematics 81), North-Holland, Amsterdam (1987).
Google Scholar
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2019 Bulletin of the Section of Logic
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
