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 the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity 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 Q¹S5 and its extension S5₀₋₂㵷 that combines S5 and the description logicALC with the universal role. We prove that interpolant and definition existence in Q¹S5 and S5₀₋₂㵷 is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment FO² of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment Q¹K of first-order modal logic K is non-elementary decidable, while uniform interpolant existence is again undecidable.
Kurucz et al. (Wed,) studied this question.