Information Technology Reference
In-Depth Information
≤
i
≤
n
, functions
F
i
:
X
[
F
1
/x
1
]
...
[
F
i−
1
/x
i−
1
]
→P
(
M
)
\
Then we find, for 1
{∅}
such that
F
i
(
s
)=
M
if
Q
i
=
∀
M
|
=
X
ʸ
where
,and
X
:=
X
[
F
1
/x
1
]
...
[
F
n
/x
n
]
.
=
X
ˆ
, it suces to show that
For
M
|
=
X
[
M/y
]
1
M
|
z
x
1
...x
i−
1
y
ↆ
z
x
1
...x
i−
1
x
i
∧
ʸ.
(1)
n
Q
i
=
∀
≤
i
≤
By Theorem 2
=
X
[
M/y
]
ʸ
, so it suces to consider only the new inclusion
atoms of (1). So let 1
M
|
n
be such that
Q
i
=
X
[
M/y
]; we
≤
i
≤
∀
and let
s
∈
need to find a
s
∈
X
[
M/y
] such that
s
(
x
1
...x
i−
1
y
)=
s
(
z
z
x
1
...x
i−
1
x
i
). Now,
since
Q
i
=
X
∀
,wenotethat
s
(
s
(
y
)
/x
i
)
∈
(Fr(
ˆ
)
∪{
x
1
,...,x
i
}
). Therefore
we may choose
s
to be any extension of
s
(
s
(
y
)
/x
i
)in
X
[
M/y
].
For the other direction, assume that
=
X
ˆ
.Thenfor1
M
|
≤
i
≤
n
,thereare
functions
F
i
:
X
[
F
1
/x
1
]
...
[
F
i−
1
/x
i−
1
]
→P
(
M
)
\ {∅}
such that (1) holds, for
X
:=
X
[
F
1
/x
1
]
...
[
F
n
/x
n
]
.
By Theorem 2
M
|
=
X
ʸ
, so it suces to show that,
n
with
Q
i
=
for all 1
,
F
i
is the constant function which maps assignments
to
M
.Solet
i
be of the above kind, and let
s
≤
i
≤
∀
∈
X
[
F
1
/x
1
]
...
[
F
i−
1
/x
i−
1
]and
a
X
[
F
1
/x
1
]
...
[
F
i
/x
i
].Firstnotethatsince
y
is universally quantified,
s
(
a/y
) has an extension
s
0
in
X
[
M/y
]. Therefore,
by (1), there is
s
1
∈
∈
M
. We need show that
s
(
a/x
i
)
∈
X
[
M/y
] such that
s
0
(
z
x
1
...x
i−
1
y
)=
s
1
(
z
x
1
...x
i−
1
x
i
).
Since now
s
1
agrees with
s
in Fr(
ˆ
)
∪{
x
1
,...,x
i−
1
}
and maps
x
i
to
a
,weobtain
that
s
(
a/x
i
)=
s
1
(Fr(
ˆ
)
∪{
x
1
,...,x
i
}
∈
X
[
F
1
/x
1
]
...
[
F
i
/x
i
]
.
)
3.3 Strictness of the Arity Hierarchy
In this section we show that the following strict arity hierarchy holds (already
in finite models).
Theorem 6.
For k
≥
2
,
FO(
ↆ
)(
k
−
1-inc)
<
FO(
ↆ
)(
k
-inc)
.
For proving this, we use the earlier work of Grohe in [13] where an analogous
result was proved for TC, LFP, IFP and PFP. More precisely, it was shown that,
for
k
≥
2,
TC
k
PFP
k−
1
≤
(2)
where the superscript part gives the maximum arity allowed for the fixed-point
operator. Since TC
k
LFP
k
IFP
k
PFP
k
, a strict arity hierarchy is ob-
≤
≤
≤
tained for each of these logics.
We start by fixing
˄
as the signature consisting of one binary relation symbol
E
and 2
k
constant symbols
b
1
,...,b
k
,c
1
,...,c
k
. Then the idea is to present a
FO(
ↆ
)(
k
-inc)[
˄
]-definable graph property, and show that it is not definable in
