Proof analysis in modal logic (Q812101)

Labelled sequent calculi, which internalize Kripke semantics into inference systems, are introduced for many normal modal logics such as K, T, K4, KB, S4, TB, S5 and GL. The calculi are cut-free and contraction-free and the validity of structural properties, invertibility of rules, admissibility of substitution, contraction and cut are proved syntactically. The interesting case of Gödel-Löb logic GL solves a long-standing open problem in the author's opinion, though the results do not quite match that claim. Firstly, the main open problem has no mention of labelled sequent calculus; so this is a partial answer. Secondly, as the author notes in the beginning of Section 6, in general cut-elimination alone does not ensure terminating proof search in a given system. So, she introduces some explicit upper bounds for terminating proof search in different systems such as those for K, KB, TB, S4 and S5. But unfortunately, the case of GL has been neglected; if it is implicit, which is not clear from the text, a brief mentioning would have removed the doubt. If there is no such a bound for GL, then the passage ``decidability properties get established in the strong form of an effective bound on proof search'' in the introduction may mislead the reader when it is not said that this does not hold for GL. Apart from these doubts, the paper contains good and original results: after the introduction and the preliminaries in Sections~1 and 2, labelled sequent calculi are introduced in Section~3, and in Section~4 the admissibility of their structural rules are proved. Section~5 is devoted to GL, and in Section~6 decidability of some of the above systems is settled. Equality is included in the systems in Subsection~7.1, and finally the paper concludes with a very interesting result on undefinability of some Kripke frame properties, such as irreflexivity and intransitivity, by modal axioms/rules. In Corollary~7.5 the author gives marvellous syntactic proofs for these well-known phenomena.