A semantical analysis of cut-free calculi for modal logics
Mitio Takano · Reports on Mathematical Logic · 2018
A b s t r a c t.We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics which 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 finite model property of the logics also follows.The purpose of this paper is to analyze semantically the logical inference rules in cut-free sequent calculi for modal logics, aiming at a cut-free or analytic version of Maehara [2], in which sequent calculi with cut are concerned with.This constitutes another proof of Kripke completeness as well as the cut-elimination property or the subformula property of the calculi.By modifying the arguments a bit, the finite model property also follows.