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

The two-dimensional modal logic of Davies and Humberstone (1980) [3] is an important aid to our understanding the relationship between actuality, necessity and a priori knowability. I show how a cut-free hypersequent calculus for 2D modal logic not only captures the logic precisely, but may be used to address issues in the epistemology and metaphysics of our modal concepts. I will explain how the use of our concepts motivates the inference rules of the sequent calculus, and then show that the completeness of the calculus for Davies-Humberstone models explains why those concepts have the structure described by those models. The result is yet another application of the completeness theorem.