Shrinking Games and Local Formulas

H. Jerome Keisler

Dept. of Mathematics, University of Wisconsin, Madison WI 53706

Wafik Boulos Lotfallah

Dept. of Engineering. Math. and Physics, Cairo University, Cairo, Egypt 11451

Abstract

Gaifman’s normal form theorem showed that every first order sentence of quantifier rank n is equivalent to a Boolean combination of “scattered local sentences”, where the local neighborhoods have radius at most 7^{n−1}. This bound was improved by Lifsches and Shelah to 3 · 4^{n−1}. We use Ehrenfeucht-Fraïssé type games with a “shrinking horizon” to get a spectrum of normal form theorems of the Gaifman type, depending on the rate of shrinking. This spectrum includes the result of Lifsches and Shelah, with a more easily understood proof and with the bound on the radius improved to 4^{n−1}. We also obtain bounds for a normal form theorem of Schwentick and Barthelmann.

Key words: Ehrenfeucht-Fraïssé games, finite model theory, local formulas, quantifier rank

1 Introduction

Gaifman [Gai82] proved a normal form theorem for first order sentences using formulas which are local with respect to the path length connecting elements by atomic formulas. This theorem states that every first order sentence of quantifier rank n is equivalent to a finite Boolean combinations of “scattered local sentences” saying that there exist disjoint local neighborhoods of some first order type, with radius at most 7^{n−1}. This bound on the radius was improved by Lifsches and Shelah [LS96] to 3 · 4^{n−1}.

Email addresses: keisler@math.wisc.edu (H. Jerome Keisler), lotfalla@uwalumni.com (Wafik Boulos Lotfallah). 1 Supported in part by the Vilas Trust Fund

Preprint submitted to Elsevier Science 8 August 2003

Since the local neighborhoods are disjoint in Gaifman’s theorem, the centers of the neighborhoods are separated by at least twice the radius. It is natural to ask whether there are other normal form theorems with different relationships between the radii of the neighborhoods and the distances separating their centers.

In this paper we use Ehrenfeucht-Fraïssé type games with a shrinking horizon between two relational structures to obtain a spectrum of normal form theorems of the Gaifman type, which roughly correspond to the rate of shrinking. Taking one particular level of this spectrum, we get a more easily understood proof of the result of Lifsches and Shelah, while slightly improving the bound to 4^{n−1}. We also apply the shrinking games to get bounds for another normal form theorem which was proved by Schwentick and Barthelmann [SB99] as a consequence of Gaifman’s theorem.

Shrinking Ehrenfeucht-Fraïssé type games were also applied in another direction by Schwentick [Sch96].

2 Basic Definitions

We fix a finite relational vocabulary ν. A, B will always stand for ν-structures, a, b will always stand for finite sequences in A, B, respectively, and (A, a), (B, b) will stand for the structures with distinguished elements. A ≅ B means that the structures A and B are isomorphic. Abusing notation we let A denote either the structure or its universe.

The shrinking game to be introduced here shares the following features with the basic Ehrenfeucht-Fraïssé game in [Ehr61].

The game is played on two structures A and B by two players, Spoiler and Duplicator. Roughly speaking, Spoiler tries to prove that the two structures look different, while Duplicator tries to prove that they look alike. By a position we will mean a triple ((A, a), (B, b), n) where |a| = |b| < ω, and n is a natural number which represents the number of rounds yet to be played.

When n = 0 the game ends, and ((A, a), (B, b), 0) is a winning position for Duplicator if and only if (A, a) and (B, b) satisfy the same atomic formulas.

When n > 0, the ordinary Ehrenfeucht-Fraïssé game proceeds from the position ((A, a), (B, b), n) according to the following rules:

• Spoiler chooses an element c in one structure (say A).

• Duplicator chooses an element d in the other structure (B).

• The game continues from the new position ((A, a, c), (B, b, d), n − 1).

We write (A, a) ≡_{n} (B, b) if Duplicator has a winning strategy in the Ehrenfeucht-Fraïssé game starting from the position ((A, a), (B, b), n). We say that (A, a) and (B, b) agree on a set of (first order) formulas F, in symbols (A, a) ≡_{F} (B, b), if for every formula ψ(x) ∈ F, A ⊧ ψ(a) if and only if B ⊧ ψ(b). The importance of the Ehrenfeucht-Fraïssé game stems from the basic result that (A, a) ≡_{n} (B, b) if and only if (A, a) and (B, b) agree on all formulas of quantifier rank at most n.

