A linear logic framework for multimodal logics

One of the most fundamental properties of a proof system is analyticity, expressing the fact that a proof of a given formula F only uses subformulas of F. In sequent calculus, this property is usually proved by showing that the cut rule is admissible, i.e., the introduction of the auxiliary lemma II in the reasoning "if H follows from G and F follows from H, then F follows from G" can be eliminated. The proof of cut admissibility is usually a tedious, error-prone process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures. In a previous work by Miller and Pimentel, linear logic (LL) was used as a logical framework for establishing sufficient conditions for cut admissibility of object logical systems (OL). The OL's inference rules are specified as an LL theory and an easy-to-verify criterion sufficed to establish the cut-admissibility theorem for the OL at hand. However, there are many logical systems that cannot be adequately encoded in LL, the most symptomatic cases being sequent systems for modal logics. In this paper, we use a linear-nested sequent (LNS) presentation of MMLL (a variant of LL with subexponentials), and show that it is possible to establish a cut-admissibility criterion for LNS systems for (classical or substructural) multimodal logics. We show that the same approach is suitable for handling the LNS system for intuitionistic logic.