Information Technology Reference
In-Depth Information
2. There exists an automorphism ʵ of
A
that is self-inverse and preserves the
rows i.e.
-
ʵ
−
1
=
ʵ,
-
A
:row(
ʵ
(
a
)) = row(
a
)
.
3. There exist tuples
∀
a
∈
b
,
c
∈
A
k
in the first and last row respectively
(i.e.
∀
i
≤
k
:(row(
b
i
)=1
∧
row(
c
i
)=
n
)
) such that
))
.
3
A
|
=
¬
[TC
x
,
y
E
DGE
k
](
b
,
c
)
and
A
|
=
¬
[TC
x
,
y
E
DGE
k
](
b
,ʵ
(
c
4. For all a
1
,...,a
k−
1
∈
that is self-
inverse, preserves the rows, and maps a
1
,...,a
k−
1
according to ʵ, but leaves
all elements in rows of distance >
1
from
row(
a
1
)
,...,
row(
a
k−
1
)
fixed i.e.
-
f
−
1
=
f
-
A there exists an automorphism f of
A
∀
a
∈
A
:row(
f
(
a
)) = row(
a
)
,
-
1:
f
(
a
i
)=
ʵ
(
a
i
)
,
-
for each a
∀
i
≤
k
−
∈
A with
∀
i
≤
k
−
1:
|
row(
a
)
−
row(
a
i
)
|
>
1
we have f
(
a
)=
a.
Using this theorem we can prove the following lemma.
Lemma 1.
Let k
2
and let ˄ be a signature consisting of a binary relation
symbol E and
2
k constant symbols b
1
,...,b
k
,c
1
,...,c
k
.Then
¬
≥
[TC
x
,
y
E
DGE
k
](
b
,
c
)
is not definable in
FO(
ↆ
)(
k
−
1-inc)[
˄
]
.
The proof of Lemma 1 is in Appendix but the outline of the proof is listed below.
Step 1 First we assume to the contrary that there is a
ˆ
(
b
,
c
∈
ↆ
)(
k
−
1-inc)
[
˄
] which is equivalent to
¬
[TC
x
,
y
E
DGE
k
](
b
,
c
). By Theorem 3 we may
assume that
ˆ
is of the form
Q
1
x
1
...Q
m
x
m
ʸ
where
ʸ
is a quantifier free
formula from FO(
)
FO(
1-inc)[
˄
].
Step 2 We let
n
=2
m
+2
and obtain a graph
ↆ
)(
k
−
A
∈C
k,n
for which items 1-4 of
Theorem 8 hold. In particular, we find two
k
-ary tuples
b
and
c
such that
A
|
=
¬
[TC
x
,
y
E
DGE
k
](
b
,
c
)and
A
|
=
¬
[TC
x
,
y
E
DGE
k
](
b
,ʵ
(
c
)). Then by
the assumption (
A
,
b
,
c
)
|
=
ˆ
, and hence we find, for 1
≤
i
≤
m
, functions
F
i
:
{∅}
[
F
1
/x
1
]
...
[
F
i−
1
/x
i−
1
]
→P
(
A
)
\{∅}
such that
F
i
(
s
)=
A
if
Q
i
=
∀
,and
(
A
,
b
,
c
)
|
=
X
ʸ
(3)
[
F
1
/x
1
]
...
[
F
m
/x
m
].
Step 3 From
X
we will construct a team
X
∗
such that
where
X
:=
{∅}
(
A
,
b
,ʵ
(
c
))
|
=
X
∗
ʸ.
(4)
3
In [13],
c
and
ʵ
(
c
) are here placed the other way round. This is however not a
problem since
ʵ
is self-inverse and preserves the rows.