We say that a formula φ is Boolean over a set of formulas F if φ is logically equivalent to a finite Boolean combination of formulas from F which have the same free variables as φ. Some of the results in this paper will show that one equivalence relation implies another. In view of the following simple lemma, results of this kind often lead to normal form theorems which say that every formula in one set is Boolean over another set.

Lemma 2.1 Let F and G be two sets of formulas with the same free variables. Suppose that whenever (A, a) ≡_{F} (B, b) we have (A, a) ≡_{G} (B, b). Then every formula in G is Boolean over F.

3 The Shrinking Game

We first need some notation concerning neighborhoods and distances in relational structures.

The Gaifman graph over a structure A is the graph over the universe of A whose edges are the pairs (a, a′) of elements of A such that both a and a′ occur in some atomic formula which holds in A. The Gaifman graph over A is undirected and contains all pairs (a, a).

If a, c ∈ A we let δ(a, c) be the natural distance between a and c in the Gaifman graph over A, i.e. the length of the shortest path connecting a and c. Thus δ(a, a) = 0, and δ(a, c) = 1 if and only if a ≠ c and there is an edge connecting a and c. Clearly δ is a metric (possibly taking the value ∞) on A. For sequences a, c in A we also define δ(a, c) to be the minimum distance between elements of a and elements of c. The degree of an element a ∈ A is the degree of a in the Gaifman graph, that is, the number of elements at distance 1 from a.

If each predicate symbol of ν is at most binary, then δ(x, y) = 1 can be defined by a quantifier-free formula. This leads to a simple and natural relationship between quantifier rank and the Gaifman graph. For example, it implies that for any s ≤ 2^{n}, the inequality δ(x, y) ≤ s can be expressed by a formula of quantifier rank at most n.

Things are not as nice if the largest arity of a relation symbol in ν is d > 2. In that case, d − 2 quantifiers are needed to express δ(x, y) = 1, and an extra d − 2 quantifiers are also needed to express larger distances.

If a = ⟨a_{1}, …, a_{k}⟩ are k elements in A and k > 0, r ≥ 0, the r-neighborhood N _{r}^{A}(a) around a is the substructure of (A, a) whose universe is the set of elements at distance ≤ r from one of a_{1}, …, a_{k}. In the case k = 1, i.e. a = ⟨a⟩, the r-neighborhood N _{r}^{A}(a) is called simple, and the element a is called the center of the neighborhood. When k = 0, i.e. a is the empty sequence, we define N _{r}^{A}(a) to be the whole structure A.

A set C ⊆ A is called s-scattered if δ(c, d) > s for any pair of distinct elements c, d ∈ C. The cardinality |C| will be called the width of the sscattered set C.

Definition 3.1 For the remainder of this paper, we fix a sequence ⟨s_{n} : n ≥ 0⟩ of natural numbers called the scattering parameters, and we define another sequence ⟨r_{n} : n ≥ 0⟩, called the local radii, as follows:

r_{0} = 1, r_{n+1} = 2r_{n} + s_{n}.

Roughly speaking, we will decompose a structure A into simple neighborhoods of radius r_{n} whose centers are s_{n}-scattered. A straightforward induction shows that

r_{n+1} = 2^{n+1} + ∑_{i=0}^{n} 2^{n−i}s_{i}.

A simple example of a scattering parameter is base t exponential growth, where t is a fixed natural number, and for all m < n,

r_{m} = t^{m} and s_{m} = (t − 2)r_{m}.

We now define the shrinking game, which depends on the underlying sequence s_{n} of scattering parameters. The notation (A, a) ≈_{n} (B, b) will mean that Duplicator has a winning strategy in the shrinking game at the position ((A, a), (B, b), n). We define the possible moves and the relation ≈_{n} by a simultaneous induction on n.

The shrinking game: The winning positions for Duplicator in the shrinking game are the same as in the Ehrenfeucht-Fraïssé game. The rules proceeding from the position ((A, a), (B, b), n), n > 0 are as follows. Spoiler chooses one structure (say A) and an integer m < n, and makes either a local move or a scattered move.

