Locality of order-invariant first-order formulas.
A query is local if the decision of whether a tuple in a structure satisfies this query only depends on a small neighborhood of the tuple. We prove that all queries expressible by order-invariant first-order formulas are local.
Introduction
One of the fundamental properties of first-order formulas is their locality, which means
that the decision of whether in a fixed structure a formula holds at some point (or at a
tuple of points) only depends on a small neighborhood of this point (tuple). This result,
proved by Gaifman [5], gives a good intuition for the expressive power of first-order
logic. In particular, it provides very convenient proofs that certain queries cannot be expressed
by a first-order formula. For example, to decide whether there is a path between
two vertices of a graph it clearly does not suffice to look at small neighborhoods of these
vertices. Hence by locality, s-t-connectivity is not expressible in first-order logic. Re-
cently, Libkin and others [3, 8-10] systematically started to explore locality as tool for
proving inexpressibility results. The ultimate goal of this line of research would have
been to separate complexity classes, in particular to separate TC 0 , that is, the class of
languages that can be recognized by (uniform) families of bounded-depth circuits with
majority gates, from LOGSPACE. However, a recent result of Hella [7], showing that
even uniform AC 0 contains non-local queries, has destroyed these hopes.
Nevertheless, locality remains an important tool for proving inexpressibility results
for query languages. In database theory, one often faces a situation where the physical
representation of the database, which we consider as a relational structure, induces an
order on the structure, but this order is hidden to the user. The user may use the order
in her queries, but the result of the query should not depend on the given order. In other
words, the user may use the fact that some order is there, but since she does not know
which one she cannot make her query depend on any particular order. It may seem
that this does not help her, but actually there are first-order formulas that use the order
to express order-invariant queries that cannot be expressed without the order. This is an
unpublished result due to Gurevich [6]; for examples of such queries we refer the reader
to [1, 2] and Example 6 (due to [4]).
Formally, we say that a first-order formula '(-x) whose vocabulary contains the
order symbol - is order-invariant on a class C of structures if for all structures A 2 C,
tuples - a of elements of A, and linear orders - 1 , - 2 on A we have: '(-a) holds in
if, and only if, '(-a) holds in It is an easy consequence of the interpolation
theorem that if a formula is order-invariant on the class of all structures, it is equivalent
to a first-order formula that does not use the ordering. This is no longer true when
restricted to the class of all finite structures, or to a class consisting of a single infinite
structure. Unfortunately, these are the cases showing up naturally in applications to
computer science.
We prove that for all classes C of structures the first-order formulas that are order-
invariant on C can only define queries that are local on all structures in C. As for (pure)
first-order logic, this property of being local gives us a good intuition about the expressive
power of order-invariant first-order formulas and a simple method to prove
inexpressibility results.
The paper is organized as follows: After the preliminaries, we prove the locality
of order-invariant first-order formulas with one free variable in Section 3. This is the
crucial step towards our main result. In the following section we reduce the case of
formulas with arbitrarily many variables to the one-variable case.
We would like to thank Juha Nurmonen for pointing us to the problem and Clemens
Lautemann for fruitful discussions about its solution.
Preliminaries
A vocabulary is a set - containing finitely many relation and constant symbols. A -
structure A consists of a set A, called the universe of A, an interpretation R A ' A r
for each r-ary relation symbol R 2 - , and an interpretation c A 2 A of each constant
For example, a graph can be considered as an fEg-structure
E is a binary relation symbol.
An ordered structure is a structure whose vocabulary contains the distinguished
binary relation symbol - which is interpreted as a linear order of the universe.
denotes the set of integers.
Occasionally, we need to consider strings as finite structures. For each l - 1, we let
- l denote the vocabulary f-;
and constant symbols min and max. We represent a string over an l-letter
alphabet by the ordered - l -structure with universe [1; n], where P j
is interpreted as g, for every j, and In our notation we
do not distinguish between the string s and its representation as a finite structure s. For
a given l ? 0 we refer to such strings as l-strings.
If A is a structure and B ' A a subset that contains all constants of A, then the
(induced) substructure of A with universe B is denoted by hBi A .
Let oe ae - be vocabularies. The oe-reduct of a -structure A, denoted by Aj oe , is
the oe-structure with universe A in which all symbols of oe are interpreted as in A. On
the other hand, each -structure A such that Aj called a -expansion of B.
For a oe-structure B, relations R
the expansion of B of a suitable vocabulary
- oe oe that contains in addition to the symbols in oe a new k i -ary relation symbol for
each new constant symbols.
a class of -structures. A k-ary query on C is a mapping ae that
assigns a k-ary relation on A to each structure A 2 C such that for isomorphic -
structures each isomorphism f between A and B is also an isomorphism
between the expanded structures (A; ae(A)), (B; ae(B)). A Boolean (or 0-ary) query on
C is just a subclass of C that is closed under isomorphism.
2.1 Types and games
Equivalence in first-order logic can be characterized in terms of the following Ehren-
Definition 1. Let r - 0 and A; A 0 structures of the same vocabulary. The r-round EF-
game on A; A 0 is played by two players called the spoiler and the duplicator. In each of
the r rounds of the game the spoiler either chooses an element v i of A or an element v 0
of A 0 . The duplicator answers by choosing an element v 0
i of A 0 or an element v i of A,
respectively.
The duplicator wins the game if the mapping that maps v i to v 0
and each
constant c A to the corresponding constant c A 0
is a partial isomorphism, that is, an isomorphism
between the substructure of A generated by its domain and the substructure
of A 0 generated by its image.
It is clear how to define the notion of a winning strategy for the duplicator in the
game.
The quantifier-depth of a first-order formula is the maximal number of nested quantifiers
in the formula. The r-type of a structure A is the set of all first-order sentences of
quantifier-depth at most r satisfied by A. It is a well-known fact that for each vocabulary
- there is only a finite number of distinct r-types of -structures (simply because there
are only finitely many inequivalent first-order formulas of vocabulary - and quantifier-
depth at most r). We write A - r A 0 to denote that A and A 0 have the same r-type.
Theorem 2. Let r - 0 and A; A 0 structures of the same vocabulary. Then A - r A 0 if,
and only if, the duplicator has a winning strategy for the r-round EF-game on A; A 0 .
The following two simple examples, both needed later, may serve as an exercise for
the reader in proving non-expressibility results using the EF-game.
Example 3. Let r - 1 and Using the r-round EF-game, it is not hard to see
that the strings 1 have the same r-type. This implies, for example,
that the class f1 n cannot be defined by a first-order sentence.
Example 4. We may consider Boolean algebras as structures of vocabulary ft; u; :;
0; 1g. In particular, let P(n) denote the power-set algebra over [1; n]. It is not hard to
prove that for each r - 1 there exists an n such that P(n) - r P(n+ 1). Thus the class
eveng cannot be defined by a first-order sentence.
In some applications, it is convenient to modify the EF-game as follows: Instead of
choosing an element in a round of the game, the spoiler may also decide to skip the
round. In this case, v i and v 0
remain undefined; we may also write v
course undefined v i s are not considered in the decision whether the duplicator wins. It
is obvious that the duplicator has a winning strategy for the r-round modified EF-game
on A; A 0 if, and only if, she has a winning strategy for the original r-round EF-game on
2.2 Order invariant first-order logic
Definition 5. Let - be a vocabulary that does not contain - and C a class of -struc-
tures. A formula '(x vocabulary - [f-g is order-invariant on C if for all
linear orders of A we have
If ' is order invariant on the class fAg we also say that ' is order-invariant on A.
To simplify our notation, if a - [ f-g-formula '(-x) is order-invariant on a class
C of -structures and A 2 C, - a 2 A we write A j= inv '(-a) to denote that for some,
hence for all orderings - on A we have (A; -) '(-a). Furthermore, we say that '(-x)
defines the query A 7! f-a j A j= inv '(-a)g on C. 1 We can easily extend the definition
to Boolean queries.
Let us emphasize that, although order-invariant first-order logic sounds like a restriction
of pure first-order logic, it is actually an extension: There are queries on the
class of all finite structures that are definable by an order-invariant first-order formula,
but not by a pure first-order formula [6]. The following example can be found in [4].
Example 6. There is an order-invariant first-order sentence ' of vocabulary
that defines the query fP(n) j n eveng on the class of all finite
Boolean algebras. By Example 4, this query is not definable in first-order logic.
Similarly, if we let A be the disjoint union of all structures P(n), for n - 1, then
the unary query "x belongs to a component with an even number of atoms" on fAg is
definable by an order-invariant first-order formula, but not by a plain first-order formula.
2.3 Local formulas
Let A be a -structure. The Gaifman graph of A is the graph with universe A where
are adjacent if there is a relation symbol R 2 - and a tuple - c such that R A - c
and both a and b occur in - c.
The distance d A (a; b) between two elements is defined to be the length of
the shortest path from a to b in the Gaifman graph of A; if no such path exists we let
d A (a; 1. The ffi-ball around a 2 A is defined to be the set B A
d A (a; b) - ffig, and the ffi-sphere is the set S A
ffig. If A is
clear from the context, we usually omit the superscript A .
For sets B; C ' A we let d(B;
(b). For tuples - a = a
let
1 This is ambiguous because '(-x) also defines a query on the class of all - [ f-g-structures.
But if we speak of a query defined by an order-invariant formula, we always refer to the query
defined in the text.
Definition 7. (1) A k-ary query ae on a class C is local if there exists a - 0 such that
for all A 2 C and -
we have
The least such - is called the locality rank of ae.
that is order-invariant on a class C is local, if the query it defines
is local. The locality rank of '(-x) is the locality rank of this query.
It should be emphasized that, in the definition of local order-invariant formulas, neither
the isomorphisms nor the distance function refer to the linear order.
Gaifman [5] has proved that first-order formulas can only define local queries.
3 Locality of invariant formulas with one free variable
In this section we are going to show that if a first-order formula with one free variable
is order-invariant on a class C of structures then it is also local on C. Before we formally
state and prove this result, we need some preparation.
Lemma 8. For all l; r 2 N there are m;n 2 N such that for all l-strings s of size at
least n there are unary relations P and P 0 on s such
Proof. Let l; r 2 N be fixed and t the number of r-types of vocabulary - l . We let
choose n large enough such that whenever the edges of a complete
graph with n vertices are colored with t colors, there is an induced subgraph of size
of whose edges have the same color.
be an l-string of length n 0 - n. For
denote the l-substring s
For we color the pair fi; jg (that is, the edge fi; jg of the complete graph
on [1; n]) with the r-type of (the representation of) hi; ji. By the choice of n we find
such that all structures hp
have the same r-type. We let g.
We claim that (s; P Intuitively, we prove this claim by carrying over a
winning strategy for the duplicator on the strings
our structures. Recall from Example 3 that such a strategy exists.
Formally, we proceed as follows: We define a mapping f : [1;
by
Consider the r-round EF-game on (s; P As usual, let v i and v 0
i be the elements
chosen in round i. It is not too difficult to prove, by induction on i, that the duplicator
can play in such a way that for every i - r one of the following conditions holds:
and the following two subconditions hold:
(a) The duplicator has a winning strategy for the (r \Gamma i)-round modified EF-game
on (u; f(v 1
(b) The duplicator has a winning strategy for the (r \Gamma i)-round modified EF-
game on (hp f(v i
is the identity on hp f(v i
else and g 0 is the identity on hp f(v 0
Clearly, this implies the claim and thus the statement of the lemma. 2
Lemma 9. If a first-order formula '(x) is order-invariant on a class C of structures
then it is local on C.
Proof. Let '(x) be a first-order formula of quantifier-depth r that is order-invariant on
a class C of -structures.
Let l 0 be the number of different r-types of vocabulary - [
the Q i are new unary relation symbols and let l := l 0
2 . Let m and n be given by Lemma
8 above w.r.t. r and l. Let - := n(2 r
- (b) via an isomorphism -.
Our goal is to show that there are linear orders - 1 and - 2 on A such that
b). From this we can conclude
A
In order to prove the existence of such linear orders, we first show that, w.l.o.g., we can
assume the following.
There is a set W ' fa; bg, and an automorphism ae on hB - (W )i such
that
To show this, we distinguish the following two cases.
2-. In this case we simply set W := fa; bg and define ae by
Case 2: Assume first that d(a; - i (a)) ? 4-, for some i ? 0.
Then we also have d(b; - i (a)) ? 2-. Furthermore, by the choice of -, B - (a)
(b). We can conclude from the proof given below that
A
If, on the other hand, d(a; every i, we set
Hence, we can assume (*). In the following we only make use of B - (a)
opposed to B - (a)
It is easy to see that every sphere S i (W ) is a disjoint union of orbits of ae, i.e. a
disjoint union of sets of the form We fix, for every
some linear order of the orbits of the sphere S i (W ). Next we fix a preorder OE on A
with the following properties.
- OE is a linear order on
are in the same sphere S i (W ) but the
orbit of c comes before the orbit of c in the order of the orbits that was chosen
above, and
- c and c 0 are not related with respect to OE, whenever c; c are
in the same orbit.
Both linear orders - 1 and - 2 will be refinements of OE. They will only differ inside
some of the orbits.
We can assume that no sphere S i (W ), with i -, is empty. Otherwise, B - (W )
would be a union of connected components of A, hence we could fix any linear order -
on the orbits of B - (W ) and define - 1 by combining - with OE and - 2 by combining
the image of - under ae with OE.
For each orbit O, we fix a vertex v(O) and define a linear order - 0 on O by
O is finite and by \Delta
ae O is infinite. For every
k, we denote by - k the image of - 0 under ae k . It is easy to see that (S i (W
To catch the intuitive idea of the proof, the reader should picture the spheres S i (W )
(for as a sequence of concentric cycles, W itself being innermost. Outside
these cycles is the rest of the structure A, fixed once and for all by the order OE. The
automorphism ae is turning the cycles, say, clockwise. In particular, it turns the cycle W
far enough to map a to b. Each cycle is ordered clockwise by - 0 . The ordering - k is the
result of turning the cycle k-steps. (Unfortunately, all this is not exactly true, because
usually the orbits do not form whole spheres. They may form small cycles or "infinite
cycles". But essentially it is the right picture.)
To define the orders - 1 and - 2 we proceed as follows. On W we let - 1 =- 0 and
looks from a as - 2 looks from b, and this is how it should
be. On the other hand, on the outermost cycle S - (W ) both orderings should be the
same, because the outside structure is fixed. So we let - 1 =- 2 =- m on S - (W ) (for the
fixed in the beginning of the proof). Now we determine two sequences
already know that on . For all
on S j (W ) but once we reach j 1 we turn it one step. That is, we let - 1 =- 1 on S j1 (W ).
We stick with this, until we reach S j2 (W ), and there we turn again and let - 1 =- 2 . We
go on like this, and after the last turn at S jm (W ) we have - 1 =- m , and that is what
we wanted. Similarly, we define - 2 by starting with - 1 and taking turns at all spheres
Again we end up with - 2 =- m on all spheres S k (W ) for
But of course the turns can be detected, so how can we hide that we took one more
turn in defining - 1 ? The idea is to consider the sequence of spheres as a long string,
whose letters are the types of the spheres. The positions where a turn is taken can
be considered as a unary predicate on this string. By Lemma 8, we can find unary
predicates of sizes m and respectively, such that the expansions of our string by
these predicates are indistinguishable. This is exactly what we need.
Essentially, this is what we do. But of course there are nasty details
1. For every i with
the
substructure of A that is induced by the spheres S ih\Gammaj (W
let, for every be the structure T i
Let the linear order - j on T i be defined by combining the orders - j on the spheres
of T i with OE. Finally let E j be the linear order on T i that is obtained by combining OE
with for the spheres S q (W ) with q - ih, and with - j+1 for the spheres S q (W )
with q ? ih. For every
For every i, we define the unary relations Q
S ic+j (W ), i.e., a vertex v is in Q j , if its distance from the central sphere in T i is j.
Now we define an l-string l be an enumeration
of all pairs of r-types of - [ g-structures. We set s
the pair (r-type of (T i
By Lemma 8 and our choice of the parameters l; there exist unary relations
and the duplicator has a winning strategy in
the r-round game on (s; P ) and (s; P 0 ). Now we are ready to define the linear orders - 1
and - 2 on A. For every i, let
- 1 is defined on T i as - u(i) , if i 62 P and as E u(i) , if
is defined on T i as - u(i) , if
Observe that, although T i and T i+1 are not disjoint, these definitions are consistent.
It remains to show that the duplicator has a winning strategy in the r-round game
on b). The winning strategy of the duplicator will be obtained
by transferring the winning strategy on (s; P ) and (s; P 0 ), making use of the gap preserving
technique that was invented in [11].
For every fi; fl, with we define a function f fi;fl from
A to
if x is in T i
We are going to show that the duplicator can play in such a way that for every i the
following conditions hold.
(1) There exist fi; such that all vertices
are in some T q
(fi;fl) , in one of S
that between successive super-spheres there is a gap of 2 r\Gammai spheres that do not
contain any chosen vertices).
(2) The duplicator has an (r \Gamma i)-round winning strategy in the modified game on
(s;
(3) For every
fi;fl then the duplicator has a (r\Gammai)-round winning strategy
in the modified game on the structures (T f fi;fl (v j )
(4) For every
(5) For every
We refer to elements elements to elements of B -\Gammafi (W
as middle elements and to the others as outer elements.
First, we show that we can conclude from these conditions that the duplicator has
a winning strategy. Let v
r be the elements that were chosen
during the game. Let j; k - r. We have to show that
(a) a if and only if v 0
(b) the mapping a 7! b, v i 7! v 0
r) is a partial isomorphism,
(c)
k .
(a) follows immediately from (5). Remember the definition of the spheres in A. It
implies that only elements of the same sphere or of succeeding spheres are related by
a relation of A. Hence if v j and v k are not of the same group of elements (i.e., inner,
middle or outer) then (b) follows immediately because (1) ensures by the properties of fi
and fl and (3) - (5) ensure that v 0
k are in the same group as v j and v k , respectively.
(c) follows for similar reasons.
are both middle (outer, inner) elements then (b) and (c) follow immediately
from (2) and (3) (respectively (4), (5)).
It remains to show, by induction on i, that (1)-(4) hold, for every i - r.
For are immediate and (2) holds by
Lemma 8.
Now be true for w.l.o.g., the spoiler have selected
a vertex v i in (A; - 1 ). (The case where he chooses v 0
i is completely analogous, as
conditions (1) to (5) are symmetric.) Let fi denote the values of fi and fl that are
obtained from (1) for We distinguish the following cases.
. In this case, we can choose
immediately hold by induction.
In this case, we also choose . There are 2
subcases.
By induction, there is an element z of
s such that the duplicator has a winning strategy in the (r \Gamma i) round game
on (s;
In
as have the same
r-type. As f fi;fl (v i only if z 2 P 0 , either the two substructures
have linear orders of type - j and - j 0
for some j; j 0 or they have linear orders
of type
for some j; j 0 . In either case there exists an element v 0
in
T z such that (3) holds. By the choice of z, (2) also follows. (1) holds as v i
and v 0
are in the same Q p . (4) holds because for the outer structure nothing
has changed. Finally, (5) still holds, as B fl (W ) is not affected, either.
By (3) of the induction hypothesis
the duplicator has a (r winning strategy in the modified
game on the structures (T f fi;fl (v j )
hence there is a v 0
i such that she still has a (r \Gamma i)-round winning strategy
in the modified game on the structures (T f fi;fl (v j )
and (T f fi;fl (v 0
This implies (3). (1), (2), (4) and
immediately.
lies
in a former gap). There are 2 subcases.
In this case, we choose
In this case, we choose
The existence of an appropriate v 0
i follows in both cases analogous to (ii), as condition
(3) ensures the existence of a winning strategy also for a buffer zone of
This case can be handle
as the second subcase of (iii).
. In this case, fi and fl are chosen in
the same way as in the first subcase of (iii) and v 0
i is chosen as ae(v i ). Hence, (1) -
hold.
Simply choose v 0
immediately,
In all cases fi
Remark 10. For later reference, let us observe that the lemma implies the statement
that the locality rank of '(x) on C is bounded by a function of the vocabulary and
quantifier-depth of '(x). More precisely, for each vocabulary - and r - 0 there is a
-; r) such that the following holds: If a first-order formula '(x) of vocabulary
- and quantifier-depth at most r is order-invariant on a class C of -structures, then it is
local on C with locality rank at most -.
(To see that this follows from the Lemma, let C be the class of all structures A
such that '(x) is order-invariant on A and remember that there are only finitely many
first-order formulas of vocabulary - and quantifier-depth at most r.)
4 Locality of invariant formulas with arbitrarily many free
variables
Lemma 11. Let - be a vocabulary and r - 0; k - 1. Then there exists a -;
such that the following holds: If '(x is a first-order formula of vocabulary
- and quantifier-depth at most r that is order-invariant on a -structure A, then for all
we have
A
Proof. We first give a sketch of the proof.
The proof is by induction on k. For the lemma just restates the locality of
order-invariant first-order formulas with one free variable, proved in Lemma 9.
For k ? 1, we assume that we have k-tuples - a, - b in A such that all the a i ; a j and
are far apart (as the hypothesis of the Lemma requires) and we have an isomorphism
for a sufficiently large -. We prove that - a and - b cannot
be distinguished by order-invariant formulas of vocabulary - and quantifier-depth
at most r.
We distinguish between three cases:
The first is that some b i , say, b k , is far away from - a. Then we can treat a
as constants and apply Lemma 9 to show that a k and b k cannot be distinguished in the
expanded structure (A; a (Here we use the hypothesis d(a
1). Then we treat b k as a constant and apply the induction hypothesis to
prove that the cannot be distinguished in the
expanded structure (A; b k ). (This requires our hypothesis that
The second case is similar, we assume that for some h - 1 the iterated partial
isomorphism - h maps some a i far away from - a. Then we first show that - a and - h (-a)
cannot be distinguished and then that - h (-a) and - b cannot be distinguished.
The third case is that for all h - 1 the entire tuple - h (-a) is close to - a. Then some
restriction of - is an automorphism of a substructure of A that maps - a to - b. We can
modify this substructure in such a way that the tuples - a and - b can be encoded by single
elements and then apply Lemma 9.
Now we describe the proof in more detail. As noted before, we prove the lemma by
induction on k. For it follows from Lemma 9, recalling Remark 10 to see that
r) is a function of - and r.
suppose that the statement of the lemma is proved for all
Let - be a vocabulary and r - 0. Let -
binary relation symbols and d
not contained in - . Let -
Let A be a -structure and - a = a
2- and d(b
We shall prove that
A
Let - be an isomorphism between hB -a)i A and hB - b)i A .
1: There is an i - k such that for all j - k we have
Without loss of generality we can assume that k has this property. Then in the
Here we use the hypothesis that
Note that the formula is order-invariant on the structure
Since we can assume that - is greater than or
equal induction hypothesis we have
A
Next, note that in the - [ fd 1 g-structure
Here we use the hypothesis that
A similar argument as above shows that
A
(4) and (5) imply (2).
CASE 2: Case 1 does not hold, and there is a z 2 Z and an i - k such that for all
We choose z with this property such that jzj is least possible For
Again we assume, without loss of generality, that for all j - k we have
This suffices to prove, as in Case 1, that
A
and a similar argument shows
that
A
This again yields (2).
CASE 3: For all z 2 Z and i - k there is a j - k such that d(- z (a i ); a
Note that for all z 2 Z the domain of - contains B 2- z (a 1
the domain of - is B 6-a) and - z (a j
is an automorphism of the substructure
hBi A .
binary relation symbols not contained in - . We expand A to a
1. Note that - remains an automorphism of hBi E . Thus
: For all z 2 Z we
have
Furthermore, / is order-invariant on E. Hence by our choice of - and (6) we have
and thus (2).Theorem 12. Every first-order formula that is order-invariant on a class C of structures
is local on C.
Proof. Again we first give a sketch of the proof.
The proof is by induction on the number k of free variables of a formula. We have
already proved that formulas with one free variable are local.
be invariant on C, A 2 C, and - a, - b 2 A k such that hB -a)i A
for a sufficiently large -. Either all the a i ; a j and b are far apart, then we
can apply Lemma 11, or some of them are close together. In the latter case, we define
a new structure where we encode pairs of elements of A that are close together by
new elements. This does not spoil the distances too much, and we can encode our k-tuples
by smaller tuples that still have isomorphic neighborhoods. On these we apply
the induction hypothesis.
More formally, we prove the following statement by induction on k: Let - be a vocabulary
and r - 0; k - 1. Then there is a -; such that for all first-order formulas
vocabulary - and quantifier depth at most r and all -structures
A we have: If ' is order-invariant on A, then ' is local on A with locality-rank at most
For this follows from Lemma 9 (cf. Remark 10). So suppose it is proved for
all be a first-order formula of vocabulary - and quantifier-
rank r that is order invariant on a -structure A.
We choose -; according to the Lemma 11. Let R 1 binary relation
symbols not contained in - and - g. We let -
Let B be the - 0 -structure obtained from A by adding a new vertex
2-, an R 1 -edge from b(a 1 ; a 2 ) to a 1 , and an R 2 -edge
from b(a 1 ; a 2 ) to a 2 . Note that for all a; b 2 A we have
For
Then for all a
A
Furthermore, / ij is order-invariant on B. Thus by our induction hypothesis, it is local
on B with locality rank at most - 0 .
k such that
If d A (a i ; a we have
A
by Lemma 11.
So without loss of generality we can assume that d(a 1 ; a 2 ) - 2-. Since 2-, by
we also have d A (b Consider the structure B(A). By (7), for all
a 2 A we have
(a). Hence
by (9) and the definition of B. Thus
which implies
A
by (8). 2
5 Further research
The obvious question following our result is: What else can be added to first-order logic
such that it remains local. Hella [7] proved that invariant first-order formulas that do not
only use an order, but also addition and multiplication, are not local. On the other hand,
we conjecture that just adding order and addition does not destroy locality.
However, the fact that invariant formulas with built-in addition and multiplication
are not local is more relevant to complexity theory, since first-order logic with built-in
addition and multiplication captures uniform AC 0 . One way to apply locality techniques
to complexity theoretic questions in spite of Hella's non-locality result is to
weaken the notion of locality. For example, it is conceivable that all invariant AC 0 or
even -queries are local in the sense that if two points of a structure of size n have
isomorphic neighborhoods of radius O(log n), then they are indistinguishable.
This would still be sufficient to separate LOGSPACE from these classes.



--R

Foundations of Databases.
Extended order-generic queries
Local properties of query languages.
Finite Model Theory.
On local and non-local properties
Private communication.
Private communication.
Notions of locality and their logical characterizations over finite models
On forms of locality over finite models.
On counting and local properties.
Graph connectivity and monadic NP.
--TR
Logics with counting and local properties
Foundations of Databases
Local Properties of Query Languages
Deciding First-Order Properties of Locally Tree-Decomposalbe Graphs
On the Forms of Locality over Finite Models
Logics with Aggregate Operators
Logics with Counting, Auxiliary Relations, and Lower Bounds for Invariant Queries

--CTR
David Gross-Amblard, Query-preserving watermarking of relational databases and XML documents, Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.191-201, June 09-11, 2003, San Diego, California
Leonid Libkin, Expressive power of SQL, Theoretical Computer Science, v.296 n.3, p.379-404, 14 March
Leonid Libkin, Logics capturing local properties, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.135-153, Jan. 2001
Guozhu Dong , Leonid Libkin , Limsoon Wong, Incremental recomputation in local languages, Information and Computation, v.181 n.2, p.88-98, March 15,
Nicole Schweikardt, On the expressive power of monadic least fixed point logic, Theoretical Computer Science, v.350 n.2, p.325-344, 7 February 2006
Lane A. Hemaspaandra, SIGACT news complexity theory column 49, ACM SIGACT News, v.36 n.4, December 2005
logics;first-order logic;ordered structures;locality