On the uniform one-dimensional fragment Antti Kuusisto University of Bremen, Germany, kuusisto@uni-bremen.de Abstract. The uniform one-dimensional fragment of first-order logic, U1 , is a recently introduced formalism that extends two-variable logic in a natural way to contexts with relations of all arities. We survey properties of U1 and investigate its relationship to description logics designed to accommodate higher arity relations, with particular attention given to DLRreg . We also define a description logic version of a variant of U1 and prove a range of new results concerning the expressivity of U1 and related logics. Keywords: two-variable logics, description logics, higher arity relations, uniform one-dimensional fragments 1 Introduction Two-variable logic [10,24] and the guarded fragment [1] are currently perhaps the most widely studied subsystems of first-order logic. Two-variable logic FO2 was proved decidable in [19], and the satisfiability problem of FO2 was shown to be NEXPTIME-complete in [7]. The extension of two-variable logic with count- ing quantifiers, FOC2 , was proved decidable in [8,20] and subsequently shown to be NEXPTIME-complete in [21]. Research on extensions and variants of two- variable logic is currently very active. Recent research has mainly concerned decidability and complexity issues in restriction to particular classes of struc- tures and also questions related to different built-in features and operators that increase the expressivity of the base language. Recent articles in the field include for example [3,4,13,25] and several others. The guarded fragment was shown 2EXPTIME-complete in [6] and in fact EXPTIME-complete over bounded arity vocabularies in the same article. The guarded fragment has since then generated a vast literature. The fragment has recently been significantly generalized in the article [2] which introduces the guarded negation first-order logic GNFO. Intuitively, GNFO only allows nega- tions of formulae that are guarded in the sense of the guarded fragment. The guarded negation fragment has been shown complete for 2NEXPTIME in [2]. The recent article [9] introduced the uniform one-dimensional fragment, U1 , which is a natural generalization of FO2 to contexts with relations of arbitrary arities. Intuitively, U1 is a fragment of first-order logic obtained by restricting quantification to blocks of existential (universal) quantifiers that leave at most one free variable in the resulting formula. Additionally, a uniformity condition applies to the use of atomic formulae: if n, k ≥ 2, then a Boolean combination of 2 atoms R(x1 , ..., xk ) and S(y1 , ..., yn ) is allowed only if the sets {x1 , ..., xk } and {y1 , ..., yn } of variables are equal. Boolean combinations of formulae with at most one free variable can be formed freely, and the use of equality is unrestricted. Several variants of U1 have also been investigated in [9] and the two subsequent papers [11,12]. Perhaps the easiest way to gain intuitive insight on U1 is to consider the fully uniform fragment, FU1 , which is a slight restriction of U1 introduced in the current article. It turns out that FU1 can be represented roughly as the standard polyadic modal logic where novel accessibility relations can be formed by the Boolean combination and permutation of atomic accessibility relations. Recall that polyadic modal logic is the extension of modal logic with formulae χ := hRi(ϕ1 , ..., ϕk ) interpreted such that M, w |= χ iff there exist points u1 , ..., uk such that (w, u1 , ..., uk ) ∈ R and M, ui |= ϕi for each i. It also turns out, as we shall see, that over vocabularies with at most binary relations, FU1 is in fact equi-expressive with FO2 . This result extends a similar observation from [18] concerning Boolean modal logic with the inverse operator and a built-in identity modality. It was proved in [18] that this logic is expressively complete for FO2 . The fact that FU1 collapses to FO2 over binary vocabularies can be taken to indicate that FU1 is a natural and in some sense minimal generalization of FO2 to higher arity contexts. The uniform one-dimensional fragment U1 was shown to have the finite model property and a NEXPTIME-complete decision problem in [11], thereby estab- lishing that the transition from FO2 to U1 comes without a cost in complexity. It was also shown in [11] that U1 is incomparable in expressivity with FOC2 ; we will prove in the current article that U1 is incomparable with GNFO, too. We note, however, that the article [9] already established a similar incomparability result concerning GNFO and the equality-free fragment of U1 . The article [11] also showed that the extension of U1 with counting quantifiers is undecidable. The article [9], in turn, established that relaxing either of the two principal con- straints of the syntax of U1 -formulae—leaving two free variables after quantifica- tion or violating the uniformity condition—leads to undecidability. Building on [9] and [11], the article [12] investigated variants of U1 in the presence of built-in equivalence relations. It was shown, e.g., that while U1 becomes 2NEXPTIME- complete when a built-in equivalence is added, a certain natural restriction of U1 (which still contains FO2 ) remains NEXPTIME-complete. In the current article we briefly discuss the above collection of results on U1 and its variants and list a number of related open problems. Unlike the guarded fragment and GNFO, two-variable logic does not cope well with relations of arities greater than two, and the same applies to FOC2 . In database theory contexts, for example, this can be a major drawback. There- fore the scope of research on two-variable logics is significantly restricted. The uniform one-dimensional fragment U1 extends two-variable logics in a way that leads to the possibility of investigating systems with relations of all arities. Another possible advantage of U1 is its one-dimensionality, i.e., the fact that its formulae are essentially of the type ϕ(x), where x is a free variable. This links 3 U1 to description logics in a natural way, as formulae of U1 can be regarded as concepts in the description logic sense. Below we make use of this issue and define a description logic DLFU1 , which we prove to be expressively equivalent to the fully uniform one-dimensional fragment FU1 . The logic DLFU1 makes explicit the link between FU1 and polyadic modal logic we mentioned above. It can be seen as the canonical extension of the description logic ALBOid [22] to higher arity contexts. While ALBOid is ALC extended with Boolean and inverse operators on roles, an identity role and singleton concepts, DLFU1 is essentially the same system with roles of all arities. The relational inverse operator is generalized to an operator that slightly generalizes the relational permutation operator. It is not difficult to come up with examples where for example ternary roles arise in a natural way. Higher arity roles are indeed natural and have therefore been investigated before in the context of desctiption logics, for example in [5,17,23]. Below we compare DLFU1 and the system DLRreg from [5], which includes, e.g., the union, composition and transitive reflexive closure operators for binary roles as well as operators that enable the creation of binary relations from higher arity roles. We show that DLFU1 and DLRreg are incomparable in expressivity. While this result itself is not at all surprizing, it is still worth proving since the related arguments directly demonstrate the relative expressivities of DLRreg and DLFU1 . We end the article by identifying a fragment of DLRreg which is in a certain sense maximal with the property that it embeds into DLFU1 . In the context of this investigation we discuss the curious fact that while U1 can count, it cannot count well enough to express the number restriction operators of DLRreg . In the investigations below concerning expressivity issues, we make occasional use of the novel Ehrenfeucht-Fraı̈ssé (EF) game for U1 from [12]. The related concrete arguments shed light on the expressivity properties of U1 . Finally, it is worth pointing out here that a rather nice and potentially fruit- ful feature of DLFU1 is that it is based on the syntactically and semantically same approach as standard polyadic modal logic. Thereby DLFU1 extends the celebrated and fruitful link between modal and description logics to higher arity contexts in a way that preserves the close relationship between the two fields. 2 Preliminaries We let VAR denote a countably infinite set of variable symbols. Let X = {x1 , ..., xk } be a finite set of variable symbols and let R be an n-ary relation symbol; R is not allowed to be the identity symbol here. An atomic formula R(xi1 , ..., xin ) is called an X-atom if {xi1 , ..., xin } = X. For example, assuming x, y, z to be distinct variables, both S(x, y) and T (x, x, y, y, x) are {x, y}-atoms while P (x) and R(x, y, z) are not. Let Z+ be theSset of positive integers. We let V denote the infinite relational vocabulary V := k ∈ Z+ τk , where τk is a countably infinite set of k-ary relation symbols; the equality symbol is not in V . A unary V -atom is an atomic formula of the form P (x) or R(x, ..., x), where P, R ∈ V . Here (x, ..., x) denotes the tuple that repeats x exactly n times, n being the arity of R. 4 The set of formulae of the equality-free uniform one-dimensional fragment U1 (wo =) of first-order logic is the smallest set F satisfying the following con- ditions (cf. [9]). 1. Every unary V -atom is in F. Also ⊥, > ∈ F. 2. If ϕ ∈ F, then ¬ϕ ∈ F. 3. If ϕ, ψ ∈ F, then (ϕ ∧ ψ) ∈ F. 4. Let Y := {x0 , ..., xk } ⊆ VAR and X ⊆ Y . Let ϕ be a Boolean combination of X-atoms over V and formulae in F whose free variables (if any) are in Y . Then ∃x1 ...∃xk ϕ ∈ F and ∃x0 ...∃xk ϕ ∈ F. For example ∃y∃z((¬R(x, y, z) ∨ T (z, y, x, x)) ∧ P (z)) is a U1 (wo =)-formula, while ∃y∃z(S(x, y) ∧ S(y, z) ∧ P (z)) is not because {x, y} 6= {y, z}. This latter formula is said to violate the uniformity condition of U1 . The formula ∃yR(x, y, z) is also illegitimate because it violates one-dimensionality, leaving two variables free instead of one. However, the sentence ∃x∃z∃yR(x, y, z) is legitimate, and so is ∀x∃z∃y(R(x, y, z) ∧ ∃u¬U (y, u)), while ∀x∀z∃yR(x, y, z) is not. The fully uniform one-dimensional fragment FU1 is the logic whose formulae are obtained from formulae of U1 (wo =) by allowing the free substitution of any collection of binary relation symbols by the equality symbol =. The uniform one-dimensional fragment U1 is obtained by adding to the above four clauses that define the set F of formulae of U1 (wo =) the additional clause x = y ∈ F. For example ∃y∃z(R(y, z, x) ∧ x 6= y ∧ ∃zS(y, z)) is a formula of U1 but not of FU1 . Clearly FU1 is a fragment of U1 . The following proposition, where FO2 denotes two-variable logic with equality, is easy to prove using disjunctive normal form representations of formulae. Proposition 1. FU1 and FO2 are equi-expressive over models with at most binary relations. That is, in restriction to models with relations of arity at most two, each formula of FU1 with at most two free variables has an equivalent FO2 -formula, and each FO2 -formula has an equivalent FU1 -formula. However, U1 is strictly more expressive than two-variable logic FO2 even over the empty vocabulary, because U1 can count better than FO2 : we observe that for example the sentence ∃x∃y∃z(x 6= y ∧ x 6= z ∧ y 6= z) is a U1 -formula. It is well known and easy to show by a two-pebble-game argument (see [16] for pebble games) that this sentence is not expressible in FO2 . It is easy to see that FO2 and therefore FU1 can define the property that |P | = 1 for a unary predicate P . Thus nominals can be simulated in those logics. The logic U1 can define even the properties |P | ≤ k, |P | ≥ k and |P | = k for any finite k. However, the counting capacity of U1 is restricted in an interesting way, as we will see later on; U1 cannot make counting statements about the in-degrees and out-degrees of binary relations. Finally, the U1 -sentence ∃x∀y∀z(R(y, z) → (x = y ∨ x = z)) provides a perhaps more interesting example of what is definable in U1 but not in FO2 . This sentence states that there is an element that belongs to every edge of R. It is easy to see by a two-pebble-game argument that this property is not 5 expressible in FO2 : the Duplicator wins the two-pebble-game played on K2 and K3 , where Kn is the n-clique. Recall that the n-clique is the structure with n elements where R is the total binary relation with the reflexive loops removed. 3 Complexity of U1 and its variants The complexity of U1 was identified in [11] by showing that the logic has the exponential model property. Theorem 1 ([11]). Every satisfiable U1 -formula ϕ has a model whose size is bounded exponentially in |ϕ|. Theorem 2 ([11]). The satisfiability problem (= finite satisfiability problem) for U1 is NEXPTIME-complete. The argument in [11] leading to the above results bears at least some degree of resemblance to the NEXPTIME upper bound proof of FO2 by Grädel, Kolaitis and Vardi in [7]. It turns out that U1 -formulae can be transferred into equi- satisfiable formulae in a generalized version of the Scott normal form specially designed for U1 , and the exponential model property can then be established by appropriately modifying and extending the arguments applied in [7]. The complexity results of the article [11] were extended in [12]. If L denotes a fragment of first-order logic and R1 , ..., Rk are binary relation symbols, then we let L(R1 , ..., Rk ) denote the language obtained by allowing for the free substi- tution of identity symbols in L-formulae by the special symbols Ri . The article [12] investigated U1 and its variants over models with a built-in equivalence relation ∼. It was shown that the satisfiability (SAT) and finite satisfiability (FINSAT) problems for U1 (∼) are 2NEXPTIME-complete. The article [12] also identified a natural restriction SU1 of U1 that still extends FO2 and showed that the SAT and FINSAT problems for SU1 (∼) are only NEXPTIME-complete; see [12] for the formal definition of SU1 . Furthermore, the article [12] established that the SAT and FINSAT-problems of SU1 (∼1 , ∼2 ), i.e., SU1 with two built-in equivalences, is undecidable. This contrasts with the case for FO2 which remains decidable with two equivalences (SAT [14] and FINSAT [15]). Several immediately interesting open problems remain, for example the de- cidability issue for U1 (≤), where ≤ denotes a built-in linear order. Also, while U1 (tr ) (i.e., U1 with a built-in transitive relation tr ) was shown undecidable in [12], it was left open whether U1 (tr (uniform)) is decidable; here U1 (tr (uniform)) denotes the language obtained from U1 by allowing the free substitution of any instances of a binary relation (rather than the equality symbol) by the built-in transitive relation tr . . 4 Expressivity issues In this section we provide an overview on the expressivity of U1 and its variants. The following theorem from [11] relates the expressivities of U1 and FOC2 . 6 Theorem 3 ([11]). U1 and FOC2 are incomparable in expressivity. Proof. It is easy to show that the U1 -sentence ∃x∃y∃zR(x, y, z) cannot be ex- pressed in FOC2 , and therefore U1 6≤ FOC2 . To prove that FOC2 6≤ U1 , let S be a binary relation symbol. We will show that U1 cannot express the FOC2 - definable condition that the in-degree (with respect to the relation S) at every node is at most one. Assume ϕ(S) is a U1 -formula that defines the property. Consider the formula ϕ(S) ∧ ∀x∃yS(x, y) ∧ ∃x∀y¬S(y, x). It is clear that this formula has only infinite models, and thereby the assumption that U1 can ex- press ϕ(S) is false by the finite model property of U1 (Theorem 1). t u We next consider U1 over vocabularies with at most binary relations. Theorem 4 ([11]). Consider models over a relational vocabulary τ with the arity bound two. Suppose that τ indeed contains at least one binary relation symbol. Then FO2 < U1 < FOC2 . Proof. We already discussed the strict inclusion FO2 < U1 above in the prelim- inaries section. A lengthy proof of the inclusion U1 ≤ FOC2 is given in [11]. The strictness of this inclusion follows from the proof of Theorem 3 where we showed that U1 cannot express that the in-degree of a binary relation is at most one. tu We then compare the expressivities of U1 and the guarded negation fragment GNFO [2]. The first non-inclusion (U1 6≤ GNFO) of the following theorem has been proved in [9], where only the equality-free fragment of U1 was investigated. The second non-inclusion (GNFO 6≤ U1 ) is new. Theorem 5. U1 and GNFO are incomparable in expressivity.   Proof. Define the two structures {a}, {(a, a)} and {a, b}, {(a, a), (b, b)} . It is straightforward to establish by using the bisimulation for GNFO, provided in [2], that these two structures are bisimilar in the sense of GNFO. Thus the U1 -sentence ∃x∃y ¬R(x, y) is not expressible in GNFO. Hence U1 6≤ GNFO. Consider then the GNFO-sentence ϕ := ∃x∃y∃z(Rxy ∧ Ryz ∧ Rzx). Let A denote the model consisting of four disjoint copies of the directed cycle with three elements. Let B be the model with three disjoint copies of the directed cycle with four elements. It follows rather directly from the Ehrenfeucht-Fraı̈ssé game for U1 (which is defined in [12]) that A and B satisfy the same U1 -sentences. For the game-based argument to work, it is essential that the two models A and B have the same cardinality, because bijections between subsets of the domains of A and B are used in the game. (See [12] for a detailed discussion of the game.) With A and B defined in this way, the rest of the game-based argument is straightforward. We can therefore now conclude that U1 cannot express the GNFO-sentence ϕ we fixed above, and hence GNFO 6≤ U1 . tu Before we close the current section, we observe that all the above results concerning expressivity hold even if attention is limited to finite models only. The same proofs apply without modification, as the reader can check. This is especially interesting in the case of Theorem 3, whose proof makes use of the finite model property of U1 . 7 5 Undecidability of U1 with counting quantifiers Since FOC2 and U1 are both NEXPTIME-complete, it is natural to ask whether the extension of U1 by counting quantifiers (UC1 ) remains decidable. Formally, UC1 is obtained from U1 by allowing the free substitution of quantifiers ∃ by quantifiers ∃≥k , ∃≤k , ∃=k . While the transition from FO2 to FOC2 preserves NEXPTIME-completeness, the analogous step from U1 to UC1 crosses the undecidability barrier. Theorem 6 ([11]). The satisfiability and finite satisfiability problems of UC1 are Π10 -complete and Σ10 -complete, respectively. Thereby UC1 has the same complexity as full first-order logic. It is an inter- esting open problem to identify natural logics that extend FOC2 into higher arity contexts in a way that preserves decidability. Possible research directions here could involve for example investigating restrictions of UC1 based on somewhat more limited ways of using the quantifiers ∃≥k , ∃≤k , ∃=k . 6 U1 and description logics In this section we define a novel logic DLFU1 which is a description logic version of FU1 and compare it to DLRreg [5], which is a well-known description logic that accommodates higher arity relations. We first generalize the relational inverse operation to contexts with higher ar- ity relations. When n is a positive integer, we let [n] denote the set {1, ..., n}. We let SRJ denote the set of all surjections σ : [k] → [m], such that 2 ≤ m ≤ k. When m = k, then σ is a permutation; permutations are natural generalizations of the relational inverse operator into higher arity contexts, and surjections generalize permutations an inch further. When we use SRJ in constructing the syntax of DLFU1 below, we assume each function σ ∈ SRJ to be a suitable string listing the ordered pairs (n, k) such that σ(n) = k in binary. The set R of roles of DLFU1 is defined by the grammar R ::= R | ε | ¬R | (R1 ∩ R2 ) | σR where R denotes an atomic role, ε the binary identity role and σ ∈ SRJ. Here R can have any arity greater or equal to two, and the arity of ε is two. The intersection of relations of different arity will produce the empty relation, so we may as well allow such terms. (We fix the arity of the empty relation in such cases to be two.) The set of concepts of DLFU1 is given by the grammar C ::= A | ¬C | (C1 u C2 ) | ∃R.(C1 , ..., Cn ) where A is an atomic concept and the arity of the relation term R is n + 1. An interpretation I is a pair (∆, ·I ), where ∆ is a nonempty set and ·I a function such that RI ⊆ ∆k and AI ⊆ ∆ for atomic roles R and atomic concepts A; here k is the arity of R. The operators of DLFU1 are defined as follows. 8 1. εI := { (u, u) | u ∈ ∆ }, (¬R)I := ∆n+1 \ RI and (R1 ∩ R2 )I := RI1 ∩ RI2 . 2. (σR)I := {(u1 , ..., um ) | (uσ(1) , ..., uσ(n+1) ) ∈ RI }. Here σ maps [n + 1] onto [m]. The arity of (σR)I is of course m. 3. (¬C)I := ∆ \ C I and (C u D)I := C I ∩ DI . 4. ( ∃R.(C1 , ..., Cn ) )I = { u ∈ ∆ | there is a tuple (u, v1 , ..., vn ) ∈ RI such that vi ∈ CiI for each i } In the pathological case where σ : [n] → [m] acts on a relation R whose arity is not equal to n, the empty binary relation is produced. We need the surjection operators (rather than simply permutations) in order to express in DLFU1 con- ditions such as the one given by the FU1 -formula ∃y(R(x, y) ∧ S(x, y, x) ∧ P (y)). In the following theorem, equivalence means equivalence in the standard sense in which formulae of modal and predicate logic are compared. Theorem 7. DLFU1 and FU1 are equi-expressive: each FU1 -formula ϕ(x) has an equivalent DLFU1 -concept, and vice versa. Proof. We only provide a rough sketch the proof. The most involved issue here is the translation of FU1 -formulae of the type ∃x1 ...∃xk ϕ into DLFU1 , where ϕ is a Boolean combination of higher arity atoms and at most unary FU1 -formulae. Here we put ϕ into disjunctive normal form and distribute the quantifier prefix over the disjunctions in order to obtain a disjunction of formulae of the type  ∃x1 ...∃xk (T (y1 , ..., yn ) ∧ χ1 (u1 ) ∧ ... ∧ χm (um ) , where {y1 , ..., yn } ⊆ {x0 , x1 , ..., xk }, {u1 , ..., um } ⊆ {x0 , x1 , ..., xk }, and where the term T (y1 , ..., yn ) is a conjunction of higher arity literals (atoms and negated atoms) such that each literal has exactly the same set {y1 , ..., yn } of variables. Such formulae can easily be translated into DLFU1 , assuming inductively that we already know how to translate the unary FU1 -formulae χi (ui ). t u We then define the description logic DLRreg from [5] and compare it to DLFU1 . DLRreg is defined by the grammar R ::= >n | R | ($i/n : C) | ¬R | (R1 ∩ R2 ) E ::= ε | R|$i,$j | (E1 ◦ E2 ) | (E1 ∪ E2 ) | E ∗ C ::= >1 | A | ¬C | (C1 u C2 ) | ∃E.C | ∃[$i]R | (≤ k [$i]R) where R is an atomic role and A an atomic concept from a finite set V of atomic role and concept symbols. The indices i and j denote integers between 1 and nmax (where nmax is the maximum arity of the symbols in V), n denotes an integer between 2 and nmax and k denotes a non-negative integer. All these numbers are encoded in binary. An interpretation I = (∆, ·I ) for DLRreg over V is any structure such that the following conditions are met (cf. [5]). 1. For each atomic concept A ∈ V and atomic role R ∈ V, we have A ⊆ ∆ and R ⊆ ∆n , where n is the arity of R. 9 2. For each n > 1, (>n )I is a subset of ∆n that covers the relations of arity n. 3. ($i/n : C)I is the set of tuples (u1 , ..., un ) ∈ (>n )I such that ui ∈ C I . 4. (¬R)I = (>n )I \ RI when R is an n-ary term and (R1 ∩ R2 )I = RI1 ∩ RI2 . 5. εI = { (u, u) | u ∈ ∆ } and (R|$i,$j )I is the relation { (u, v) | u = wi and v = wj for some tuple (w1 , ..., wn ) ∈ RI }. 6. The operators ◦, ∪ and ·∗ in the terms (E1 ◦ E2 ), (E1 ∪ E2 ) and E ∗ are interpreted in the usual way, i.e., ◦ is the relational composition operator, ∪ the union and ·∗ the transivitive reflexive closure operator. 7. (>1 )I = ∆, (¬C)I = (>1 )I \ C I and (C u D)I = C I ∩ DI . 8. (∃E.C)I = { u | exists (u, v) ∈ E I such that v ∈ C I } 9. (∃[$i]R)I = { u | exists (v1 , ..., vn ) ∈ RI such that u = vi } 10. (≤ k [$i]R)I = { u | |{ u | exists (v1 , ..., vn ) ∈ RI such that u = vi }| ≤ k }. DLRreg interpretations are associated with the atomic built-in relations >n . When comparing the expressivity of DLRreg with DLFU1 below, we consider interpretations I where the relations >n are appropriate atomic built-in roles and thus directly available also in DLFU1 . Proposition 2. DLRreg and DLFU1 are incomparable in expressvity. Proof. It is easy to see that DLRreg is closed under disjoint copies such that if C I = U for some DLRreg -concept C, then C I1 +I2 = U1 ∪ U2 , where I1 + I2 consists of two disjoint copies of I and obviously U1 and U2 are the related copies of U . Because of the free use of role negation in DLFU1 , the same does not hold in that logic. For example the DLFU1 -concept ¬∃(¬R).A, where R is a binary role, is satisfied in an interpretation consisting of a single element u that satisfies A and connects to itself via R. This interpretation together with a disjoint copy of itself does not satisfy ¬∃(¬R).A. Thus DLFU1 is not contained in DLRreg . For the converse, it suffices to observe that DLFU1 cannot define the concept ∃(R∗ ).A. It is well known that this property is not first-order expressible, and thus it is not definable in DLFU1 . t u We finish up the current section by identifying a maximal fragment of DLRreg that embeds into DLFU1 . What exactly we mean by maximality in this context will become clear below. Let DLR0reg denote the fragment of DLRreg without Kleene star and count- ing, i.e., DLR0reg is obtained by the grammar that drops the terms E ∗ and (≤ k [$i]R) from the grammar of DLRreg . For each positive integer k, we let DLR0reg [≤ k] denote the system we obtain if we add the terms (≤ k [$i]R) (with each arity for R and each related i included) to the grammar of DLR0reg . (Note that (≤ 0 [$i]R) is equivalent to ¬∃[$i]R.) Similarly, we let DLR0reg [∗] be the logic we obtain by adding the term E ∗ to the grammar of DLR0reg . We will show that while DLR0reg embeds into DLFU1 (Theorem 8), neither DLR0reg [∗] nor any of the logics DLR0reg [≤ k] does (Theorem 9). We already observed above that the operator ·∗ of DLRreg is inexpressible in DLFU1 . The 10 fact that the number restriction operators (≤ k [$i]R) are definable neither in DLFU1 nor in U1 , as we shall prove, is somewhat more surprising since U1 can do some counting. However, as we already discussed earlier, the counting ability of U1 is limited. Finally, it is not entirely trivial that we can indeed keep the composition operator in DLR0reg and still embed this logic into DLFU1 . This is because the use of the composition operator often requires the three-variable fragment of first-order logic, and DLFU1 collapses to FO2 on binary vocabularies. Theorem 8. DLR0reg embeds into DLFU1 . Proof. We begin by showing that we can eliminate the composition operator ◦ from DLR0reg altogether. Consider a concept D of DLR0reg . We first observe that we can use the the standard identity R ◦ (S ∪ T ) = (R ◦ S) ∪ (R ◦ T ) of relation algebra to obtain from D an expression where the composition operators are on the “atomic” level, with the relational terms ε and R|$i,$j of the grammar  of DLRreg regarded as atoms. We then use the equivalence ∃ E1 ∪ ... ∪ Em . C ≡ (∃E1 .C) t ... t (∃Em .C) to obtain a disjunction of formulae ∃Ei .C where Ei is a composition of “atomic” terms S. To eliminate the composition operators from the terms Ei = S1 ◦ ... ◦ Sn , we use the equivalence ∃ S1 ◦ ... ◦ Sn ).C ≡ ∃S1 .∃S2 .∃S3 ... ∃Sn .C. Thus we can eliminate instances of ◦ from DLR0reg . Next we note that all the remaining  union operators are also eliminable, using the equivalence ∃ E1 ∪ ... ∪ Em . C ≡ (∃E1 .C) t ... t (∃Em .C) We then show how to translate the obtained formula (which is free of union and composition operators) into DLFU1 . For presentational reasons, we will translate the formula into the first-order fragment FU1 . The syntax of DLR0reg without composition and union is given by the grammar R ::= >n | R | ($i/n : C) | ¬R | (R1 ∩ R2 ) E ::= ε | R|$i,$j C ::= >1 | A | ¬C | (C1 u C2 ) | ∃E.C | ∃[$i]R where R|$i,$j with i = j is not allowed; these are easy to eliminate. Our trans- lation will be defined with three translation operators s, t, T that correspond to, respectively, the terms for R, E, C above. Each of these operators is parameter- ized by an appropriate tuple of variables. We first define T as follows. 1. T [x](>1 ) := > and T [x](A) := A(x). 2. T [x](¬C) := ¬T [x](C) and T [x](C1 uC2 ) := T [x](C1 ) ∧ T [x](C2 ). 3. T [x](∃E.C) := ∃y t[x, y]( E ) ∧ T [y]C , where t is the translation for terms E to be defined below.  4. T [x](∃[$i]R) := ∃x1 ...∃xi−1 ∃xi+1 ...∃xn s[x1 , ..., xi−1 , x, xi+1 , ..., xn ](R) , where s is a translation for R and n is the arity of R. We then define the operator t. 1. t[x, y](ε) := x = y. 11 2. t[x, y](R|$i,$j ) := ∃z s[u](R)), where ∃z quantifies existentially each of the variables x1 , ..., xn except for xi and xj , and where u is obtained from the tuple (x1 , ..., xn ) by replacing xi by x and xj by y. Here n is the arity of the relation R and s is the translation for R. We finally define the operator s as follows. 1. s[x1 , ..., xn ](>n ) := >n (x1 , ..., xn ) and s[x1 , ..., xn ](R) := R(x1 , ..., xn ) for atomic roles R and the built-in relation >n . 2. s[x1 , ..., xn ]( ($i/n : C) ) := T [xi ](C) ∧ >n (x1 , ..., xn ), where T is the trans- lation for C. 3. s[x1 , ..., xn ](¬R) := >n (x1 , ..., xn ) ∧ ¬ s[x1 , ..., xn ](R). 4. s[x1 , ..., xn ]( R1 ∩ R2 ) := s[x1 , ..., xn ](R1 ) ∧ s[x1 , ..., xn ](R2 ). The translated formula is now easily modified to a formula of FU1 . This involves shifting the quantifiers introduced in clause 2 of the translation t[x, y]. t u We then show that none of the operators of DLRreg missing from DLR0reg could be added to DLR0reg without losing the embedding into DLFU1 . By an operator we here mean ·∗ and each term (≤ k [$i]R) with k ∈ Z+ . Note that for a fixed k, the term (≤ k [$i]R) strictly speaking denotes a collection of operators, because we could vary i and the arity of R. Thus a more fine-grained analysis than the one below could be given. We ignore this issue for the sake of simplicity. Theorem 9. DLR0reg [∗] and DLR0reg [≤ k] for each k ∈ Z+ are all incomparable with DLFU1 Proof. We already observed in the proof of Proposition 2 that DLFU1 cannot define the concept ∃(R∗ ).A and that DLRreg cannot define ¬∃(¬R).A, where ¬ is the full negation of DLFU1 . Thus it now suffices to show that for each k ∈ Z+ , the concept (≤ k [$2]R) is not expressible in DLFU1 . Here R is a binary relation. In the proof of Theorem 3, we already dealt with the special case where k = 1: if ϕ(x) was an FU1 -formula defining the concept (≤ 1 [$2]R), then the FU1 -sentence ∀xϕ(x) would define that the in-degree of R is at most one. Thus we can now fix a k ≥ 2 and define two interpretations, one consisting of k + 1 copies of the clique of size k and the other one of k copies of the clique of size k + 1. (Recall that a clique is a structure where the binary relation R is the total relation with the reflexive loops removed). We have prepared the setting in such a way that it is now easy to show, using once again the EF-game for U1 (defined in [12]), that the two structures satisfy exactly the same U1 -sentences. However, the concept (≤ k − 1 [$2]R) is satisfied by every element in the first structure and by none of the elements of the second one. Thus no U1 -formula is equivalent to (≤ k − 1 [$2]R), because if ϕ(x) was equivalent to (≤ k − 1 [$2]R), the U1 -sentence ∃xϕ(x) would be satisfied by the first structure but not the second one. t u Acknowledgements This work was supported by the ERC grant 647289 “CODA.” 12 References 1. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded frag- ments of predicate logic. Journal of Philosophical Logic, 27(3):217–274, 1998. 2. V. Bárány, B. ten Cate, and L. Segoufin. Guarded negation. In Proc. of ICALP (2), pages 356–367, 2011. 3. S. Benaim, M. Benedikt, W. Charatonik, E. Kieroński, R. Lenhardt, F. Mazowiecki, and J. Worrell. Complexity of two-variable logic on finite trees. In Proc. of ICALP (2), pages 74–88, 2013. 4. M. Bojańczyk, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. Journal of the ACM, 56(3), 2009. 5. D. Calvanese, G. De Giacomo, and M. Lenzerini. On the decidability of query containment under constraints. In Proc. of PODS, pages 149–158, 1998. 6. E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, 64(4):1719–1742, 1999. 7. E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53–69, 1997. 8. E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In Proc. of LICS, pages 306–317, 1997. 9. L. Hella and A. Kuusisto. One-dimensional fragment of first-order logic. In Proc. of AiML, pages 274–293, 2014. 10. L. Henkin. Logical systems containing only a finite number of symbols. Presses De l’Université De Montréal, 1967. 11. E. Kieroński and A. Kuusisto. Complexity and expressivity of uniform one- dimensional fragment with equality. In Proc. of MFCS (1), pages 365–376, 2014. 12. E. Kieroński and A. Kuusisto. Uniform one-dimensional fragments with one equiv- alence relation. In Proc. of CSL, pages 597–615, 2015. 13. E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing, 43(3), 2014. 14. E. Kieroński and M. Otto. Small substructures and decidability issues for first- order logic with two variables. Journal of Symbolic Logic, 77(3):729–765, 2012. 15. E. Kieroński and L. Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In Proc. of LICS, pages 123–132, 2009. 16. L. Libkin. Elements of Finite Model Theory. Springer, 2004. 17. C. Lutz, U. Sattler, and S. Tobies. A suggestion for an n-ary description logic. In Proc. of DL’99, 1999. 18. C. Lutz, U. Sattler, and F. Wolter. Modal logic and the two-variable fragment. In Proc. of CSL, pages 247–261, 2001. 19. M. Mortimer. On languages with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21(1):135–140, 1975. 20. L. Pacholski, W. Szwast, and L. Tendera. Complexity of two-variable logic with counting. In Proc. of LICS, pages 318–327, 1997. 21. I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quan- tifiers. Journal of Logic, Language and Information, 14(3):369–395, 2005. 22. R. A. Schmidt and D. Tishkovsky. Using tableau to decide description logics with full role negation and identity. ACM Transactions on Computational Logic, 15(1), 2014. 23. J. G. Schmolze. Terminological knowledge representation systems supporting n-ary terms. In Proc. of KR’89, pages 432–443, 1989. 13 24. D. Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27, 1962. 25. W. Szwast and L. Tendera. FO2 with one transitive relation is decidable. In Proc. of STACS, pages 317–328, 2013.