Local move:

• Spoiler chooses an element c ∈ N _{r_{m}+s_{m}}^{A}(a).

• Duplicator chooses an element d ∈ N _{r_{m}+s_{m}}^{B}(b).

• The new position is ((A, a, c), (B, b, d), m).

Scattered move:

• Spoiler chooses a nonempty finite s_{m}-scattered set C ⊆ N _{r_{m}}^{A}(a) such that (A, c) ≈_{m} (A, e) for all c, e ∈ C, and if |a| = 0 then |C| ≤ n − m.

• Duplicator chooses an s_{m}-scattered set D ⊆ N _{r_{m}}^{B}(b) such that |D| = |C|.

• Spoiler chooses an element d ∈ D.

• Duplicator chooses an element c ∈ C.

• The new position is ((A, c), (B, d), m).

Note that Spoiler can shorten the shrinking game by choosing m < n − 1. The reason for giving Spoiler this freedom is to insure that the set of scattered moves available to Spoiler increases as n increases, as stated in the following easy lemma.

Lemma 3.2 (i) ≈_{n} is an equivalence relation for each n.

(ii) If (A, a) ≈_{n} (B, b), then (A, a) ≈_{m} (B, b) for all m ≤ n.

In the Ehrenfeucht-Fraïssé game, n is always the number of moves which remain to be played, while in the shrinking game there will be n or fewer moves to be played, depending on the choices of Spoiler.

The following lemma explains the role of the local radii r_{n}.

Lemma 3.3 Let a, c ∈ A and b, d ∈ B with |a| = |b| > 0 and |c| = |d| > 0. Suppose (A, a) ≈_{n} (B, b), (A, c) ≈_{n} (B, d), δ(a, c) > r_{n}, and δ(b, d) > r_{n}. Then (A, a, c) ≈_{n} (B, b, d).

Proof: The proof is by induction on n. The case n = 0 follows easily since r_{0} = 1. For the induction step, Duplicator has winning strategies at the positions ((A, a), (B, b), n) and ((A, c), (B, d), n). By definition one has r_{n} ≥ 2r_{m} + s_{m} for each m < n, and this is just what is needed to construct a winning strategy for Duplicator at the combined position ((A, a, c), (B, b, d), n). The details are omitted.

4 n-Quantifier Equivalence

Definition 4.1 Fix a finite sequence s = (s_{0}, …, s_{n−1}) of scattering parameters. We say that s shrinks rapidly if 2r_{m} ≤ s_{m} for all m < n.

For example, s shrinks rapidly when r_{m} = t^{m} and s_{m} = (t−2)r_{m} for some fixed t ≥ 4. Note that if s shrinks rapidly, then for each m < n, each s_{m}-scattered set contains at most one point in each simple r_{m}-neighborhood.

We assume throughout this section that s shrinks rapidly.

Theorem 4.2 For all structures A and B, A ≈_{n} B implies A ≡_{n} B.

Proof: We prove by induction that Duplicator can play the Ehrenfeucht-Fraïssé game starting from the position (A, B, n) so that for each i = 1 … n, she maintains the property

(A, a) ≈_{n−i} (B, b) (1)

after i rounds, where a, b are the elements chosen in the Ehrenfeucht-Fraïssé game.

Induction Base (i = 1): Without loss of generality let a_{1} ∈ A be chosen by Spoiler in the Ehrenfeucht-Fraïssé game. Since every local neighborhood of the empty sequence is the whole structure, this is just a local move for Spoiler in the shrinking game at the initial position (A, B, n). The winning strategy of Duplicator in the shrinking game gives a response b_{1} ∈ B such that (1) holds for i = 1.

Induction Step: Suppose that 1 ≤ i < n and (1) is true for i.

We can assume without loss of generality that Spoiler chooses a_{i+1} ∈ A in the Ehrenfeucht-Fraïssé game. Let p = n − i. Thus (1) says that Duplicator has a winning strategy in the shrinking game at the position

((A, a), (B, b), p). (2)

We distinguish between two cases.

Case a: a_{i+1} ∈ N _{r_{p−1}+s_{p−1}}^{A}(a).

