A Modified Subformula Property for the Modal Logic S4.2
Bulletin of the Section of Logic, Tome 48 (2019) no. 1
Voir la notice de l'article provenant de la source Library of Science
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.
Keywords:
modal logic S4.2, sequent calculus, subformula property
@article{BSL_2019_48_1_a0,
author = {Takano, Mitio},
title = {A {Modified} {Subformula} {Property} for the {Modal} {Logic} {S4.2}},
journal = {Bulletin of the Section of Logic},
publisher = {mathdoc},
volume = {48},
number = {1},
year = {2019},
language = {en},
url = {http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a0/}
}
Takano, Mitio. A Modified Subformula Property for the Modal Logic S4.2. Bulletin of the Section of Logic, Tome 48 (2019) no. 1. http://geodesic.mathdoc.fr/item/BSL_2019_48_1_a0/