A Modified Subformula Property for the Modal Logic S4.2
Treść / Zawartość
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.
- M. Fitting, Subformula results in some propositional modal logics, Studia Logica 37 (1978), pp. 387–391.
- G. E. Hughes and M. J. Cresswell, A New Introduction to Modal Logic, Routledge, London and New York (1996).
- M. Takano, A modified subformula property for the modal logics K5 and K5D, Bulletin of the Section of Logic 30 (2001), pp. 115–122.
- M. Takano, A semantical analysis of cut-free calculi for modal logics, Reports on Mathematical Logic 53 (2018), pp. 43–65.
- G. Takeuti, Proof Theory, Second Edition (Studies in Logic and the Foundations of Mathematics 81), North-Holland, Amsterdam (1987).