Information Technology Reference
In-Depth Information
1-inc)[ ˄ ]. This graph property will actually be a negated version of
the one that separates the fragments in (2). For this, we first define a first-order
formula indicating that the k -tuples
)( k
FO(
x
y
form a 2 k -clique in a graph. Namely,
and
we define E DGE k (
x
,
y
) as follows:
):=
1 ≤i,j≤k
E DGE k (
x
,
y
E ( x i ,y j )
( E ( x i ,x j )
E ( y i ,y j )) .
1 ≤i = j≤k
Using this we define the graph property. Let
x
,
y
be tuples of disjoint variables
and
t
,
u
tuples of terms, all of the same length. Then for a first-order formula
ˈ (
x
,
y
M |
¬
[TC x , y ˈ ](
t
,
u
t M ,
u M ) is not in the transitive
), we write
=
)if(
{
m 1 ,
m 2 )
| M |
= ˈ (
m 1 ,
m 2 )
}
closure of
. Note that by transitive closure of a
binary relation R we denote the smallest transitive relation containing R .Now,
given two k -ary tuples of disjoint constant terms b and c , the non-trivial part is
to show that ¬ [TC x , y E DGE k ]( b , c ) is not definable in FO( )( k − 1-inc)[ ˄ ]. It is
definable in FO(
(
)( k -inc)[ ˄ ] by the following theorem.
Theorem 7 ([1]). Let ˈ (
x
,
y
) be any first-order formula, where
x
and
y
are
. Furthermore, let ˈ (
k
ary tuples of disjoint variables, for some k
N \{
0
}
x
,
y
)
be the result of writing
¬
ˈ (
x
,
y
) in negation normal form. Then for all models
M
containing the signature of ˈ, and all pairs
b
,
c
of k-ary constant term tuples
of the model,
M |
= ˆ
M |
=
¬
[TC x , y ˈ ](
b
,
c
) ,
for ˆ defined as
( ˈ (
z
(
b z z
=
c ∧∀ w
z
,
w
)
w z
)) .
Note that ˆ is not yet of the right form since Definition 1 does not allow terms to
appear in inclusion atoms. This is however not a problem since all the terms that
appear in inclusion atoms can be replaced by using new existentially quantified
variables and new identity atoms.
Hence, for Theorem 6, it suces to prove that
¬
b
,
c
[TC x , y E DGE k ](
)isnot
)( k
1-inc)[ ˄ ]. In this part we follow the work in [13]. For
definable in FO(
k,n
1, we first let
C k,n denote the set of all graphs
A
with universe
A := { 1 ,...,n}×{−k,...,− 1 , 1 ,...,k}.
The following theorem generates a graph A ∈C k,n which will be used in the
non-definability proof. It was originally proved by Grohe using a method of
Hrushovski [16] to extend partial isomorphisms of finite graphs.
Theorem 8 ([13]). Let k,n
2 . Then there exists a graph
A ∈C k,n such that:
1. There exists a mapping row : A
→{
1 ,...,n
}
such that
A :( E A ab
a, b
⃒|
row( b )
row( a )
|≤
1) .
Search WWH ::




Custom Search