Labelled Sequent Calculi for Inquisitive Modal Logics

We present cut-free labelled sequent calculi for various systems of inquisitive modal logic, including inquisitive epistemic logic and inquisitive doxastic logic. Inquisitive modal logic extends the framework of standard modal logic with a question-forming operator and an inquisitive modal operator. Under an epistemic interpretation, this modal operator may be used to express not only the information available to an agent, but also the issues entertained by the agent. Each of our proof systems is shown to satisfy cut-admissibility, height-preserving admissibility of weakening and contraction, and height-preserving invertibility of all rules. The completeness of our calculi is established proof-theoretically.