Deep sequent systems for modal logic (Q834716)

This is a very interesting paper presenting a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination of the axioms d, t, b, 4, 5. They are based on a form of deep inference where rules may not only be applied to the outermost connective but also deep inside formulas. The systems all enjoy the subformula property, all rules are invertible, and weakening, contraction and cut are admissible. This is achieved without reference to semantic notions like, for example, labels. The author establishes soundness, completeness and terminating proof search as well as a syntactic cut-elimination procedure. Also relations to other formalisms (a system by Kashima, the calculus of structures, labeled systems, hypersequents, and the display calculus) are studied in detail. The systems presented in this paper are not as modular as labeled systems. Brünnler and Strassburger overcome this shortcoming the sequel paper [\textit{K. Brünnler } and \textit{L. Strassburger}, Lect. Notes Comput. Sci. 5607, 152--166 (2009; Zbl 1180.03024)]. The deep inference approach to modal logic, as introduced in this paper, is essential for establishing syntactic cut-elimination for the logic of common knowledge. Such a cut-elimination procedure is presented in [\textit{K. Brünnler} and \textit{T. Studer}, Ann. Pure Appl. Logic 160, No.~1, 82--95 (2009; Zbl 1170.03007)].