Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3

Daishi Yazaki

Bulletin of the Section of Logic (2019)

  • Volume: 48, Issue: 4
  • ISSN: 0138-0680

Abstract

top
The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has (cut) and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously.

How to cite

top

Daishi Yazaki. "Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3." Bulletin of the Section of Logic 48.4 (2019): null. <http://eudml.org/doc/295596>.

@article{DaishiYazaki2019,
abstract = {The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has (cut) and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously.},
author = {Daishi Yazaki},
journal = {Bulletin of the Section of Logic},
keywords = {modal logic; analytic cut; subformula property; finite model property},
language = {eng},
number = {4},
pages = {null},
title = {Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3},
url = {http://eudml.org/doc/295596},
volume = {48},
year = {2019},
}

TY - JOUR
AU - Daishi Yazaki
TI - Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3
JO - Bulletin of the Section of Logic
PY - 2019
VL - 48
IS - 4
SP - null
AB - The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has (cut) and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously.
LA - eng
KW - modal logic; analytic cut; subformula property; finite model property
UR - http://eudml.org/doc/295596
ER -

References

top
  1. [1] T. Shimura, Cut-free system for modal logic S4.3 and S4.3Grz, Reports on Mathematical Logic, Vol. 25 (1991), pp. 57–73. 
  2. [2] M. Takano, A modied subformula property for the modal logics K5 and K5D, Bulletin of the Section of Logic, Vol. 30 (2001), pp. 115–122. 
  3. [3] M. Takano, A semantical analysis of cut-free calculi for modal logics, Reports on Mathematical Logic, Vol. 53 (2018), pp. 43–65. http://dx.doi.org/10.4467/20842589RM.18.003.8836 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.