=Paper=
{{Paper
|id=Vol-3739/paper-11
|storemode=property
|title=Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
|pdfUrl=https://ceur-ws.org/Vol-3739/paper-11.pdf
|volume=Vol-3739
|authors=Frank Wolter,Michael Zakharyaschev
|dblpUrl=https://dblp.org/rec/conf/dlog/WolterZ24
}}
==Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations==
https://ceur-ws.org/Vol-3739/paper-11.pdf
Interpolant Existence is Undecidable for Two-Variable
First-Order Logic with Two Equivalence Relations
Frank Wolter1 , Michael Zakharyaschev2
1
University of Liverpool, Ashton Street, Liverpool L69 3BX, UK
3
Birkbeck, University of London, Malet Street, London WC1E 7HX, UK
Abstract
The interpolant existence problem (IEP) for a logic πΏ is to decide, given formulas π and π, whether there exists a
formula π, built from the shared symbols of π and π, such that π entails π and π entails π in πΏ. If πΏ enjoys the Craig
interpolation property (CIP), then the IEP reduces to validity in πΏ. 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 πΏ 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.
Keywords
Craig interpolant, interpolant existence problem, two-variable fragment of first-order logic.
1. Introduction
A first-order (FO) formula π is called a Craig interpolant for FO-formulas π and π if π |= π |= π and π
is built from the shared non-logical symbols of π and π. Interpolants have been applied in many areas
ranging from formal verification [1] and software specification [2] to theory combinations [3, 4, 5] and
query reformulation and rewriting in databases [6, 7].
For many fragments πΏ of FO, including many description logics (DLs), the existence of a Craig inter-
polant for π and π is guaranteed if π entails π. This phenomenon is known as the Craig interpolation
property (CIP) of πΏ. The CIP holds, for instance, for the DLs πβπ, πβπβ, and πβππ¬β [8], and also for
the guarded negation fragment of FO [9]. In this case, the problem to decide whether an interpolant for
π and π exists reduces to showing that π entails π in πΏ, and so is not harder than entailment. Moreover,
interpolants can often be extracted from a proof of the entailment.
An important consequence of the CIP of a logic πΏ is the projective Beth definability property (BDP)
of πΏ: if a relation is implicitly definable over a signature π in πΏ, then it is explicitly definable over
π in πΏ. The BDP is used in ontology engineering for extracting explicit definitions of concepts or
nominals from ontologies [10, 8, 11], developing and maintaining ontology alignments [12], and for
robust modularisations and decompositions of ontologies [13, 14]. Explicit definitions are used in
ontology-based data management to equivalently rewrite ontology-mediated queries [15, 16, 17, 18, 19].
Unfortunately, there are many prominent fragments of FO that do not enjoy the CIP and BDP: for
example, DLs with nominals such as πβππͺ and/or role inclusions such as πβπβ [8], the guarded
and the two-variable fragment of FO [20, 21, 22]. To extend interpolation-based techniques to such
formalisms, it has recently been suggested to investigate the interpolant existence problem (IEP) for
logics πΏ without the CIP: given formulas π and π as an input, decide whether they have a Craig
interpolant in πΏ. It has been shown that the IEP is decidable for many DLs with nominals and role
inclusions [23], Horn-DLs [24], the two-variable and guarded fragments of FO [25], and some decidable
DL 2024: 37th International Workshop on Description Logics, June 18β21, 2024, Bergen, Norway
$ wolter@liverpool.ac.uk (F. Wolter); m.zakharyaschev@bbk.ac.uk (M. Zakharyaschev)
0000-0002-4470-606X (F. Wolter); 0000-0002-2210-5183 (M. Zakharyaschev)
Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
fragments of first-order modal logics [26]. These positive results naturally lead to a conjecture that the
IEP for πΏ is decidable whenever the entailment in πΏ is decidable.
In this paper, we disprove this conjecture by showing that the IEP is undecidable for the two-variable
FO with two equivalence relations and also for the two-variable guarded fragment of FO with constants
and two equivalence relations. In the realm of Description Logic, the former result means that interpolant
existence is undecidable for concept inclusions in πβπ enriched with Boolean operators on roles and
the identity role. As a consequence, we also obtain the undecidability of the explicit definition existence
problem (EDEP) for each of these logics πΏ, which is the problem of deciding, given formulas π, π and a
signature π, whether there exists an explicit π-definition of π modulo π in πΏ. (It is known [26] that the
IEP and EDEP are polynomially reducible to each other.)
The paper is structured as follows. Section 2 introduces the fragments of FO we are interested in and
summarises the necessary technical tools and results. Section 3 proves the undecidability of the IEP for
the two-variable FO with two equivalence relations by reduction of the infinite Post Correspondence
Problem. Section 4 shows how this result can be adapted to the two-variable guarded fragment with
constants and two equivalence relations and to suitable description logics. Finally, Section 5 discusses a
few challenging open problems.
2. Preliminaries
Let π be a signature of individual constants and unary and binary predicate symbols, including two
distinguished binary equivalence predicates πΈ1 , πΈ2 . Let var be a set comprising two individual variables.
We consider the following fragments of first-order logic FO(π) over π:
FO2 2E(π) is the set of constant-free FO-formulas constructed in the usual way from atoms π₯ = π¦ with
π₯, π¦ β var and π
(π₯), for any π-ary predicate symbol π
β π and π-tuple π₯ of variables from var ;
GF2 2Ec (π) admits variables in var and individual constants in atoms but restricts quantification to the
patterns (οΈ )οΈ (οΈ )οΈ
βπ¦ πΌ(π₯, π¦) β π(π₯, π¦) , βπ¦ πΌ(π₯, π¦) β§ π(π₯, π¦) ,
where π(π₯, π¦) is a GF2 2Ec -formula and πΌ(π₯, π¦) is an atom with occurrences of π₯, π¦.
The signature sig(π) of a formula π in any of these logics is the (οΈset of predicate and constant )οΈsymbols
occurring in π. Formulas are interpreted in π-structures A = dom(A), (π
A )π
βπ , (πA )πβπ ) with a
domain dom(A) ΜΈ= β
, relations π
A on dom(A) of the same arity as predicates π
β π, and πA β dom(A).
It is always assumed that πΈ1A and πΈ2A are equivalence relations on dom(A). A pointed structure is a pair
A, π with a tuple π = (π1 , . . . , ππ ), π β€ 2, of elements from dom(A).
The decision problems for FO2 2E and GF2 2Ec are known to be co2NExpTime- and 2ExpTime-
complete, respectively; see [27, 28] and references therein.
Definition 1. Let πΏ β {FO2 2E, GF2 2Ec }, let π(π₯) and π(π₯) be πΏ(π)-formulas with the same free
variables π₯, and let π = sig(π) β© sig(π). An πΏ(π)-formula π(π₯) is called an πΏ-interpolant for π and π
if π(π₯) |= π(π₯) and π(π₯) |= π(π₯).
Our concern here is the following πΏ-interpolant existence problem (πΏ-IEP, for short):
(πΏ-IEP) given πΏ-formulas π(π₯) and π(π₯), decide whether they have an πΏ-interpolant π(π₯).
We remind the reader of a well-known criterion of interpolant existence in terms of appropriate
bisimulations. Let π β π. Given pointed π-structures A, π and B, π, we call A, π and B, π πΏ(π)-
equivalent and write A, π β‘πΏ,π B, π if A |= π(π) iff B |= π(π), for all πΏ(π)-formulas π.
Definition 2. A nonempty relation π½ β dom(A)Γdom(B) is called an FO2 2E(π)-bisimulation between
A and B if the following conditions are satisfied for all (π, π) β π½:
1. for every πβ² β dom(A), there is a πβ² β dom(B) such that (πβ² , πβ² ) β π½ and (π, πβ² ) β¦β (π, πβ² ) is a
partial π-isomorphism between A and B;
2. for every πβ² β dom(B), there is a πβ² β dom(A) such that (πβ² , πβ² ) β π½ and (π, πβ² ) β¦β (π, πβ² ) is a
partial π-isomorphism between A and B.
Observe that FO2 2E(π)-bisimulations are global in the sense that dom(A) β {π | (π, π) β π½} and
dom(B) β {π | (π, π) β π½}.
Definition 3. A global relation π½ β dom(A) Γ dom(B) is an GF2 2Ec (π)-bisimulation between A and
B if (πA , πB ) β π½ for all π β π and the following conditions are satisfied for all (π, π) β π½:
1. for every πβ² β dom(A) such that either π
A (π, πβ² ), for some binary π
β π, or πβ² = π, condition 1
of Definition 2 holds;
2. for every πβ² β dom(B) such that either π
B (π, πβ² ), for some binary π
β π, or πβ² = π, condition 2
of Definition 2 holds.
For tuples π = (π1 , . . . , ππ ) and π = (π1 , . . . , ππ ) with π β€ 2, we write A, π βΌπΏ,π B, π if π β¦β π is a
partial π-isomorphism between A and B and there is an πΏ(π)-bisimulation π½ between A and B such
that (ππ , ππ ) β π½, for all π β€ π. The following characterisation is well known; see, e.g., [29, 30, 28]:
Lemma 1. Let πΏ β {FO2 2E, GF2 2Ec } and π β π. For any pointed π-structures A, π and B, π with
|π| = |π|,
A, π βΌπΏ,π B, π implies A, π β‘πΏ,π B, π
and, conversely, if structures A and B are π-saturated [31], then
A, π β‘πΏ,π B, π implies A, π βΌπΏ,π B, π.
Using this lemma, one can obtain the following variant of Robinsonβs joint consistency criterion [32,
25]:
Lemma 2. Let πΏ β {FO2 2E, GF2 2Ec }. Then πΏ(π)-formulas π(π₯) and π(π₯) do not have an πΏ-interpolant
iff there exist pointed πΏ(π)-structures A, π and B, π such that
β’ A |= π(π),
β’ B |= Β¬π(π),
β’ A, π βΌπΏ,π B, π, where π = sig(π) β© sig(π).
Definition 4. Given formulas π(π₯), π(π₯) and a signature π, an explicit π-definition of π(π₯) modulo
π(π₯) in a logic πΏ is an πΏ(π)-formula π(π₯) such that |= π(π₯) β (π(π₯) β π(π₯)).
The explicit π-definition existence problem (EDEP) for πΏ is formulated as follows:
(πΏ-EDEP) given πΏ-formulas π(π₯), π(π₯) and a signature π, decide whether there exists an explicit
π-definition of π(π₯) modulo π(π₯) in πΏ.
The IEP and EDEP turn out to be closely related [33]. Here, we only need the following lemma whose
proof can be found in [26]:
Lemma 3. For any πΏ β {FO2 2E, GF2 2Ec }, the πΏ-IEP is polynomially reducible to the πΏ-EDEP.
3. Undecidability of the FO2 2E-IEP
In this section, we prove the undecidability of the FO2 2E-IEP by a reduction of the undecidable
infinite Post Correspondence Problem (πPCP) [34, 35], which is formulated as follows: given an alphabet
Ξ = {π΄1 , . . . , π΄π }, π β₯ 2, and a finite set π« of pairs (π£1 , π€1 ), . . . , (π£π , π€π ) of non-empty words over
Ξ, decide whether there exists an infinite sequence of indices π1 , π2 , . . . , for 1 β€ ππ β€ π and π < π, such
that the π-words π£π1 π£π2 . . . and π€π1 π€π2 . . . coincide. If this is the case, the πPCP instance π« is said to
have a solution.
Suppose that an πPCP instance π« is given. Our aim is to construct FO2 2E-formulas π(π₯) and π(π₯)
such that π« has a solution iff π(π₯) and Β¬π(π₯) are satisfied in FO2 2E(π)-bisimilar pointed structures,
where π is the shared signature of π and π, and then apply Lemma 2. In our construction π = {π
, π}βͺΞ
with two binary predicates π
, π and the π΄π β Ξ treated as unary predicates. The formula π(π₯) is
defined by taking:
(οΈ )οΈ [οΈ (οΈ )οΈ]οΈ
π(π₯) = π0 (π₯) β§ βπ¦ π
(π₯, π¦) β§ π1 (π¦) β§ βπ₯ π1 (π₯) β βπ¦ π
(π₯, π¦) β§ π2 (π¦) β§
[οΈ (οΈ )οΈ]οΈ (οΈ )οΈ
βπ₯ π2 (π₯) β βπ¦ π
(π₯, π¦) β§ π0 (π¦) β§ βπ₯, π¦ (π0 (π₯) β§ π0 (π¦)) β π₯ = π¦ β§
[οΈ βοΈ (οΈ )οΈ]οΈ
βπ¦ π(π₯, π¦) β§ π΄π (π¦) β π΄π (π¦) .
π΄π βΞ
The only purpose of π(π₯) is to generate an π
-cycle with three points: for any structure A, π0 , if
A |= π(π0 ), then A contains a cycle π
(π0 , π1 ), π
(π1 , π2 ), π
(π2 , π0 ). The last conjunct of π is needed
to ensure that sig(π) β© sig(π) = π.
Before defining π(π₯) formally, we explain the intuition behind Β¬π(π₯). Suppose A, π0 and B, π0
are such that A |= π(π0 ), B |= Β¬π(π0 ) and A, π0 βΌπΏ,π B, π0 , for πΏ = FO2 2E. Then B contains an
π
-chain . . . πβ3 , πβ2 , πβ1 , π0 , π1 , π2 , π3 , . . . such that A, π0 βΌπΏ,π B, π3π , for π β Z. The purpose of the
formula Β¬π(π₯) is to generate an infinite π-chain π£ starting from π0 , along which an infinite sequence
of words π£π , π < π, is written, and also an infinite π-chain π€ starting from π3 , along which a sequence
of words π€π , π < π, is written. Using the equivalence relations πΈ1 and πΈ2 , the formula Β¬π(π₯) ensures
that the respective pairs (π£π , π€π ), π < π, are all in π«. That the resulting π-words coincide (and give a
solution to π«) is ensured by A, π0 βΌπΏ,π B, π0 . The intended models A, π0 and B, π0 are illustrated in
Fig. 1.
To define Β¬π formally, suppose π£π = π΄π1 . . . π΄πππ and π€π = π΅1π . . . π΅π π
π , for 1 β€ π β€ π, ππ β₯ 1, and
ππ β₯ 1. Along with the π΄π β Ξ, to generate unique π-chains π£ and π€, we require auxiliary unary
predicates ππ£ππ , π = 1, . . . , ππ , and ππ€π π , π = 1, . . . , ππ , as well as πππ£ and πππ€ , for π = 1, 2, and π π£ , π π€ .
Let 1Μ = 2, 2Μ = 1, π₯Β― = π¦, and π¦Β― = π₯.
We define Β¬π(π₯) to be a conjunction of the following four groups of formulas:
(generation) π1π£ (π₯) β§ π π£ (π₯), βπ₯, π¦ π π’ (π₯) β§ π(π₯, π¦) β π π’ (π¦) , for π’ β {π£, π€},
(οΈ )οΈ
βπ₯ πππ£ (π₯) β πβ€π πππ (π₯) , βπ₯ πππ€ (π₯) β πβ€π πππ (π₯) , for π = 1, 2,
(οΈ βοΈ )οΈ (οΈ βοΈ )οΈ
(οΈ )οΈ (οΈ )οΈ
βπ¦ π
(π₯, π¦) β π1 (π¦) , βπ₯, π¦ π1 (π₯) β§ π
(π₯, π¦) β (οΈ π2 (π¦) ,
βπ₯, π¦ π2 (π₯) β§ π
(π₯, π¦) β π1π€ (π¦) β§ π π€ (π¦) ,
)οΈ
where, the formula πππ generating the word π£π , for π = 1, 2, is defined recursively as
πππ (π₯) = πΌπ,1
π π
(π₯) β§ π½π,1 (π₯),
π
Β― ) β§ π΄ππ (π₯
Β― ) β§ ππ£ππ (π₯ π )οΈ
πΌπ,π (π₯) = βπ₯ Β― (π(π₯, π₯ Β― ) β§ πΈπ (π₯, π₯ Β― ) β§ πΌπ,π+1 (π₯ Β― ) , for π = 1, . . . , ππ β 1,
π π
Β― ) β§ π΄πππ (π₯ Β― ) β§ πΒ―ππ£ (π₯
(οΈ )οΈ
πΌπ,π π
(π₯) = βπ₯
Β― π(π₯, π₯ Β― ) β§ πΈπ (π₯, π₯ Β― ) β§ ππ£ππ (π₯ Β―) ,
π
Β― ) β§ π΄ππ (π₯
Β― ) β§ ππ£ππ (π₯ π
(οΈ )οΈ
π½π,π (π₯) = βπ₯ Β― π(π₯, π₯ Β― ) β πΈπ (π₯, π₯ Β― ) β§ π½π,π+1 Β― ) , for π = 1, . . . , ππ β 1,
(π₯
π (οΈ π ππ π£
)οΈ
π½π,π π
(π₯) = βπ₯
Β― π(π₯, π₯
Β― ) β πΈ π (π₯, π₯
Β― ) β§ π΄ π π
(π₯
Β― ) β§ π π£π (π₯
Β― ) β§ πΒ―π (π₯Β― ) ,
.. .. ..
. . .
.. .. .. .. ..
. . . . .
πΈ1
π π π π π
π1π3 π1π3 π1π3
π΄ππ2π2 π΄ππ2π2 π1π€ π1π£ π1π€
ππ ππ ππ
ππ€π22 ππ£π22 ππ€π22
.. .. .. .. ..
. π£π2 . π£π2 . . .
πΈ2
π΄π12 π΄π12 ππ€1 π2 ππ£1π2 ππ€1 π2
π π π π π
π2π2 π2π2 π2π2
π΄ππ1π1 π΄ππ1π1 π2π€ π2π£ π2π€
ππ ππ ππ
ππ€π11 ππ£π11 ππ€π11
.. .. .. .. ..
. . . . .
π£π1 π£π1
π΄π21 π΄π21 ππ€2 π1 ππ£2π1 ππ€2 π1
πΈ1
π π π π π
π΄π11 π΄π11 ππ€1 π1 ππ£1π1 ππ€1 π1
π π π
π π
π1π€ π1π1 π1π£ π1π1 π1π€ π11
π
... ...
π
π
π
π0 π
π
πβ3 π
πβ2 π
πβ1 π
π0 π
π1 π
π2 π
π3 π
π
π2 π1
π
A B
Figure 1: Intended models A, π0 and B, π0 with A |= π(π0 ), B |= Β¬π(π0 ), and A, π0 βΌπΏ,π B, π0 , where
π-bisimilar points in the disjoint union of A and B are connected by dotted lines and πΈπ -equivalence classes in
B, π = 1, 2, are encircled by dashed lines. Model A contains two disjoint copies of a 3-point π
-cycle followed by
an infinite π-chain. Model B has an infinite π
-chain of points ππ , for π β Z; each π6π starts an infinite π-chain for
the word π£π1 π£π2 . . . , and each π6π+3 starts an infinite π-chain for the word π€π1 π€π2 . . . . These π-words coincide
with the π-word written on the π-chains in A.
and the formulas πππ , generating the respective words π€π , are defined analogously but with π΅ππ , ππ€π π
and ππ in place of π΄ππ , ππ£ππ and ππ , respectively.
(disjointness) βπ₯ π (π₯) β Β¬π β² (π₯) , for any distinct π, π β² β Ξ, distinct π, π β² of the form ππ£ππ , ππ€π π ,
(οΈ )οΈ
as well as for {π, π β² } = {π1π’ , π2π’ } with π’ β {π£, π€}, and {π, π β² } = {π π£ , π π€ }.
(οΈ )οΈ
(coordination) βπ₯, π¦ π
(π₯, π¦) β πΈ1 (π₯, π¦) ,
βπ₯ π(οΈππ£ (π₯) β§ πππ (π₯) β βπ¦ πΈπ (π₯, π¦) β§ πππ€ (π¦) β πππ (π¦) , for π = 1, 2, π β€ π,
[οΈ (οΈ )οΈ]οΈ
βπ₯, π¦ πΈπ (π₯, π¦) β§ πΒ―ππ£ (π₯) β§ πΒ―ππ€ (π¦) β πΈΒ―π (π₯, π¦) , for π = 1, 2.
)οΈ
(uniqueness) βπ₯, π¦ π (π₯) β§ π (π¦) β§ πΈπ (π₯, π¦) β π₯ = π¦ , for π of the form ππ£ππ , ππ€π π , π = 1, 2.
(οΈ )οΈ
Clearly π = sig(π) β© sig(π) consists of π
, π and the predicates in Ξ.
We now show that the constructed FO2 2E-formulas π and π are as required:
Theorem 4. Let π and π be the FO2 2E-formulas defined above for a given πPCP instance π«. Then π« has a
solution iff there exist structures A, π and B, π such that A |= π(π), B |= Β¬π(π), and A, π βΌFO2 2E,π B, π.
Proof. (β) Suppose that π£π1 π£π2 Β· Β· Β· = π€π1 π€π2 . . . is a solution to the given π«. It is not hard to
check that, for the structures A and B shown in Fig. 1, we have A |= π(π0 ), B |= Β¬π(π0 ), and
A, π0 βΌFO2 2E(π) B, π0 . It is to be noted that a formula enforcing a 3-point cycle is needed as a 1- or
2-point cycle is not FO2 2E(π)-bisimilar to a chain. Also note that two disjoint copies of a 3-point
π
-cycle followed by an π-chain in A are needed to ensure FO2 2E(π)-bisimilarity between A, π0 and
B, π0 . Indeed, suppose, for example, that π and π are the πth points in the π-chains starting from π0
and π0 , respectively. Now, if we consider the (π + 1)th point πβ² in the π-chain starting from π3 , then,
to obtain a partial π-isomorphism between (π, πβ² ) and some (π, πβ² ), we may need to take the (π + 1)th
point πβ² from the second π-chain in A.
(β) Suppose A |= π(π0 ), B |= Β¬π(π0 ), and A, π0 βΌFO2 2E,π B, π0 . Consider first the pointed
structure B, π0 . As B |= Β¬π(π0 ), the axioms in the first two lines of (generation) give an infinite
sequence π£ = π£ π1 π£ π2 . . . depicted below.
πΈ2
πΈ1 πΈ1
π1 1 π π΄ππ1π1 π2 2 π π΄ππ2π2
π π΄1 π π΄2 π π΄1 π π΄2
π0 . π. . . π. . ... ...
π1π£ ππ£1π1 ππ£2π1
ππ
ππ£π11π2π£ ππ£1π2 ππ£2π2
ππ
ππ£π22π1π£
π£ = π£ π1 π£ π2 π£ π3
We show that the π-word π£π1 π£π2 . . . over Ξ, i.e.,
π΄π11 π΄π21 . . . π΄ππ1π π΄π12 π΄π22 . . . π΄ππ2π . . .
1 2
β β β β
π£π1 π£π2
written on π£ is unique. Indeed, by (disjointness) and (generation), all π-successors ofπ0 carry the
same ππ£1π , all of them are in the same πΈ1 -equivalence class, and so must coincide by (uniqueness).
1
Next we see that all of the π-successors of the ππ£1π -point carry ππ£2π , and so must coincide, etc. This
1 1
gives us the word π£π1 carried by the segment π£ π1 sitting in the same πΈ1 -equivalence class. The last point
in this segment carries π2π£ , which triggers the next segment π£ π2 sitting in the same πΈ2 -equivalence
class, and so on. All of the points in π£ carry π π£ by the second formula in (generation). The points on
the boundaries between π£ ππ and π£ ππ+1 belong to both πΈ1 - and πΈ2 -equivalence classes.
As A, π0 βΌπΏ,π B, π0 , π
β π and π
(π0 , π1 ), π
(π1 , π2 ), π
(π2 , π0 ), Definition 2 gives points ππ , π > 0, in
B such that π
(π0 , π1 ), π
(π1 , π2 ), π
(π2 , π3 ) and π3 βΌπΏ,π π0 . By the third and fourth lines in (generation),
we have π1π€ (π3 ), π π€ (π3 ), and so, by (disjointness), π0 ΜΈ= π3 . By the first formula in (coordination),
we must have πΈ1 (π0 , π3 ).
The same argument as for π0 above gives us an π-chain π€ starting from π3 and disjoint from π£ in
view of (disjointness) that defines uniquely an π-word π€πβ²1 π€πβ²2 . . . over Ξ. The chain π€ consists of
consecutive segments π€πβ²1 , π€πβ²2 , . . . such that π€πβ²1 sits in the same πΈ1 -equivalence class as π£ π1 , π€πβ²2 sits
in an πΈ2 -equivalence class, π€πβ²3 in an πΈ1 -equivalence class, etc.
By the second formula in (coordination), we have π1 = πβ²1 , and so (π£π1 , π€πβ²1 ) β π«; by the third one,
the ends of π£ π1 and π€π1 are πΈ2 -related, from which π2 = πβ²2 and (π£π2 , π€πβ²2 ) β π«. The ends of π£ π2 and
π€π2 are πΈ1 -related, so π3 = πβ²3 and (π£π3 , π€πβ²3 ) β π«, etc.
Finally, let π£ be π(π0 , π0 ), π(π0 , π1 ), . . . and let π€ be π(π3 , π0 ), π(π0 , π1 ), . . . . Since these π-chains
are unique and π3 βΌπΏ,π π0 , we must have ππ βΌπΏ,π ππ , for all π < π. It follows that the Ξ-symbols carried
by each pair ππ and ππ must coincide, which gives a solution to π«. β£
Since the πPCP is undecidable, as an immediate consequence of Theorem 4 and Lemma 3 we obtain
our main result:
Theorem 5. The FO2 2E-IEP and FO2 2E-EDEP are both undecidable.
4. Undecidability of the IEP for Guarded and Description Logics
It is not hard to tweak the construction in the previous section to show that the GF2 2Ec -IEP is also
undecidable. Observe that the formula π defined above can be equivalently represented as a formula in
GF2 2Ec and that the FO2 2E(π)-bisimulation between A and B is actually a GF2 2Ec (π)-bisimulation
(οΈ to have one copy of the π
-cycle
(in this case, it is actually enough )οΈ with an π-chain in A). The only
unguarded conjunct of π is βπ₯, π¦ (π0 (π₯) β§ π0 (π¦)) β π₯ = π¦ , which is needed to generate an π
-cycle
with three points. The same result can be achieved using a guarded πβ² with two individual constants π1
and π2 as follows:
βοΈ (οΈ
πβ² (π₯) = π
(π₯, π1 ) β§ π
(π1 , π2 ) β§ π
(π2 , π₯) β§ βπ¦ π(π₯, π¦) β§
[οΈ )οΈ]οΈ
π΄π (π¦) β π΄π (π¦) .
π΄π βΞ
We then obtain Theorem 4 with πβ² and GF2 2Ec in place of π and FO2 2E, respectively, and, as an
immediate consequence, the following:
Theorem 6. The GF2 2Ec -IEP and GF2 2Ec -EDEP are both undecidable.
These undecidability results can be interpreted as results about description logics with Boolean
operators on roles that correspond to the two-variable fragments [36, 37]. The crucial operators
required are role intersection, negation, and the identity role. Denote by πβπ β©,Β¬,id 2E the extension of
the basic description logic πβπ with the operators β© and Β¬ on roles, the identity role id interpreted
as {(π, π) | π β dom(A)} in any structure A, and two equivalence relations. The interpolant existence
problem for πβπ β©,Β¬,id 2E (or πβπ β©,Β¬,id 2E-IEP, for short) is the problem to decide, given πβπ β©,Β¬,id 2E-
concepts πΆ1 and πΆ2 , whether there exists an πβπ β©,Β¬,id 2E-concept πΆ built from the shared concept
and role names from πΆ1 and πΆ2 such that πΆ1 β πΆ and πΆ β πΆ2 are valid concept inclusions. We then
obtain the following:
Theorem 7. The πβπ β©,Β¬,id 2E-IEP and πβπ β©,Β¬,id 2E-EDEP are both undecidable.
To obtain a DL version of the undecidability for the GF2 2Ec -IEP, we can add nominals and the
universal role to πβπ β©,Β¬,id 2E and, to reflect guarded quantification, admit only Boolean combinations
of roles that contain at least one positive occurrence of a role name that is different from the universal
role.
5. Open Problems
This paper presents first examples of decidable fragments of first-order logic, for which the interpolant
existence problem and the explicit definition existence problem are undecidable. Numerous questions
remain open, including the following:
β’ Is the IEP decidable for FO2 1E, that is, FO2 with one equivalence relation? Note that the
decidability and coNExpTime-completeness proofs for FO2 1E are significantly less involved than
those for FO2 2E [28]. What happens if we extend FO2 with a single transitive (rather than
equivalence) relation?
β’ Is the FO2 2E-IEP still undecidable if one drops equality from FO2 ? Note that, for FO2 without
equivalence relations and without equality, the IEP is decidable and the known complexity bounds
are the same as for the case with equality [26].
β’ Is the IEP decidable for πβππ¬βπͺ? What about C2 , that is, FO2 with counting quantifiers ββ₯π π₯,
π β N? A possible hint that the IEP for C2 might be undecidable is given by a recent result of [38]
according to which the following related separation problem is undecidable: given two mutually
exclusive C2 -formulas π and π, decide whether there exists an FO2 -formula π, called a separator
for π and π, such that π |= π and π |= Β¬π.
References
[1] K. L. McMillan, Interpolation and SAT-based model checking, in: Proceedings of the 15th
International Conference on Computer Aided Verification, CAV 2003, Springer, 2003, pp. 1β13.
URL: https://doi.org/10.1007/978-3-540-45069-6_1. doi:10.1007/978-3-540-45069-6\_1.
[2] R. Diaconescu, Logical support for modularisation, Logical environments 83 (1993) 130.
[3] A. Cimatti, A. Griggio, R. Sebastiani, Interpolant generation for UTVPI, in: Proceedings of the
22nd International Conference on Automated Deduction, CADE 2022, Springer, 2009, pp. 167β182.
URL: https://doi.org/10.1007/978-3-642-02959-2_15. doi:10.1007/978-3-642-02959-2\_15.
[4] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Combined covers and Beth definability,
in: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4,
2020, Proceedings, Part I, 2020, pp. 181β200. URL: https://doi.org/10.1007/978-3-030-51074-9_11.
doi:10.1007/978-3-030-51074-9\_11.
[5] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Combination of uniform inter-
polants via Beth definability, J. Autom. Reason. 66 (2022) 409β435. URL: https://doi.org/10.1007/
s10817-022-09627-1. doi:10.1007/s10817-022-09627-1.
[6] D. Toman, G. E. Weddell, Fundamentals of Physical Design and Query Compilation, Synthesis
Lectures on Data Management, Morgan & Claypool Publishers, 2011.
[7] M. Benedikt, J. Leblay, B. ten Cate, E. Tsamoura, Generating Plans from Proofs: The Interpolation-
based Approach to Query Reformulation, Synthesis Lectures on Data Management, Morgan &
Claypool Publishers, 2016.
[8] B. ten Cate, E. Franconi, I. Seylan, Beth definability in expressive description logics, J. Artif. Intell.
Res. 48 (2013) 347β414.
[9] M. Benedikt, B. ten Cate, M. Vanden Boom, Effective interpolation and preservation in guarded
logics, ACM Trans. Comput. Log. 17 (2016) 8. URL: https://doi.org/10.1145/2814570. doi:10.1145/
2814570.
[10] B. ten Cate, W. Conradie, M. Marx, Y. Venema, Definitorially complete description logics, in: Proc.
of KR, 2006, pp. 79β89.
[11] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On free description logics with definite descriptions,
in: Proceedings of the 18th International Conference on Principles of Knowledge Representation
and Reasoning, KR 2021, 2021, pp. 63β73. URL: https://doi.org/10.24963/kr.2021/7. doi:10.24963/
kr.2021/7.
[12] D. Geleta, T. R. Payne, V. A. M. Tamma, An investigation of definability in ontology alignment,
in: E. Blomqvist, P. Ciancarini, F. Poggi, F. Vitali (Eds.), Knowledge Engineering and Knowledge
Management - 20th International Conference, EKAW 2016, Bologna, Italy, November 19-23, 2016,
Proceedings, volume 10024 of Lecture Notes in Computer Science, 2016, pp. 255β271. URL: https:
//doi.org/10.1007/978-3-319-49004-5_17. doi:10.1007/978-3-319-49004-5\_17.
[13] B. Konev, C. Lutz, D. Walther, F. Wolter, Formal properties of modularisation, in: H. Stuckenschmidt,
C. Parent, S. Spaccapietra (Eds.), Modular Ontologies: Concepts, Theories and Techniques for
Knowledge Modularization, volume 5445 of Lecture Notes in Computer Science, Springer, 2009, pp.
25β66. URL: https://doi.org/10.1007/978-3-642-01907-4_3. doi:10.1007/978-3-642-01907-4\
_3.
[14] E. Botoeva, B. Konev, C. Lutz, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Inseparability and
conservative extensions of description logic ontologies: A survey, in: J. Z. Pan, D. Calvanese,
T. Eiter, I. Horrocks, M. Kifer, F. Lin, Y. Zhao (Eds.), Reasoning Web: Logical Foundation of
Knowledge Graph Construction and Query Answering - 12th International Summer School 2016,
Aberdeen, UK, September 5-9, 2016, Tutorial Lectures, volume 9885 of Lecture Notes in Computer
Science, Springer, 2016, pp. 27β89. URL: https://doi.org/10.1007/978-3-319-49493-7_2. doi:10.1007/
978-3-319-49493-7\_2.
[15] I. Seylan, E. Franconi, J. de Bruijn, Effective query rewriting with ontologies over DBoxes, in:
Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, 2009,
pp. 923β925. URL: http://ijcai.org/Proceedings/09/Papers/157.pdf.
[16] D. Toman, G. E. Weddell, First order rewritability for ontology mediated querying in Horn-DLFD,
in: Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located
with the 17th International Conference on Principles of Knowledge Representation and Reasoning
(KR 2020), Online Event [Rhodes, Greece], September 12th to 14th, 2020, 2020.
[17] E. Franconi, V. Kerhet, N. Ngo, Exact query reformulation over databases with first-order and
description logics ontologies, J. Artif. Intell. Res. 48 (2013) 885β922. URL: https://doi.org/10.1613/
jair.4058. doi:10.1613/jair.4058.
[18] E. Franconi, V. Kerhet, Effective query answering with ontologies and DBoxes, in: Description
Logic, Theory Combination, and All That, Springer, 2019, pp. 301β328.
[19] D. Toman, G. E. Weddell, FO Rewritability for OMQ using Beth Definability and Interpolation, in:
Proceedings of the 34th International Workshop on Description Logics, DL 2021, CEUR-WS.org,
2021. URL: http://ceur-ws.org/Vol-2954/paper-29.pdf.
[20] S. D. Comer, Classes without the amalgamation property., Pacific J. Math. 28 (1969) 309β318.
[21] D. Pigozzi, Amalgamation, congruence-extension, and interpolation properties in algebras, Algebra
Univers. (1971) 269β349.
[22] M. Marx, C. Areces, Failure of interpolation in combined modal logics, Notre Dame J. Formal Log.
39 (1998) 253β273.
[23] A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, F. Wolter, Living without Beth and Craig: Definitions
and interpolants in description and modal logics with nominals and role inclusions, ACM Trans.
Comput. Log. 24 (2023) 34:1β34:51. URL: https://doi.org/10.1145/3597301. doi:10.1145/3597301.
[24] M. Fortin, B. Konev, F. Wolter, Interpolants and explicit definitions in extensions of the description
logic β°β, in: Proceedings of the 19th International Conference on Principles of Knowledge
Representation and Reasoning, KR 2022, 2022.
[25] J. C. Jung, F. Wolter, Living without Beth and Craig: Definitions and interpolants in the guarded
and two-variable fragments, in: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
in Computer Science, LICS 2021, IEEE, 2021, pp. 1β14. URL: https://doi.org/10.1109/LICS52264.
2021.9470585. doi:10.1109/LICS52264.2021.9470585.
[26] A. Kurucz, F. Wolter, M. Zakharyaschev, Definitions and (uniform) interpolants in first-order
modal logic, in: P. Marquis, T. C. Son, G. Kern-Isberner (Eds.), Proceedings of the 20th International
Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece,
September 2-8, 2023, 2023, pp. 417β428. URL: https://doi.org/10.24963/kr.2023/41. doi:10.24963/
KR.2023/41.
[27] E. Kieronski, J. Michaliszyn, I. Pratt-Hartmann, L. Tendera, Two-variable first-order logic with
equivalence closure, SIAM J. Comput. 43 (2014) 1012β1063. URL: https://doi.org/10.1137/120900095.
doi:10.1137/120900095.
[28] I. Pratt-Hartmann, Fragments of First-Order Logic, Oxford Logic Guides, Oxford University Press,
United Kingdom, 2023.
[29] V. Goranko, M. Otto, Model theory of modal logic, in: Handbook of Modal Logic, Elsevier, 2007,
pp. 249β329.
[30] E. GrΓ€del, M. Otto, The freedoms of (guarded) bisimulation, in: Johan van Benthem on Logic and
Information Dynamics, Springer International Publishing, 2014, pp. 3β31.
[31] C. Chang, H. J. Keisler, Model Theory, Elsevier, 1998.
[32] A. Robinson, A result on consistency and its application to the theory of definition, Indagationes
Mathematicae 18 (1956) 47β58.
[33] D. M. Gabbay, L. Maksimova, Interpolation and Definability: Modal and Intuitionistic Logics,
Oxford, England: Oxford University Press UK, 2005.
[34] K. Ruohonen, Reversible machines and Postβs correspondence problem for biprefix morphisms, J.
Inf. Process. Cybern. 21 (1985) 579β595.
[35] F. Gire, Two decidability problems for infinite words, Inf. Process. Lett. 22 (1986) 135β140. URL:
https://doi.org/10.1016/0020-0190(86)90058-X. doi:10.1016/0020-0190(86)90058-X.
[36] C. Lutz, U. Sattler, F. Wolter, Description logics and the two-variable fragment, in: C. A.
Goble, D. L. McGuinness, R. MΓΆller, P. F. Patel-Schneider (Eds.), Working Notes of the 2001
International Description Logics Workshop (DL-2001), Stanford, CA, USA, August 1-3, 2001, vol-
ume 49 of CEUR Workshop Proceedings, CEUR-WS.org, 2001. URL: https://ceur-ws.org/Vol-49/
LutzSattlerWolter-66start.ps.
[37] C. Lutz, U. Sattler, F. Wolter, Modal logic and the two-variable fragment, in: L. Fribourg (Ed.),
Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of
the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in
Computer Science, Springer, 2001, pp. 247β261. URL: https://doi.org/10.1007/3-540-44802-0_18.
doi:10.1007/3-540-44802-0\_18.
[38] L. Kuijer, T. Tan, F. Wolter, M. Zakharyaschev, Separating counting from non-counting in fragments
of two-variable first-order logic (extended abstract), in: Proceedings of the 37th International
Workshop on Description Logics, CEUR Workshop Proceedings, CEUR-WS.org, 2024.