On the uniform one-dimensional fragment

Abstract

The uniform one-dimensional fragment of rst-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 de ne 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

Introduction

Two-variable logic [ 10,24 ] and the guarded fragment [ 1 ] are currently perhaps the most widely studied subsystems of rst-order logic. Two-variable logic FO2 was proved decidable in [ 19 ], and the satis ability problem of FO2 was shown to be NEXPTIME-complete in [ 7 ]. The extension of two-variable logic with counting quanti ers, FOC2, was proved decidable in [ 8,20 ] and subsequently shown to be NEXPTIME-complete in [ 21 ]. Research on extensions and variants of twovariable logic is currently very active. Recent research has mainly concerned decidability and complexity issues in restriction to particular classes of structures and also questions related to di erent built-in features and operators that increase the expressivity of the base language. Recent articles in the eld 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 signi cantly generalized in the article [ 2 ] which introduces the guarded negation rst-order logic GNFO. Intuitively, GNFO only allows negations 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 rst-order logic obtained by restricting quanti cation to blocks of existential (universal) quanti ers 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 atoms R(x1; :::; xk) and S(y1; :::; yn) is allowed only if the sets fx1; :::; xkg and fy1; :::; yng 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 j= i there exist points u1; :::; uk such that (w; u1; :::; uk) 2 R and M; ui j= '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 nite model property and a NEXPTIME-complete decision problem in [ 11 ], thereby establishing 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 quanti ers is undecidable. The article [ 9 ], in turn, established that relaxing either of the two principal constraints of the syntax of U1-formulae|leaving two free variables after quanti cation 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 2NEXPTIMEcomplete 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 brie y 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. Therefore the scope of research on two-variable logics is signi cantly 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 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 de ne 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 di cult 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 re exive 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-Frasse (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 fruitful 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 elds. 2

Preliminaries

We let VAR denote a countably in nite set of variable symbols. Let X = fx1; :::; xkg be a nite 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 fxi1 ; :::; xin g = X. For example, assuming x; y; z to be distinct variables, both S(x; y) and T (x; x; y; y; x) are fx; yg-atoms while P (x) and R(x; y; z) are not.

Let Z+ be the set of positive integers. We let V denote the in nite relational vocabulary V := Sk 2 Z+ k, where k is a countably in nite 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 2 V . Here (x; :::; x) denotes the tuple that repeats x exactly n times, n being the arity of R.

The set of formulae of the equality-free uniform one-dimensional fragment U1(wo =) of rst-order logic is the smallest set F satisfying the following conditions (cf. [ 9 ]). 1. Every unary V -atom is in F . Also ?; > 2 F . 2. If ' 2 F , then :' 2 F . 3. If '; 2 F , then (' ^ ) 2 F . 4. Let Y := fx0; :::; xkg 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 9x1:::9xk ' 2 F and 9x0:::9xk ' 2 F .

