A semantical analysis of cut-free calculi for modal logics

Mitio Takano


We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics hich are obtained from the least normal logic K by adding axioms from T, 4, 5, D and B. This implies Kripke completeness, as well as the cutelimination property or the subformula property of the calculi. By slightly modifying the arguments, the nite model property of the logics also follows.

Received 9 June 2017

AMS subject classification: 03B45, 03F05

Słowa kluczowe: Sequent calculus, Kripke completeness, finite model property, cutelimination, subformula property

[1] R. Gor´e, Tableau methods for modal and temporal logics, In: Handbook of Tableau Methods (eds. M. D’Agostino, D.M. Gabbay, R. H¨ahnle and J. Posegga), Kluwer, Dordrecht, 1999, pp. 297–396.

[2] S. Maehara, A general theory of completeness proofs, Annals of the Japan Association for Philosophy of Science 3:5 (1970), 242–256.

[3] G.F. Shvarts, Gentzen style systems for K45 and K45D, In: Logic at Botik ’89 (eds. A.R. Meyer and M.A. Taitslin), Lecture Notes in Computer Science 363, Springer, Berlin, 1989, pp. 245–256.

[4] M. Takano, Subformula property as a substitute for cut-elimination in modal propositional logics, Mathematica Japonica 37 (1992), 1129–1145.

[5] M. Takano, A modified subformula property for the modal logics K5 and K5D, Bulletin of the Section of Logic 30 (2001), 115–122.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.