Information Technology Reference
In-Depth Information
Step 4 At last, we will show that
X
∗
can be constructed by quantifying the
prefix
Q
1
x
1
...Q
m
x
m
in
A
{∅}
A
|
over
. Hence we will obtain that
=
ˆ
(
b
,ʵ
(
c
)). But now, since
A
|
=
¬
[TC
x
,
y
E
DGE
k
](
b
,ʵ
(
c
))
,
this contradicts the assumption that
ˆ
(
b
,
c
) defines
¬
[TC
x
,
y
E
DGE
k
]
(
b
,
c
). Hence the assumption is false and we obtain the result of Lemma 1.
The most dicult part of the proof is Step 3, and we will sketch this next.
The idea is that we define two operations auto and swap for teams
Y
of
A
with Dom(
Y
)=
.Thenwelet
X
∗
:= swap(auto(
X
)) and show by
induction on the complexity of
ʸ
that (4) follows from (3). In the induction proof,
the only non-trivial case is the base case where
ʸ
is either a first-order literal or
an (at most
k
{
x
1
,...,x
m
}
1-ary) inclusion atom. Let us now explore this base case in more
detail and examine how the two operations arise from it.
Consider first the case where
ʸ
is a first-order literal. For this, we define the
operation swap. For a team
Y
of
A
with Dom(
Y
)=
−
{
x
1
,...,x
m
}
,swap(
Y
) will
s
|
where
s
maps each variable
x
i
either to
s
(
x
i
)
be defined as a team
{
s
∈
Y
}
or
ʵ
s
(
x
i
). Here
ʵ
is the automorphism introduced in item 2 of Theorem 8. The
idea is to define swap so that for all teams
Y
of
A
with Dom(
Y
)=
ⓦ
{
x
1
,...,x
m
}
and all literals
ʸ
∈
FO[
˄
] we obtain that
A
,
b
,
c
|
=
Y
ʸ
⃒
A
,
b
,ʵ
(
c
|
=
swap(
Y
)
ʸ.
4
(
)
(
))
(5)
Consider then the case where
ʸ
=
y
1
...y
l
ↆ
z
1
...z
l
for
l
≤
k
−
1. First note
that in this case (5) does not necessarily hold. Since, assuming the left-hand side
of (5) and given any
s
0
∈ Y
, we first notice that there is an
s
1
∈ Y
such that
s
0
(
y
i
)=
s
1
(
z
i
) for all
i
.Now,given
s
0
of
s
0
, a natural choice from swap(
Y
)for
the inclusion atom would be
s
1
. However, this might not work since possibly
s
0
(
y
i
)=
ʵ
s
1
(
z
i
)forsome
i
. To overcome this, we again apply Theorem 8. This
time we compose assignments of teams with automorphisms obtained by item 4
of Theorem 8. Namely, we first let
I
consist of all
i
for which
s
0
(
y
i
)=
ʵ
ⓦ
s
1
(
z
i
).
Then by item 4 of Theorem 8 we find an automorphism
f
which maps
s
1
(
z
i
)to
ʵ
ⓦ
I
, but leaves all elements in rows of distance
>
1from(
s
1
(
z
i
))
i∈I
fixed. Then for
i
s
1
(
z
i
)for
i
ⓦ
∈
∈
I
, we obtain that
s
0
(
y
i
)=
ʵ
s
1
(
z
i
)=
f
s
1
(
z
i
)
,
ⓦ
ⓦ
s
1
(
z
i
)
.
4
A detailed definition of swap is in Appendix but it can be illustrated by using
Ehrenfeucht-Fraısse games [17,18]. The point is that we have chosen
n
:= 2
m
+2
so
that Duplicator has a winning strategy in the
m
-round Ehrenfeucht-Fraısse game
EF
m
((
A
,
b
,
c
)
,
(
A
,
b
,ʵ
(
c
)). Then for each
s ∈ Y
,welet
s
correspond to Duplicator's
choices in a single play of EF
m
((
A
,
b
,
c
)
,
(
A
,
b
,ʵ
(
c
)) where Spoiler picks members of
(
A
,
b
,
c
) according to
s
and Duplicator picks members of (
A
,
b
,ʵ
(
c
)) according to her
winning strategy (see Fig. 1 in Appendix). Then we obtain that (5) holds.
I
, we obtain that
s
0
(
y
i
)=
s
1
(
z
i
)=
f
and for
i
∈
ⓦ
