Deciding the existence of interpolants and definitions in First-Order Modal Logic

None of the first-order modal logics between K and S5 under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that deciding the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to deciding the validity of an implication, as in classical first- order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic S5: the one-variable fragment Q1S5 and its extension S5ALCu that combines S5 and the description logic ALC with the universal role. We prove that interpolant and definition existence in Q1S5 and S5ALCu is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment FO2 of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment Q1K of first-order modal logic K is non-elementary decidable, while uniform interpolant existence is again undecidable.