An Existential Locality Theorem
Martin Grohe, Stefan Wöhrle
Gaifman's locality theorem (1981) states that every first-order sentence
is equivalent to a Boolean combination of sentences saying: There exist
elements a_1,...,a_k that are far apart from one another, and each a_i
satisfies some local condition described by a first-order formula. We
prove that every existential first-order sentence is equivalent to a
positive Boolean combination of sentences saying: There exist elements
a_1,...,a_k that are far apart from one another, and each a_i satisfies
some local condition described by an existential first-order formula.
We then show how a variant of this existential locality theorem can
be applied to evaluate existential first-order sentences in certain
finite structures, such as planar graphs or graphs of bounded degree,
improving a result of Frick and Grohe (1999) for the special case of
existential sentences.