Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic

TL;DR

This paper investigates the decidability and computational complexity of the existence of interpolants and definitions in various fragments of first-order modal logic, revealing decidability results and complexity bounds.

Contribution

It establishes the decidability and complexity of interpolant and definition existence in specific first-order modal logic fragments, including $ extsf{Q}^1 extsf{S5}$ and $ extsf{S5}_{ ext{ALC}^u}$, and extends results to classical first-order logic fragments.

Findings

Interpolant and definition existence in $ extsf{Q}^1 extsf{S5}$ and $ extsf{S5}_{ ext{ALC}^u}$ is decidable in coN2ExpTime.

Uniform interpolant existence in these fragments is undecidable.

Interpolant and definition existence in $ extsf{Q}^1 extsf{K}$ is non-elementary decidable.

Abstract

None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{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 $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable.