We consider the problem of deciding whether two disjoint classes of models defined in a fragment of first-order logic (FO) with counting can be separated in the same fragment but without counting. This problem turns out to be hard. We show that separation for the two-variable fragment FO2 extended with counting quantifiers by means of plain FO2 is undecidable, and the same is true of the pair ℒℐ/ℒℐ of description logics. On the other hand, we establish 2ExpTime-completeness of the separation problem for the pairs ℒ/ℒ and ℒℐ/ℒℐ.
Our concern in this paper is the following separation problems for a pair of languages and :
/-separation: given two mutually exclusive -formulas and , decide whether there exists an
-formula —a separator for and —such that |= and |= ¬ ;
Craig /-separation: decide whether the given -formulas and have an -separator that
only contains common non-logical symbols (predicates and functions) of and .
To illustrate, could be an ontology and a concept that is not satisfiable with respect to , both
given in an expressive language . Then a separator ontology ′ in a weaker, easier to comprehend
language potentially explains unsatisfiability as it inherits that |= ′ and is not satisfiable under
′. Also, in the context of concept learning, and could represent positive and negative examples
for a target concept . Then any separator in an appropriately chosen language could represent the
concept one aims to learn [
Separation generalises definability (aka membership), which asks whether a given -formula (say, a
datalog query) is equivalent to some -formula (say, a first-order query), and is regarded as one of
the main approaches to understanding the expressive power of relative to . For instance, studying
separability of regular languages by smaller language classes (e.g., a star-free language) has brought
major insights into the respective formal languages, with some fundamental open problems in the area
cast as separation questions [
Craig /-separation generalises classical Craig interpolation in [
Our aim in this paper is to investigate the decidability and complexity of the separation problem for certain fragments of C2—that is, the two-variable first-order logic FO2 extended with counting quantifiers—and the same fragments but without counting.
Example 1. Consider the following C2-formulas: () = ∃=1 (, ),
() = ∃=1 (︀ (, ) ∧ ())︀ ∧ ∃=1 (︀ (, ) ∧ ¬())︀ .
Then |= ¬ and the FO2-formula () = ∀ (︀ (, ) → ())︀ ∨ ∀ (︀ (, ) → ¬())︀ is a separator for () and (). For ′() = ∃=2 (, ), we also have |= ¬ ′, but () and ′() are not separable in FO2. On the other hand, there is no Craig FO2-separator for () and () as it would have to be defined using only, and so separate () and ′() as well.
The logics we consider here can all be regarded as fragments of first-order logic, FO, and are defined as follows. Let be a signature containing unary and binary relation symbols and possibly constants. Fix a set var comprising two individual variables. Then FO2( ), the two-variable fragment of FO( ), is defined as the set of formulas that are built from atoms (), (, ), and = with unary ∈ , binary ∈ , and , ∈ var, using the Boolean connectives ∧ and ¬ and quantifier ∃ with ∈ var (other Booleans and ∀ are regarded as standard abbreviations); C2( ), the two-variable fragment of FO2( ) with counting, extends FO2( ) with the counting quantifiers ∃<, for ∈ N and ∈ var (other counting quantifiers ∃=, ∃≤ , ∃≥ can be introduced as abbreviations).
In this paper, we are only interested in formulas () with one free variable ∈ var. The signature of is the set sig ( ) of relation and constant symbols occurring in .
FO( ) and its fragments are interpreted in -structures A = (dom(A), (A)∈ , (A)∈ ) with a domain dom(A) ̸= ∅, relations A on dom(A) of the same arity as ∈ , and elements A ∈ dom(A). A pointed structure is a pair A, with ∈ dom(A).
We also consider a few fragments of C2 that correspond to some standard description logics (DLs).
In the context of DLs, unary relation symbols are called concept names, binary ones role names, and
constants individual names [
An ℒℐ( )-concept is defined by the grammar
::= ⊤ | | {} | ¬ | ⊓ ′ | ≥ . | ∃., where ∈ is a concept, ∈ an individual, a role name in or its inverse, and > 0. We consider several fragments of ℒℐ. The weakest, ℒ, is obtained by dropping the universal role (indicated by omitting · from the name), inverse roles (indicated by omitting ℐ), nominals (indicated by omitting ), and only admitting qualified number restrictions of the form ∃. = (≥ 1 .) (indicated by dropping ). The languages between ℒ and ℒℐ are now defined in the obvious way.
The semantics of DLs can be defined via the standard translation · ♯ into C2 with constants. For any ℒℐ-concept , we denote by ♯ the C2-formula with constants and free variable ∈ var defined inductively by taking ⊤♯ = ( = ), ♯ = (),
{}♯ = ( = ), (¬)♯ = ¬♯, ( ⊓ )♯ = ♯ ∧ ♯, (∃.)♯ = ⊤ ∧ ∃¯ ¯, (≥ .)♯ = ∃≥ ¯ (︀ (, ¯) ∧ ¯♯︀) ,
♯ ♯ where ¯= , ¯= and {, } = var.
The complexities of the satisfiability problems for the logics in question are as follows [
Our main results are summarised in the next theorem: Theorem 1. The separation and Craig separation problems are • undecidable for the pairs C2/FO2 and ℒℐ/ℒℐ, • 2ExpTime-complete for the pairs ℒℐ/ℒℐ and ℒ/ℒ.
The proof of Theorem 1 is based on the following straightforward model-theoretic characterisation
of separation in terms of bisimulations; see [
A |= (),
B |= (),
A, ∼ () B, .
For Craig separation, we additionally require that ⊆ sig ( ) ∩ sig ( ).
Here, A, ∼ () B, means that there is an ()-bisimulation between A and B such that
(, ) ∈ , which implies that A |= () if B |= (), for all ()-formulas () [
With the exception of separating modal -calculus formulas by plain modal formulas [
Craig separators are a generalisation of Craig interpolants where = . If the logic has the
Craig interpolation property (CIP), then the Craig separator existence problem for and reduces to
checking whether |= and is thus not harder than entailment. Only recently the problem of deciding
the existence of Craig interpolants has been considered for logics without the CIP [20, 21]. In fact, the
bisimulation-based method employed here makes heavy use of techniques introduced for checking
Craig interpolant existence [
We have started investigating the separation problem for fragments of FO with counting by formulas in the same fragments but without counting. Many problems remain to be addressed; we mention a few of them below: 1. Our decidability proofs are non-constructive, and it would be of interest to develop algorithms that construct separators whenever they exist and determine bounds on their size. 2. With the exception of ℒ, the logics with counting we considered do not have the finite model property. It would be of interest to investigate whether our results also hold on finite structures. In that case, the bisimulation criterion does not hold as formulated (because its proof uses compactness) and one has to employ a diferent criterion that holds on finite structures (say, bounded bisimulations). 3. Our logics have the universal role. We conjecture that without the universal role ℒ/ℒand ℒℐ/ℒℐ-separation becomes coNExpTime-complete. 4. Is definability less complex than separation for the pairs of languages considered here. For example, is C2/FO2-definability decidable? [13] T. Place, Separating regular languages with two quantifier alternations, Log. Methods Comput.
Sci. 14 (2018). URL: https://doi.org/10.23638/LMCS-14(4:16)2018. doi:10.23638/LMCS-14(4:16) 2018. [14] C. Lutz, R. Piro, F. Wolter, Description Logic TBoxes: Model-Theoretic Characterizations and
Rewritability, in: IJCAI, 2011, pp. 983–988. [15] M. Benedikt, B. ten Cate, M. Vanden Boom, Efective interpolation and preservation in guarded logics, ACM Trans. Comput. Log. 17 (2016) 8. URL: https://doi.org/10.1145/2814570. doi:10.1145/ 2814570. [16] V. Bárány, M. Benedikt, B. ten Cate, Some model theory of guarded negation, J. Symb. Log. 83 (2018) 1307–1344. [17] M. Otto, Eliminating recursion in the -calculus, in: C. Meinel, S. Tison (Eds.), STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, Springer, 1999, pp. 531–540. URL: https://doi.org/10.1007/3-540-49116-3_50. doi:10.1007/3-540-49116-3\_50. [18] A. Bötcher, C. Lutz, F. Wolter, Ontology approximation in Horn description logics, in: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, 2019, pp. 1574–1580. URL: https://doi.org/10.24963/ijcai.2019/218. doi:10.24963/IJCAI.2019/218. [19] B. Konev, C. Lutz, F. Wolter, M. Zakharyaschev, Conservative rewritability of description logic TBoxes, in: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, 2016, pp. 1153–1159. URL: http://www.ijcai.org/Abstract/16/167. [20] A. Kurucz, F. Wolter, M. Zakharyaschev, Definitions and (uniform) interpolants in first-order modal logic, in: 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. [21] A. Kurucz, F. Wolter, M. Zakharyaschev, A non-uniform view of Craig interpolation in modal logics with linear frames, CoRR abs/2312.05929 (2023). URL: https://doi.org/10.48550/arXiv.2312.05929. doi:10.48550/ARXIV.2312.05929. arXiv:2312.05929.