Here Duplicator pretends that a_{i+1} is a local move by Spoiler in the shrinking game at position (2). Duplicator uses her winning strategy to respond with an element b_{i+1} ∈ N _{r_{p−1}+s_{p−1}}^{B}(b). This insures that (1) holds for i + 1.

Case b: a_{i+1} ∉ N _{r_{p−1}+s_{p−1}}^{A}(a).

Here Duplicator hopes to find in the structure B a duplicate d ∉ N _{r_{p−1}}^{B}(b) such that

(A, a_{i+1}) ≈_{p−1} (B, d). (3)

Then choosing b_{i+1} = d will guarantee (1) for i + 1 by Lemmas 3.2 and 3.3.

For the sake of contradiction we assume that this is not possible. So any d satisfying (3) will be inside N _{r_{p−1}}^{B}(b). Let D be an s_{p−1}-scattered set in N _{r_{p−1}}^{B}(b) of maximal width w consisting of elements d ∈ B satisfying (3). The above argument for Case a shows that D is nonempty, i.e. w ≥ 1. Since 2r_{p−1} ≤ s_{p−1}, the set D contains at most one element in each neighborhood N _{r_{p−1}}^{B}(b_{j}), so w = |D| ≤ |b| = i.

We now form a set C in A as follows. Let Spoiler choose m = p − 1 and the set D as a scattered move in the shrinking game at the position (2). Take C ⊆ N _{r_{p−1}}^{A}(a_{1}, …, a_{i}) to be the response of Duplicator in her winning strategy. Then |C| = w, and (A, c) ≈_{p−1} (B, d) ≈_{p−1} (A, a_{i+1}) for all c ∈ C, d ∈ D.

We will now consider another play of the shrinking game starting from the original position (A, B, n). By the hypothesis A ≈_{n} B, Duplicator has a winning strategy for this game. Noting that C ∪ {a_{i+1}} is s_{p−1}-scattered, we let Spoiler choose m = p − 1 and the set C ∪ {a_{i+1}} of width w + 1 as a scattered move in A. This is a legal move since w + 1 ≤ i + 1 = n − m. Duplicator must then respond with an s_{p−1}-scattered set consisting of w + 1 elements of B which satisfy (3). By assumption, all these elements must be inside N _{r_{p−1}}^{B}(b), contradicting the maximality of w.

Here is a generalization of Theorem 4.2 to structures with distinguished elements.

Corollary 4.3 If (A, a) ≈_{n} (B, b), and A ≈_{n} B, then (A, a) ≡_{n} (B, b).

Proof: The argument is exactly as in the proof of Theorem 4.2 but starting after |a| rounds.

5 Shrinking Formulas

In this section we continue to assume that s shrinks rapidly.

We will apply the shrinking games to obtain normal form theorems of the type introduced in Gaifman [Gai82] and improved by Lifsches and Shelah [LS96].

We will introduce a hierarchy of first order formulas which corresponds in a natural way to the shrinking games. This hierarchy depends on a given sequence of scattering parameters s.

Definition 5.1 The set SH_{n}(x) of shrinking formulas in x of rank at most n is defined inductively as follows.

SH_{0}(x) is the set of all quantifier free formulas in x.

For each m < n, SH_{m+1}(x) is the set of all finite Boolean combinations of formulas in SH_{m}(x) and formulas of the forms

(∃y ∈ N_{s_{m}+r_{m}}(x)) ψ(x, y), (4)

(∃y_{1}, …, y_{l} ∈ N_{r_{m}}(x)) (⋀_{i≤l} θ(y_{i}) ∧ ⋀_{i<j≤l} δ(y_{i}, y_{j}) > s_{m}) , (5)

where ψ(x, y) ∈ SH_{m}(x, y), θ(y) ∈ SH_{m}(y), and l ≤ n − m when |x| = 0.

In the case that x is empty, shrinking formulas in x are called shrinking sentences, formula (5) simplifies to

(∃y_{1}, …, y_{l}) (⋀_{i≤l} θ(y_{i}) ∧ ⋀_{i<j≤l} δ(y_{i}, y_{j}) > s_{m}) ,

and formula (4) is not needed because it is the special case of formula (5) where l = 1.

Lemma 5.2 There are only finitely many shrinking formulas in x of rank at most n, up to logical equivalence.