For example 9y9z((:R(x; y; z) _ T (z; y; x; x)) ^ P (z)) is a U1(wo =)-formula, while 9y9z(S(x; y) ^ S(y; z) ^ P (z)) is not because fx; yg 6= fy; zg. This latter formula is said to violate the uniformity condition of U1. The formula 9yR(x; y; z) is also illegitimate because it violates one-dimensionality, leaving two variables free instead of one. However, the sentence 9x9z9yR(x; y; z) is legitimate, and so is 8x9z9y(R(x; y; z) ^ 9u:U (y; u)), while 8x8z9yR(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 de ne the set F of formulae of U1(wo =) the additional clause x = y 2 F .

For example 9y9z(R(y; z; x) ^ x 6= y ^ 9zS(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 9x9y9z(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 de ne the property that jP j = 1 for a unary predicate P . Thus nominals can be simulated in those logics. The logic U1 can de ne even the properties jP j k, jP j k and jP j = k for any nite 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 9x8y8z(R(y; z) ! (x = y _ x = z)) provides a perhaps more interesting example of what is de nable 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 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 re exive loops removed. 3

Complexity of U1 and its variants

The complexity of U1 was identi ed in [ 11 ] by showing that the logic has the exponential model property.

Theorem 1 ([ 11 ]). Every satis able U1-formula ' has a model whose size is bounded exponentially in j'j.

Theorem 2 ([ 11 ]). The satis ability problem (= nite satis ability 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 Gradel, Kolaitis and Vardi in [ 7 ]. It turns out that U1-formulae can be transferred into equisatis able 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 rst-order logic and R1; :::; Rk are binary relation symbols, then we let L(R1; :::; Rk) denote the language obtained by allowing for the free substitution 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 satis ability (SAT) and nite satis ability (FINSAT) problems for U1( ) are 2NEXPTIME-complete. The article [ 12 ] also identi ed 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 de nition 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 decidability 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. Theorem 3 ([ 11 ]). U1 and FOC2 are incomparable in expressivity. Proof. It is easy to show that the U1-sentence 9x9y9zR(x; y; z) cannot be expressed 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 FOC2de nable 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 de nes the property. Consider the formula '(S) ^ 8x9yS(x; y) ^ 9x8y:S(y; x): It is clear that this formula has only in nite models, and thereby the assumption that U1 can express '(S) is false by the nite model property of U1 (Theorem 1). tu

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 preliminaries 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 rst 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. De ne the two structures fag; f(a; a)g and fa; bg; f(a; a); (b; b)g . 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 9x9y :R(x; y) is not expressible in GNFO. Hence U1 6 GNFO.

Consider then the GNFO-sentence ' := 9x9y9z(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-Frasse game for U1 (which is de ned 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 de ned 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 xed 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 nite models only. The same proofs apply without modi cation, as the reader can check. This is especially interesting in the case of Theorem 3, whose proof makes use of the nite model property of U1.

Undecidability of U1 with counting quanti ers

Since FOC2 and U1 are both NEXPTIME-complete, it is natural to ask whether the extension of U1 by counting quanti ers (UC1) remains decidable. Formally, UC1 is obtained from U1 by allowing the free substitution of quanti ers 9 by quanti ers 9 k; 9 k; 9=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 satis ability and nite satis ability problems of UC1 are 10-complete and 10-complete, respectively.

Thereby UC1 has the same complexity as full rst-order logic. It is an interesting 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 quanti ers 9 k; 9 k; 9=k. 6

U1 and description logics

In this section we de ne 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 rst generalize the relational inverse operation to contexts with higher arity relations. When n is a positive integer, we let [n] denote the set f1; :::; ng. 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 2 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 de ned by the grammar

R ::= R j " j :R j (R1 \ R2) j R where R denotes an atomic role, " the binary identity role and 2 SRJ. Here R can have any arity greater or equal to two, and the arity of " is two. The intersection of relations of di erent arity will produce the empty relation, so we may as well allow such terms. (We x 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 j :C j (C1 u C2) j 9R:(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 de ned as follows. 1. "I := f (u; u) j u 2 g, (:R)I := n+1 n RI and (R1 \ R2)I := R1I \ R2I. 2. ( R)I := f(u1; :::; um) j (u (1); :::; u (n+1)) 2 RIg. Here maps [n + 1] onto [m]. The arity of ( R)I is of course m. 3. (:C)I := n CI and (C u D)I := CI \ DI. 4. ( 9R:(C1; :::; Cn) )I =

f u 2 j there is a tuple (u; v1; :::; vn) 2 RI such that vi 2 CiI for each i g 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 conditions such as the one given by the FU1-formula 9y(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 9x1:::9xk' 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 quanti er pre x over the disjunctions in order to obtain a disjunction of formulae of the type 9x1:::9xk(T (y1; :::; yn) ^ 1(u1) ^ ::: ^ m(um) ; where fy1; :::; yng fx0; x1; :::; xkg, fu1; :::; umg fx0; x1; :::; xkg, 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 fy1; :::; yng 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). tu

We then de ne the description logic DLRreg from [ 5 ] and compare it to DLFU1 . DLRreg is de ned by the grammar

R ::= >n j R j ($i=n : C) j :R j (R1 \ R2) E ::= " j Rj$i;$j j (E1 E2) j (E1 [ E2) j E

C ::= >1 j A j :C j (C1 u C2) j 9E:C j 9[$i]R j ( k [$i]R) where R is an atomic role and A an atomic concept from a nite 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 2 V and atomic role R 2 V, we have A R n, where n is the arity of R. and 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) 2 (>n)I such that ui 2 CI . 4. (:R)I = (>n)I n RI when R is an n-ary term and (R1 \ R2)I = R1I \ R2I . 5. "I = f (u; u) j u 2 g and (Rj$i;$j )I is the relation

f (u; v) j u = wi and v = wj for some tuple (w1; :::; wn) 2 RI g: 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 re exive closure operator. 7. (>1)I = , (:C)I = (>1)I n CI and (C u D)I = CI \ DI . 8. (9E :C)I = f u j exists (u; v) 2 E I such that v 2 CI g 9. (9[$i]R)I = f u j exists (v1; :::; vn) 2 RI such that u = vig 10. ( k [$i]R)I = f u j jf u j exists (v1; :::; vn) 2 RI such that u = vigj k g.

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 CI = U for some DLRreg -concept C, then CI1+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 :9(:R):A, where R is a binary role, is satis ed in an interpretation consisting of a single element u that satis es A and connects to itself via R. This interpretation together with a disjoint copy of itself does not satisfy :9(:R):A. Thus DLFU1 is not contained in DLRreg .

For the converse, it su ces to observe that DLFU1 cannot de ne the concept 9(R ):A. It is well known that this property is not rst-order expressible, and thus it is not de nable in DLFU1 . tu

We nish 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.

0

Let DLRreg denote the fragment of DLRreg without Kleene star and counting, i.e., DLRr0eg 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 DLRr0eg [ 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 DLRr0eg . (Note that ( 0 [$i]R) is equivalent to :9[$i]R.) Similarly, we let DLRr0eg [ ] be the logic we obtain by adding the term E to the grammar of DLRr0eg .

0

We will show that while DLRreg embeds into DLFU1 (Theorem 8), neither DLRr0eg [ ] nor any of the logics DLRr0eg [ k] does (Theorem 9). We already observed above that the operator of DLRreg is inexpressible in DLFU1 . The fact that the number restriction operators ( k [$i]R) are de nable 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 0 operator in DLRreg and still embed this logic into DLFU1 . This is because the use of the composition operator often requires the three-variable fragment of rst-order logic, and DLFU1 collapses to FO2 on binary vocabularies.

0 Theorem 8. DLRreg embeds into DLFU1 .

Proof. We begin by showing that we can eliminate the composition operator from DLRreg altogether. Consider a concept D of DLRr0eg . We rst observe that 0 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 Rj$i;$j of the grammar of DLRreg regarded as atoms. We then use the equivalence 9 E1 [ ::: [ Em : C (9E1:C) t ::: t (9Em:C) to obtain a disjunction of formulae 9Ei: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 9 S1 ::: Sn ):C 9S1:9S2:9S3 ::: 9Sn:C: Thus we can eliminate instances of from DLRr0eg .

Next we note that all the remaining union operators are also eliminable, using the equivalence 9 E1 [ ::: [ Em : C (9E1:C) t ::: t (9Em: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 rst-order fragment FU1. The syntax of DLRr0eg without composition and union is given by the grammar

R ::=

>n j R j ($i=n : C) j :R j (R1 \ R2) E ::= " j Rj$i;$j C ::=

>1 j A j :C j (C1 u C2) j 9E :C j 9[$i]R where Rj$i;$j with i = j is not allowed; these are easy to eliminate. Our translation will be de ned with three translation operators s; t; T that correspond to, respectively, the terms for R; E ; C above. Each of these operators is parameterized by an appropriate tuple of variables. We rst de ne T as follows. 1. T [x](>1) := > and T [x](A) := A(x). 2. T [x](:C) := :T [x](C) and T [x](C1 u C2) := T [x](C1) ^ T [x](C2). 3. T [x](9E :C) := 9y t[x; y]( E ) ^ T [y]C , where t is the translation for terms

E to be de ned below. 4. T [x](9[$i]R) := 9x1:::9xi 19xi+1:::9xn 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 de ne the operator t. 1. t[x; y](") := x = y. 2. t[x; y](Rj$i;$j) := 9z s[u](R)), where 9z quanti es 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 nally de ne 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 translation 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 modi ed to a formula of FU1. This involves shifting the quanti ers introduced in clause 2 of the translation t[x; y]. 0 We then show that none of the operators of DLRreg missing from DLRreg 0 could be added to DLRreg without losing the embedding into DLFU1 . By an operator we here mean and each term ( k [$i]R) with k 2 Z+. Note that for a xed 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 ne-grained analysis than the one below could be given. We ignore this issue for the sake of simplicity. with DLFU1 Theorem 9. DLRr0eg [ ] and DLRr0eg [ k] for each k 2 Z+ are all incomparable Proof. We already observed in the proof of Proposition 2 that DLFU1 cannot de ne the concept 9(R ):A and that DLRreg cannot de ne :9(:R):A, where : is the full negation of DLFU1 . Thus it now su ces to show that for each k 2 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 de ning the concept ( 1 [$2]R), then the FU1-sentence 8x'(x) would de ne that the in-degree of R is at most one. Thus we can now x a k 2 and de ne 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 re exive 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 (de ned in [ 12 ]), that the two structures satisfy exactly the same U1-sentences. However, the concept ( k 1 [$2]R) is satis ed by every element in the rst 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 9x'(x) would be satis ed by the rst structure but not the second one. tu Acknowledgements This work was supported by the ERC grant 647289 \CODA."

References

1. H. Andreka , J. van Benthem , and I. Nemeti. Modal languages and bounded fragments of predicate logic . Journal of Philosophical Logic , 27 ( 3 ): 217 { 274 , 1998 .

2. V. Barany , B. ten Cate , and L. Segou n. Guarded negation . In Proc. of ICALP (2) , pages 356 { 367 , 2011 .

3. S. Benaim , M. Benedikt , W. Charatonik , E. Kieronski, R. Lenhardt , F. Mazowiecki , and J. Worrell . Complexity of two-variable logic on nite trees . In Proc. of ICALP (2) , pages 74 { 88 , 2013 .

4. M. Bojanczyk , A. Muscholl , T. Schwentick , and L. Segou n. 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. Gra del. On the restraining power of guards . Journal of Symbolic Logic , 64 ( 4 ): 1719 { 1742 , 1999 .

7. E. Gradel, P. Kolaitis , and M. Vardi . On the decision problem for two-variable rst-order logic . Bulletin of Symbolic Logic , 3 ( 1 ): 53 { 69 , 1997 .

8. E. Gradel, 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 rst-order logic . In Proc. of AiML , pages 274 { 293 , 2014 .

10. L. Henkin . Logical systems containing only a nite number of symbols . Presses De l'Universite De Montreal , 1967 .

11. E. Kieronski and A. Kuusisto . Complexity and expressivity of uniform onedimensional fragment with equality . In Proc. of MFCS (1) , pages 365 { 376 , 2014 .

12. E. Kieronski and A. Kuusisto . Uniform one-dimensional fragments with one equivalence relation . In Proc. of CSL , pages 597 { 615 , 2015 .

13. E. Kieronski, J. Michaliszyn , I. Pratt-Hartmann , and L. Tendera . Two-variable rst-order logic with equivalence closure . SIAM Journal on Computing , 43 ( 3 ), 2014 .

14. E. Kieronski and M. Otto . Small substructures and decidability issues for rstorder logic with two variables . Journal of Symbolic Logic , 77 ( 3 ): 729 { 765 , 2012 .

15. E. Kieronski and L. Tendera . On nite satis ability of two-variable rst-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 fur 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 quanti ers . 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 .

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 .