A Proof-Theoretic Study of Modal Logic

TL;DR

This paper develops a proof-theoretic hypersequent calculus framework for major modal logics like S5 and its variants, providing explanations and cut-elimination results for these systems.

Contribution

It introduces a unified hypersequent calculus framework for modal logics and proves cut-elimination for most of these systems, advancing proof theory in modal logic.

Findings

Proposes a hypersequent calculus framework for modal logics.

Establishes cut-elimination for K, T, D, S4, S5 systems.

Provides syntactic methods and discusses quantified versions.

Abstract

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.