Abstract

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the $\mathsf{K}$, $\mathsf{D}$, $\mathsf{T}$, $\mathsf{K4}$, $\mathsf{D4}$ and $\mathsf{S4}$ spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for $\Box$ and $\Diamond$. Starting points for this research are 2-sequents and indexed-based calculi (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration.