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.
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 [
For many fragments of FO, including many description logics (DLs), the existence of a Craig
interpolant 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 ℒℐ [
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 [
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 ℒℋ [
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.
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 : FO22E( ) 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 ; GF22Ec( ) admits variables in var and individual constants in atoms but restricts quantification to the patterns ∀ (︀ (, ) → (, ))︀ , ∃ (︀ (, ) ∧ (, ))︀ , where (, ) is a GF22Ec-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 FO22E and GF22Ec are known to be co2NExpTime- and 2ExpTimecomplete, respectively; see [27, 28] and references therein.
Definition 1. Let ∈ {FO22E, GF22Ec}, 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 |= () if B |= (), for all ()-formulas . Definition 2. A nonempty relation ⊆ dom(A)× dom(B) is called an FO22E()-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 FO22E()-bisimulations are global in the sense that dom(A) ⊆ { | (, ) ∈ } and dom(B) ⊆ { | (, ) ∈ }.
Definition 3. A global relation ⊆ dom(A) × dom(B) is an GF22Ec()-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 ∈ {FO22E, GF22Ec} 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 ∈ {FO22E, GF22Ec}. Then ( )-formulas () and () do not have an -interpolant if 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 ∈ {FO22E, GF22Ec}, the -IEP is polynomially reducible to the -EDEP. 3. Undecidability of the FO22E-IEP In this section, we prove the undecidability of the FO22E-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 FO22E-formulas () and () such that has a solution if () and ¬ () are satisfied in FO22E( )-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 = FO22E. 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 2 1
2 and in place of , and , respectively. and the formulas , generating the respective words , are defined analogously but with , (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 FO22E-formulas and are as required: 01 = 11 21 11 1 21 1 We show that the -word 1 2 . . . over Γ, i.e., 1 3 . . .
. . . 2 2 . ..
11 12 22 12 1 12 22 . ..
22 21 2 11 21 . . . 11 12 22 . . . 22 . . . ⏟ 1⏞ ⏟ 2⏞ Theorem 4. Let and be the FO22E-formulas defined above for a given PCP instance . Then has a solution if there exist structures A, and B, such that A |= (), B |= ¬ (), and A, ∼ FO22E, 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 ∼ FO22E() 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 FO22E()-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 FO22E()-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 ∼ FO22E, 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. written on is unique. Indeed, by (disjointness) and (generation), all -successors of0 carry the same 11 , all of them are in the same 1-equivalence class, and so must coincide by (uniqueness). Next we see that all of the -successors of the 11 -point carry 21 , and so must coincide, etc. This 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 FO22E-IEP and FO22E-EDEP are both undecidable.
It is not hard to tweak the construction in the previous section to show that the GF22Ec-IEP is also undecidable. Observe that the formula defined above can be equivalently represented as a formula in GF22Ec and that the FO22E()-bisimulation between A and B is actually a GF22Ec()-bisimulation (in this case, it is actually enough to have one copy of the -cycle 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 GF22Ec in place of and FO22E, respectively, and, as an immediate consequence, the following: Theorem 6. The GF22Ec-IEP and GF22Ec-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 ℒ∩,¬,id2E 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 ℒ∩,¬,id2E (or ℒ∩,¬,id2E-IEP, for short) is the problem to decide, given ℒ∩,¬,id2Econcepts 1 and 2, whether there exists an ℒ∩,¬,id2E-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 ℒ∩,¬,id2E-IEP and ℒ∩,¬,id2E-EDEP are both undecidable.
To obtain a DL version of the undecidability for the GF22Ec-IEP, we can add nominals and the universal role to ℒ∩,¬,id2E and, to reflect guarded quantification, admit only Boolean combinations of roles that contain at least one positive occurrence of a role name that is diferent from the universal role.
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 FO21E, that is, FO2 with one equivalence relation? Note that the decidability and coNExpTime-completeness proofs for FO21E are significantly less involved than those for FO22E [28]. What happens if we extend FO2 with a single transitive (rather than equivalence) relation? • Is the FO22E-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 |= ¬ . [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, Efective 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, volume 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.