=Paper=
{{Paper
|id=Vol-1577/paper_16
|storemode=property
|title=On the Uniform One-dimensional Fragment
|pdfUrl=https://ceur-ws.org/Vol-1577/paper_16.pdf
|volume=Vol-1577
|authors=Antti Kuusisto
|dblpUrl=https://dblp.org/rec/conf/dlog/Kuusisto16
}}
==On the Uniform One-dimensional Fragment==
https://ceur-ws.org/Vol-1577/paper_16.pdf
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.