Proof: This follows by an easy induction on n, since the language has a finite vocabulary.

We now establish the connection between shrinking formulas and the shrinking game.

Lemma 5.3 If (A, a) and (B, b) agree on all shrinking formulas of rank at most n, then (A, a) ≈_{n} (B, b).

Proof: This is proved by induction on n. Assume the result for all m < n, and suppose Spoiler makes a scattered move, choosing m < n and an s_{m}- scattered set C ⊆ N _{r_{m}}^{A}(a), with |C| ≤ n − m if |a| = 0. Then all the c ∈ C belong to the same ≈_{m}-equivalence class. By inductive hypothesis, there is a formula θ(y) ∈ SH_{m}(y) which defines this equivalence class. Then (A, a) satisfies the formula (5) in Definition 5.1 with l = |C|. This formula belongs to SH_{n}(x), and thus is also satisfied by (B, b). Therefore Duplicator has a winning response.

The argument is similar when Spoiler makes a local move, so Duplicator has a winning strategy for the shrinking game.

We now put our results together to get a normal form theorem.

Theorem 5.4 If A, B agree on all shrinking sentences of rank at most n, then A ≡_{n} B.

Proof: By Theorem 4.2 and Lemma 5.3.

To get normal form theorems of the Gaifman type, we examine the locality properties of shrinking formulas.

Definition 5.5 By an s-scattered r-local sentence of width l we mean a sentence of the form

∃y_{1} ⋯ ∃y_{l} (⋀_{i≤l} θ(y_{i}) ∧ ⋀_{i<j≤l} δ(y_{i}, y_{j}) > s)

where θ(y) is r-local.

Proposition 5.6 (i) Every shrinking formula of rank at most n is (r_{n} − 1)- local.

(ii) Every shrinking sentence of rank at most n is a finite Boolean combination sentences each of which is s_{m}-scattered and (r_{m} − 1)-local for some m < n.

Proof: By induction on n, using the fact that for each m < n, (s_{m} + r_{m}) + (r_{m} − 1) ≤ r_{n} − 1.

We can now state a normal form theorem of the Gaifman type.

Theorem 5.7 Fix a scattering sequence s which shrinks rapidly. Then each first order sentence of quantifier rank at most n is logically equivalent to a finite Boolean combination of sentences each of which is s_{m}-scattered and (r_{m} − 1)- local of width at most n − m, for some m < n.

In the case that r_{m} = 4^{m}, we get the result of Lifsches and Shelah [LS96] with an improved bound on the radius.

Corollary 5.8 Every first order sentence of quantifier rank at most n is logically equivalent to a finite Boolean combination of sentences each of which is 2 · 4^{m}-scattered and (4^{m} − 1)-local of width at most n − m, for some m < n.

Proof: Take r_{m} = 4^{m} and s_{m} = 2r_{m} in Theorem 5.7.

By examining the proofs, one can readily extend the normal form results in this section from sentences to formulas. We will leave these extensions to the reader.

Finally, we give an upper bound for the quantifier rank of the scattered local sentences in Theorem 5.7.

Theorem 5.9 Let d be the least upper bound of 2 and the maximum number of arguments of the relation symbols of the vocabulary ν. In Theorem 5.7, the local formulas inside the s_{m}-scattered (r_{m} − 1)-local sentences can be taken to have quantifier rank at most log_{2}(r_{m}) + d − 1.

In the case r_{m} = 4^{m}, the local formulas inside can be taken to have quantifier rank at most 2m + d − 1.

Proof: One proves by induction on n that each shrinking formula in x of rank n has quantifier rank at most |x| + log_{2}(r_{n}) + d − 2. To do this, a bound is needed on the quantifier rank of the distance inequality δ(x, y) ≤ r. In the case d = 2, this inequality is expressible by a first order formula of quantifier rank log_{2}(r). In the case d > 2, it is expressible by a first order formula of quantifier rank log_{2}(r) + d − 2. The remaining details are left to the reader.

6 The Schwentick-Barthelmann Normal Form

In this section we continue to assume that s shrinks rapidly.

In [SB99] Schwentick and Barthelmann modified Gaifman’s normal form by proving that every first order sentence is logically equivalent to a sentence of the form ∃x_{1} … ∃x_{l}∀yφ(x, y) where φ is a first order local formula around y. We will use the shrinking game to give another proof of this fact which makes it easier to keep track of width and locality bounds in the normal form.

