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

TL;DR

The paper investigates non-uniform existence problems for Craig interpolants and explicit definitions in first-order modal logics that lack CIP/BDP, focusing on the one-variable fragments ${ m Q^1S5}$ and the modal description logic ${ m S5_{ALC^u}}$. It proves that interpolant and explicit-definition existence are decidable in ${ m coN2ExpTime}$ and 2ExpTime-hard, while uniform interpolant existence is undecidable, using a novel component-wise bisimulation framework and mosaic-type constructions to obtain exponential size bounds. It then extends these results to equality-free ${ m FO^2}$ (via ${ m Q^1S5}$) and to ${ m Q^1K}$, showing non-elementary upper bounds for IEP/EDEP and undecidability of UIEP/CEP in those logics. The findings illuminate the limits of reducing interpolation/definability to validity in logics between ${ m K}$ and ${ m S5}$, provide tight complexity separations, and offer a foundation for modular reasoning about ontologies and FO^2-like fragments in two-dimensional modal settings.

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.

Figures (4)

• Figure 1: Representing accepting computation-trees.
• Figure 2: Passing information from one configuration to the next.
• Figure 3: Enforcing $2^n$$\sigma$-bisimilar trees.
• Figure 4: The model $\mathfrak N$.

Theorems & Definitions (67)

• Example 1.1: based on DBLP:journals/jsyml/Fine79
• Theorem 1.2
• Theorem 1.3
• Theorem 1.4
• Theorem 1.5
• Lemma 2.1
• Theorem 3.1
• proof
• Example 3.2
• Theorem 3.3