A cut-free sequent system for two-dimensional modal logic, and why it matters (Q450956)

\textit{M. Davies} and \textit{L. Humberstone}'s two-dimensional modal logic [``Two notions of necessity'', Philos. Stud. 38, No. 1, 1--30 (1980; \url{doi:10.1007/BF00354523})] has become an important aid to our understanding of the relationship between actuality, necessity and a priori knowability. The author develops a hypersequent calculus for two-dimensional modal logic and proves the completeness of this calculus for Davies-Humberstone models, explaining why those concepts have the structure described by those models. The cut-elimination theorem for the introduced hypersequent calculus is obtained as a consequence of the completeness result.