Theorem 6.1 Let n > 0, r = n · 4^{n}, q = log(r) + d − 1. Suppose that every sentence of the form

∃x_{1} … ∃x_{l}∀yφ(x, y) (6)

which holds in A holds in B, where l ≤ n and φ is a first order local formula around y of radius at most r and quantifier rank at most q. Then A ≈_{n} B.

Proof: The hypotheses say that Duplicator has a winning strategy in the following one-sided game, where Spoiler must start in A:

• Spoiler chooses a tuple a in A of width ≤ n.

• Duplicator chooses b in B with |b| = |a|.

• Spoiler chooses d ∈ B.

• Duplicator chooses c ∈ A.

• The game proceeds with an ordinary Ehrenfeucht-Fraïssé game from

((N _{r}^{A}(c), a, c), (N _{r}^{B}(d), b, d), q).

Using arguments like those in the preceding sections of this paper, one can now show that Duplicator has a winning strategy in the shrinking game.

Corollary 6.2 Every first order sentence of quantifier rank n is logically equivalent to a finite conjunction of sentences of the form (6) in Theorem 6.1.

7 Narrow Sentences

For an arbitrary scattering sequence s, we obtain a normal form theorem for sentences in which there is a uniform bound on the size of an s_{m}-scattered set in each r_{m} neighborhood.

Definition 7.1 A first order sentence φ is s-narrow if there exists a finite bound k such that for each m < n, φ logically implies that for all x, every s_{m}-scattered set in N^{r_{m}}(x) has width at most k.

Note that if s shrinks rapidly, then every sentence is s-narrow with bound k = 1. In the next theorem, the interesting case is where s does not shrink rapidly.

Theorem 7.2 Fix a scattering sequence s. Let φ be an s-narrow sentence with bound k. Then each first order sentence of quantifier rank at most n is φequivalent to a finite Boolean combination of first order s_{m}-scattered (r_{m} − 1)- local sentences of width at most k(n − m), for m < n.

We omit the proof, which is a direct generalization of the proof of Theorem 5.7.

8 Conclusion

We introduced a shrinking Ehrenfeucht-Fraïssé game, in which the players move in neighborhoods whose radii shrink at a rate which depends on a sequence s of scattering parameters. The main result shows that if s shrinks rapidly and Duplicator has a winning strategy for the n-round shrinking game on two structures, then Duplicator has a winning strategy for the n-round Ehrenfeucht-Fraïssé game.

This leads, as a special case, to a more easily understood proof of a Gaifman type normal form theorem of Lifsches and Shelah, with a slightly improved bound on the local radius. The shrinking game is also used to obtain bounds for a normal form theorem of Schwentick and Barthelmann showing that each first order sentence is equivalent to a sentence of the form ∃x_{1} ⋯ ∃x_{l}∀yφ(x, y) where φ(x, y) is local around y.

For an arbitrary scattering sequence s, a spectrum of normal form theorems is obtained for s-narrow sentences. The method gives bounds on the radius of the local neighborhoods, the number of local neighborhoods and distance between them, and on the quantifier rank of the scattered local sentences.

References:

[Ehr61] A. Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fund. Math., vol. 49 (1961), pp. 129-141.

[Gai82] H. Gaifman, On local and nonlocal properties, J. Stern, editor, Logic Colloquium ’81, North Holland, Amsterdam (1982), pp. 105-135.

[Lib97] L. Libkin, On the forms of locality over finite models, In Proc. 12th IEEE Symp. on Logic in Computer Science (1997).

[Lib00] L. Libkin, On counting logics and local properties, In ACM TOCL, vol. 1 (1) (2000).

[LS96] S. Lifsches and S. Shelah, Distorted sums of models, Publication #603, Shelah’s Archive.

[Sch96] T. Schwentick, On winning Ehrenfeucht games and monadic NP, Annals of Pure and Applied Logic, vol. 79 (1996), pp. 61-92.

[SB99] T. Schwentick and K. Barthelmann, Local normal forms for first-order logic with applications to games and automata, Discrete Math. Theor. Comput. Sci., vol. 3 (1999), no. 3, pp. 109-124 (electronic).