Information Technology Reference
In-Depth Information
C
)(
k
-dep) we denote the
Also different arity fragments were defined. By FO(
C
) in which only dependence atoms of the form =(
x
1
,...,x
n
+1
)
sentences of FO(
with
n
≤
k
may appear. FO(
C
)(
k
-ind) denotes the sentences of FO(
C
)inwhich
only independence atoms containing at most
k
+1 different variables may appear.
It was shown in [10,4] that (under the lax team semantics)
↥
c
)(
k
-ind)
where ESO(
k
-ary) denote the sentences of ESO in which the quantified functions
and relations have arity at most
k
. This yields a strict arity hierarchy for both
FO(=(
...
)) and FO(
ESO(
k
-ary) = FO(=(
...
))(
k
-dep) = FO(
↥
c
) since the property “
R
is even” is definable in ESO(
k
-ary)
but not in ESO(
k
1-ary), for
k
-ary
R
[12].
The main contribution of this article is to show that arity fragments of inclu-
sion logic also give rise to a strict expressivity hierarchy. We let FO(
−
C
)(
k
-inc)
denote the FO(
C
) sentences in which at most
k
-ary inclusion atoms (i.e. atoms
of the form
x
ↆ
y
where
|
x
|
=
|
y
|≤
k
) may appear. For proving the claim, we
define, for each
k
≥
2, a graph property which is definable in FO(
ↆ
)(
k
-inc) but
not in FO(
1-inc). The non-definability part of the proof will be based on
Martin Grohe's work in fixed-point logics in [13] where analogous results were
proved for transitive closure logic (TC), least fixed-point logic (LFP), inflation-
ary fixed-point logic (IFP) and partial fixed-point logic (PFP). We will also give
a negative answer to the open question presented in [4]; that was, whether the
fragments FO(
ↆ
)(
k
−
) give rise to an infinite expressivity hierarchy. This will
be done by showing that FO(
ↆ
)(
k
∀
). However, if the strict version
of team semantics is used, then we obtain that FO(
ↆ
)(1
∀
)=FO(
ↆ
ↆ
)(
k
∀
)
<
FO(
ↆ
)((
k
+1)
∀
)
[14].
The article is organized as follows. In Sect. 2 we define inclusion logic and
present some of its basic properties. In Sect. 3 we show two results for inclusion
logic. First we prove that the universal hierarchy collapses at level 1, and then
we show that the arity hierarchy is strict (the full proof of this is in Appendix).
In Sect. 4 we relate these results to analogous results in dependence logic and
its variants, and conclude the section by presenting open problems.
2 Preliminaries
2.1 Notation
Unless otherwise stated, we use
x
1
,x
2
,...
to denote variables and
t
1
,t
2
,...
to denote terms. Analogously, bold versions
t
2
,...
are used
to denote tuples of variables and tuples of terms, respectively. For tuples
a
and
b
,wewrite
ab
for the concatenation of the tuples. If
f
is a unary func-
tion and (
x
1
,...,x
n
) is a sequence listing members of Dom(
f
), then we write
f
(
x
1
,...,x
n
)for(
f
(
x
1
)
,...,f
(
x
n
)).
x
1
,
x
2
,...
and
t
1
,
2.2 Inclusion Logic
The syntax of FO(
ↆ
) is obtained by adding inclusion atoms to the syntax of
first-order logic.
