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.
Ciardelli et al. (Sun,) studied this question.