Labelled Sequents for Inquisitive First-Order Modal Logic

In recent work 5, an inquisitive first-order modal logic has been proposed to reason about relations of modal dependence, including the notion of global supervenience (functional dependence among the extensions of predicates relative to a space of possibilities).At present, no proof system exists for this logic.We provide a complete labelled sequent calculus, extending a calculus developed by Litak and Sano 22 for a weak version of inquisitive first-order logic.We prove strong completeness for the calculus and show that it enjoys desirable structural properties, including the invertibility of its rules and the admissibility of cut.