Information Technology Reference
In-Depth Information
3.1 Syntactical Fragments
Definition 3.
Let
Cↆ{ↆ
,
=(
...
)
,
↥
c
,
↥}
. Then universal and arity fragments
of
FO(
C
)
are defined as follows:
-
FO(
C
)(
k
∀
)
is the class of
FO(
C
)
formulae in which at most k universal quan-
tifiers may appear,
-
FO(
C
)(
k
-inc)
is the class of
FO(
C
)
formulae in which inclusion atoms of
the form
x
1
ↆ
x
2
where
x
1
and
x
2
are sequences of length at most k,may
appear,
-
FO(
C
)(
k
-dep)
is the class of
FO(
C
)
formulae in which dependence atoms of
the form
=(
x
1
,x
2
)
where
x
1
x
2
is a sequence of length at most k
+1
,may
appear,
-
FO(
C
)(
k
-ind)
is the class of
FO(
C
)
formulae in which conditional indepen-
dence atoms of the form
x
2
↥
x
1
x
3
where
x
1
x
2
x
3
is a sequence listing at
most k
+1
distinct variables, may appear.
For an increasing (with respect to
≤
) sequence of logics (
L
k
)
k∈
N
,wesaythat
the
L
m
=
k∈
N
L
k
.Ifthe
L
k
-hierarchy does
not collapse at any level, then we say that the hierarchy is infinite. An infinite
L
k
-hierarchy is called strict if
L
k
-hierarchy collapses at level
m
if
L
k
<
L
k
+1
for all
k
∈
N
.
As mentioned before, we show that the FO(
ↆ
)(
k
∀
)-hierarchy collapses already
at level 1 but FO(
ↆ
)(
k
-inc) forms a strict hierarchy which holds already in finite
models.
3.2 Collapse of the Universal Hierarchy
We first show that the universal hierarchy of inclusion logic collapses. This is done
by introducing a translation where all universal quantifiers are removed, and new
existential quantifiers, new inclusion atoms and one new universal quantifier are
added. The translation holds already at the level of formulae.
Theorem 5.
FO(
ↆ
)(1
∀
)=FO(
ↆ
)
.
) be a formula. We define a formula
ˆ
∈
Proof.
Let
ˆ
∈
FO(
ↆ
FO(
ↆ
)(1
∀
)such
ˆ
. By Theorem 3 we may assume that
ˆ
is of the form
that
ˆ
≡
Q
1
x
1
...Q
n
x
n
ʸ
where
ʸ
is quantifier-free. We let
ˆ
:=
∃x
1
...∃x
n
∀y
(
1
≤i≤n
Q
i
=
∀
z
x
1
...x
i−
1
y ↆ
z
x
1
...x
i−
1
x
i
∧ ʸ
)
where
z
lists Fr(
ˆ
). Let now
M
be a model and
X
a team such that Fr(
ˆ
)
ↆ
=
X
ˆ
. By Theorem 2 we may assume
without loss of generality that Fr(
ˆ
)=Dom(
X
). Assume first that
Dom(
X
); we show that
M
|
=
X
ˆ
⃔
M
|
M
|
=
X
ˆ
.
