This paper proposes a basic proof theoretic framework for major modal logics: {\sf S5} and some of its subsystems. The framework is based on a version of hypersequent calculus, and the basic modal systems we handle here are the system {\sf K} and its standard extensions with combinations of axioms: $T, D, 4, B, 5$. First we propose a reasonable explanation of how the standard sequent and hypersequent calculi for some of those modal logics such as {\sf K, T, D, S4, S5} emerge on the basis of the framework. Then, by a syntactic method, we prove the cut-elimination theorem for the modal logics except for the modal logics {\sf KB, KDB, KTB}. Quantified versions of the systems of the framework are also discussed.

翻译：本文为主要的模态逻辑系统——{\sf S5}及其部分子系统——提出了一个基本的证明论框架。该框架基于超序贯演算的一种变体，我们在此处理的基本模态系统是系统{\sf K}及其与公理组合$T, D, 4, B, 5$的标准扩张。首先，我们提出了一种合理的解释，说明其中一些模态逻辑（如{\sf K, T, D, S4, S5}）的标准序贯和超序贯演算如何基于该框架产生。然后，通过语法方法，我们证明了除模态逻辑{\sf KB, KDB, KTB}之外的模态逻辑的切割消去定理。文中还讨论了该框架系统的量化版本。