Decidable first-order modal logics with counting quantifiers

In this paper, we examine the computational complexity of various natural one-variable fragments of first-order modal logics with the addition of arbitrary counting quantifiers. The addition of counting quantifiers provides us a rich language with which to succinctly express statements about the quantity of objects satisfying a given property, using only a single variable. We provide optimal upper bounds on the complexity of the decision problem for several one-variable fragments, by establishing the finite model property. In particular, we show that the decision (validity) problem for the one-variable fragment of the minimal first-order modal logic QK with counting quantifiers is coNExpTime-complete. In the propositional setting, these results also provide optimal upper bounds for many two-dimensional modal logics in which one component is von Wright’s logic of ‘elsewhere’