Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations

TL;DR

The paper addresses whether the interpolant existence problem (IEP) is decidable in fragments of first-order logic lacking Craig interpolation property, challenging the prevailing intuition that IEP mirrors entailment decidability. Using a reduction from the infinite Post Correspondence Problem, it shows that the IEP is undecidable for the two-variable fragment with two equivalence relations ($FO^2 2E$) and, via guarded-embedding techniques, for the two-variable guarded fragment with constants and two equivalence relations ($GF^2 2E_c$); it also establishes undecidability of the corresponding explicit definition existence problem (EDEP). These results extend to description logics such as $ALC^{\cap,\neg,\text{id}}2E$, indicating undecidability of interpolant and explicit-definition questions in expressive DLs with Boolean role operators and the identity role. The findings disprove the conjecture that IEP should be decidable whenever entailment is decidable and open new questions about the boundaries of undecidability in interpolation-related problems for DLs and FO fragments.

Abstract

The interpolant existence problem (IEP) for a logic L is to decide, given formulas P and Q, whether there exists a formula I, built from the shared symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the Craig interpolation property (CIP), then the IEP reduces to validity in L. Recently, the IEP has been studied for logics without the CIP. The results obtained so far indicate that even though the IEP can be computationally harder than validity, it is decidable when L is decidable. Here, we give the first examples of decidable fragments of first-order logic for which the IEP is undecidable. Namely, we show that the IEP is undecidable for the two-variable fragment with two equivalence relations and for the two-variable guarded fragment with individual constants and two equivalence relations. We also determine the corresponding decidable Boolean description logics for which the IEP is undecidable.

Figures (1)

• Figure 1: Intended models $\mathfrak{A}\xspace,a_0$ and $\mathfrak{B}\xspace,b_0$ with $\mathfrak{A}\xspace\models \varphi(a_0)$, $\mathfrak{B}\xspace \models \neg \psi(b_0)$, and $\mathfrak{A}\xspace,a_0 \sim_{L,\varrho} \mathfrak{B}\xspace,b_0$, where $\varrho$-bisimilar points in the disjoint union of $\mathfrak{A}\xspace$ and $\mathfrak{B}\xspace$ are connected by dotted lines and $E_i$-equivalence classes in $\mathfrak{B}\xspace$, $i=1,2$, are encircled by dashed lines. Model $\mathfrak{A}\xspace$ contains two disjoint copies of a 3-point $R$-cycle followed by an infinite $S$-chain. Model $\mathfrak{B}\xspace$ has an infinite $R$-chain of points $b_i$, for $i \in \mathbb Z$; each $b_{6i}$ starts an infinite $S$-chain for the word $v_{i_1}v_{i_2}\dots$, and each $b_{6i+3}$ starts an infinite $S$-chain for the word $w_{i_1}w_{i_2}\dots$. These $\omega$-words coincide with the $\omega$-word written on the $S$-chains in $\mathfrak{A}\xspace$.

Theorems & Definitions (12)

• Definition 1
• Definition 2
• Definition 3
• Lemma 1
• Lemma 2
• Definition 4
• Lemma 3
• Theorem 4
• proof
• Theorem 5