The size of a formula as a measure of complexity

We introduce a refinement of the usual Ehrenfeucht-Fra\"{\i}ss\'e game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure the size formulas needed for expressing a given property. We will give two versions of the game: the first version characterizes the size of formulas in propositional logic, and the second version works for first-order predicate logic.


Introduction
We propose a refinement of the usual Ehrenfeucht-Fraïssé game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure not only quantifier rank but also lengths of conjunctions and disjunctions needed for expressing a given property. Our game is similar to the game in [1] and in [5].
The most common measure of complexity of a first order sentence is its quantifier rank, and the method of Ehrenfeucht-Fraïssé games can be successfully used to prove lower bound results for this measure of complexity. However, the number of non-equivalent first order formulas of quantifier rank n is an exponential tower of height n with a polynomial depending on the vocabulary on the top. Thus we are not very close to knowing the formula if we merely know its quantifier rank. In this paper we measure complexity in terms of the number of symbols in the formula. The advantage of our measure is that there are only 2 P (n) non-equivalent formulas with n symbols, where P (x) is a polynomial depending on the vocabulary.
Let us consider the question of the complexity of deciding whether a binary string s 1 s 2 . . . s n = 10110010...01 (1) has a certain pattern. One approach to this is circuit complexity. For example, it is proved in [3] that constant depth circuits cannot decide the parity of (1), i.e. the question whether (1) has an even number of ones. Another approach is computational complexity, where the parity of (1) is easily decided in linear time. In so called descriptive complexity the question is posed, what is the logical complexity of the simplest formula in a given logic that expresses the property of (1) in question, for example parity. Concerning this type of problems, it was proved in [2] that the question whether a set R of n + 1-sequences (a 1 , . . . , a n+1 ) from a finite set {1, . . . , m} has an even cardinality cannot be expressed in existential second order logic, where the second order variables range over ≤ n-ary relations, that is, there is no sentence φ of such existential second order logic with the property that the structure ({1, . . . , m}, R) satisfies φ if and only if R has even cardinality. Let us return to (1). A natural setup of using logic to study the question of complexity of finding patterns in (1) is to use the propositional logic with propositional symbols p 1 , p 2 , . . . , p n with the meaning p i is true if and only if s i = 1.
Propositional logic gives rise to a variety of complexity measures. We focus here on the simplest of them, namely the number of occurrences of propositional symbols in a formula. Up to a constant factor this is the same as the number of symbols, that is, the length of the formula. The parity of (1) is naturally expressed by the propositional formula where which gives the upper bound 1 2 n2 n to the size of the smallest formula expressing parity. However, there is a shorter formula ψ defined as follows: ψ = φ 1,n , where for 1 ≤ i < j ≤ n and k = ⌊ i+j 2 ⌋ φ i,j = (φ i,k ∧ φ k+1,j ) ∨ (¬φ i,k ∧ ¬φ k+1,j ) and This gives (up to a constant factor) the upper bound n 2 for the shortest propositional formula expressing parity 1 . Krapchenko (see [6, p 258]) has proved in 1971 that this is optimal. We prove below the same result using our refinement of the Ehrenfeucht-Fraïssé game. For a slightly different complexity question, suppose we have n unary predicates: P 1 (x), . . . , P n (x).
We ask what is the length of the shortest formula in first order logic with the unary predicates (7) that expresses the property that every Boolean combination of the predicates is non-empty. This property can be written as the existential sentence: where, as above in (6), P A i (x) = P i (x) if i ∈ A, and P A i (x) = ¬P i (x) if i ∈ A. This gives the upper bound (n + 1)2 n to the size of the smallest sentence expressing the given property (we define the size of a formula to be the total number of atomic subformulas and quantifiers occurring in it). In Section 5, we show that this is optimal for existential sentences. If we give up existential sentences and allow a quantifier alternation, we have a smaller sentence φ defined as follows: where addition i + 1 is to be calculated modulo n. The size of φ is only 8n + 4, so this is really optimal (up to a constant factor) because we cannot have such a φ without mentioning each P i at least once.
In our final application, we consider the minimal size of a first-order sentence expressing that the length of a linear order is at least n. It is well known that this can be expressed by a sentence with quantifier rank ⌈log n⌉ + 1. Such a sentence φ n can be obtained as follows: define first recursively formulas θ k (x, y) by letting θ 2 (x, y) := x < y and θ k (x, y) := ∃z(θ l (x, z) ∧ θ m (z, y)), where l = ⌊k/2⌋ + 1 and m = ⌈k/2⌉, for k > 2. Thus, θ k (x, y) says that there are at least k elements in the interval [x, y]. Then φ n can be defined as ∃x∃yθ n (x, y).
Clearly the size of φ n is linear in n. However, with a clever trick of recycling quantified variables it is possible to define a variant φ ′ n of φ n that has size c⌈log n⌉, where c is a small constant. Moreover, φ ′ n can be chosen to be in the 4-variable logic FO 4 (see [4], Section 5). On the other hand, Grohe and Schweikardt prove in [4] that the minimal size of an equivalent sentence in FO 3 is at least 1 2 √ n. Their proof is based on a method which is related to the game we study in this paper, but it is not formulated in a game theoretic form.

A Game for Propositional Logic
We introduce now a game for measuring how long a propositional formula has to be to express a given property of binary strings where s i ∈ {0, 1}. We denote strings by s, r, t etc. Let n be the fixed length of the strings considered. We shall discuss nonempty sets S of such strings and call them string properties. For example, S could be the set of strings (9) where the cardinality of the set {i ∈ {1, . . . , n} : s i = 1} is even. Another example is the set of strings (9) with more ones than zeros. In an extreme case S can be a singleton, e.g. the singleton constant one string {111 . . . 1}. Propositional formulas are built up from propositional symbols (3) by means of ¬, ∧ and ∨. We use Greek letters φ, ψ etc to denote propositional formulas. The concept s |= φ of a string s satisfying a propositional formula φ is defined in the usual way: Definition 1 Suppose φ is a propositional formula and S a string property. We say that φ defines S if for all strings s s ∈ S ⇐⇒ s |= φ.
We define the size w(φ) of the propositional formula φ as follows: Note that w(φ) is just the number of occurrences of propositional symbols in φ. Up to a constant factor, this is the same as the number of symbols in φ.
Note that while there are, up to logical equivalence, 2 2 n propositional formulas over the propositional symbols p 1 , . . . , p n altogether, there are for each m, up to logical equivalence, only at most 2 m · (n + 2) 2m propositional formulas φ with w(φ) ≤ m.
A natural question now is: Question: Given a string property S, what is the size of the smallest propositional formula that defines S.
We shall define a game for the study of this question. In defining the game we follow mostly [1] and to a lesser degree [5]. This game resembles the usual Ehrenfeucht-Fraïssé game for the first order logic, but also the Ehrenfeucht-Fraïssé game for the independence friendly logic, presented in [5].
In the usual Ehrenfeucht-Fraïssé game we have two structures A and B and the game is about their similarity. Player II maintains that the structures are very similar. Player I maintains that there is a difference. During the game player I picks elements from either one of the models and player II tries to find similar elements in the other model.
In the new game we do not have just two models but instead two classes of models. Player II maintains that whatever features the models in one class have all in common, some member of the other class also has. The game to be defined is able to detect very minute differences in models and is in that sense finer than the usual Ehrenfeucht game. In particular, this game can detect differences in the size of conjunctions and disjunctions needed for separating the classes of models. This is a game of perfect information and the concept of winning strategy is defined as usual. Since the rank w m decreases in each move, the game always ends in a finite number of moves. Hence the game is determined: exactly one of the players has a winning strategy in EF w (S, R).
Note that if the players have reached a position (w m , S m , R m ) in the game EF w (S, R), then the continuation of the game from that position onwards can be seen as a play of the game EF wm (S m , R m ). Thus, player I (player II) has a winning strategy in the game EF w (S, R) from position (w m , S m , R m ) onwards if an only if player I (player II, respectively) has a winning startegy in the game EF wm (S m , R m ).
We say that a propositional formula φ separates string properties S and R, in symbols (S, R) |= φ, if s |= φ for all s ∈ S and r |= φ for all r ∈ R. (1) w Player I has a winning strategy in the game EF w (S, R).
(2) w There is a propositional formula φ of size ≤ w such that (S, R) |= φ.
Proof. We prove the equivalence of (1) w and (2) w by induction on w. Consider first the case w = 1. By Definition 2, there are no moves in the game EF 1 (S, R), and player I wins if and only if there is a proposition symbol p i such that either (S, R) |= p i , or (S, R) |= ¬p i . Since w(p i ) = w(¬p i ) = 1, we have (1) 1 =⇒ (2) 1 . On the other hand, if w(φ) ≤ 1, then φ is, up to logical equivalence, either a proposition symbol, or the negation of a proposition symbol. Thus, (2) 1 implies (1) 1 .
Let us then consider the case w > 1, and assume (1) v ⇐⇒ (2) v for all v < w as an induction hypothesis. To prove (1) w ⇐⇒ (2) w , assume first that player I has a winning strategy in the game EF w (S, R). We have the following two cases according to the type of the first move in the winning strategy of player I.
Case 1: Player I makes a left splitting move by choosing u, v, C and D such that 1 ≤ u, v < w, w = u + v and S = C ∪ D. Since this move is given by a winning strategy, player I has a winning strategy in both of the games EF u (C, R) and EF v (D, R). By induction hypothesis, there are formulas ψ and θ such that w(ψ) ≤ u, w(θ) ≤ v, (C, R) |= ψ and (D, R) |= θ. Thus, s |= ψ for all s ∈ C and s |= θ for all s ∈ D, whence s |= ψ ∨ θ for all s ∈ S. On the other hand, for all r ∈ R, r |= ψ and r |= θ, whence consequently Case 2: Player I makes a right splitting move by choosing u, v, C and D such that 1 ≤ u, v < w, w = u + v and R = C ∪ D. Since this move is given by a winning strategy, player I has a winning strategy in both of the games EF u (S, C) and EF v (S, D). By induction hypothesis there are formulas ψ and θ such that w(ψ) ≤ u, w(θ) ≤ v, (S, C) |= ψ and (S, D) |= θ. Thus, for all s ∈ S, s |= ψ and s |= θ, whence s |= ψ ∧ θ. On the other hand, r |= ψ for all r ∈ C and r |= θ for all r ∈ D, whence r |= ψ ∧ θ for all r ∈ R. It follows To prove the converse implication (2) w =⇒ (1) w , assume that there is a formula φ of size ≤ w such that (S, R) |= φ. We show that then player I has a winning strategy in the game EF w (S, R). We assume without loss of generality that φ is in negation normal form 2 . The strategy depends on φ as follows.
Case 1: φ is a proposition symbol or the negation of a proposition symbol. Then by the definition of the game EF w , player I wins without making any moves.
Case 2: φ is ψ ∨ θ. Let C be the set of strings s ∈ S such that s |= ψ, and let D be the set of strings s ∈ S such that s |= θ. Since s |= φ for every s ∈ S, we have S = C ∪ D. Moreover, since r |= φ for every r ∈ R, we have (C, R) |= ψ and (D, R) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (C, R) and EF v (D, R). Thus, using w = u + v, S = C ∪ D as his first move and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (S, R).
Let C be the set of strings r ∈ R such that r |= ψ, and let D be the set of strings r ∈ R such that s |= θ. Since r |= φ for every r ∈ R, we have R = C ∪ D. Moreover, since s |= φ for every s ∈ S, we have (S, C) |= ψ and (S, D) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (S, C) and EF v (S, D). Thus, using w = u + v, R = C ∪ D in his first move, and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (S, R). Q.E.D.
Corollary 4 Suppose K is a string property. Then the following conditions are equivalent: (2) Player I has a winning strategy in the game EF w (S, R) for all S and R such that S ⊆ K and R ∩ K = ∅.
Proof. Suppose K is defined by φ of size ≤ w. Let S and R be given so that S ⊆ K and R ∩ K = ∅. Thus every model in S satisfies φ and no model in R does, whence (S, R) |= φ. By Theorem 3, player I has a winning strategy in EF w (S, R). For the converse, suppose player I has a winning strategy in EF w (S, R) for all (S, R) with S ⊆ K and R ∩ K. This holds in particular if S is K and R is the complement of K. Thus for this choice of S and R we have We get the following method for showing that a string property K is not definable by a propositional formula of size ≤ w: We find classes S and R such that 3. Player II has a winning strategy in EF w (S, R).

The Propositional Complexity of Parity
We shall now prove that the parity of a binary string of n bits cannot be expressed with a propositional formula smaller than n 2 . The result has been proved in [6] with a method which is very similar to ours, even if it does not explicitly use games. We present the proof as an example of the use of our game.
Suppose S and R are disjoint sets of binary strings of length n. Let The density of the pair (S, R) is defined to be the pair Proof. Suppose s > 1 and i ∈ {1, . . . , n}. Then there are f ∈ S and , then there is a string in R satisfying p i (¬p i , respectively). It follows that neither p i , nor ¬p i separates the sets S and R. In As above, we conclude that neither p i , nor ¬p i separates the sets S and R. Q.E.D.
Proof. We prove (a); the proof of (b) is similar. Clearly r 0 + r 1 = r and r 0 s 0 + r 1 s 1 = r s . Since the harmonic mean is never greater than the arithmetic mean 3 , we have and the claim follows. Q.E.D.
Lemma 7 Suppose D(S, R) = (s, r) and w < sr. Then player II has a winning strategy in EF w (S, R).
Proof. The proof is by induction on w. In the case w = 1, the assumption w < sr implies that either s > 1 or r > 1. By Lemma 5, there is no proposition symbol p i such that (S, R) |= p i or (S, R) |= ¬p i . Since the game EF 1 (S, R) ends in its initial position (1, S, R), this means that player II automatically wins this game. Assume then that w > 1. Using Lemma 5 again, we see that player I does not win the game EF w (S, R) without making moves. Suppose then that player I makes a left splitting move w = u + v and S = C ∪ D. Let S 0 ⊆ C and S 1 ⊆ D be sets such that S = S 0 ∪ S 1 and S 0 ∩ S 1 = ∅.
Let D(S 0 , R) = (s 0 , r 0 ) and D(S 1 , R) = (s 1 , r 1 ). Then by Lemma 6(a), contrary to the assumption. If s 0 r 0 > u, then by induction hypothesis, player II has a winning strategy in the game EF u (S 0 , R), whence, a fortiori, he has a winning strategy in EF u (C, R). Otherwise, s 1 r 1 > v, and by the same argument, player II has a winning strategy in the game EF v (D, R). Thus, in any case, player II can make his move in such a way that he is guaranteed to win.
The case of a right splitting move w = u + v and R = C ∪ D is proved in the same way by using Lemma 6(b). Q.E.D.
We are now ready to prove the promised lower bound for parity of binary strings.
Corollary 8 ( [6]) If φ is a propositional formula expressing the parity of strings s ∈ {0, 1} n , then the size of φ is at least n 2 .
Proof. Let S be the set of all strings f ∈ {0, 1} n such that |{i : f i = 1}| is even, and let R be the complement of S. Thus, |S| = |R| = 2 n−1 . Furthemore, for each string f ∈ S, there are n different strings g ∈ {0, 1} n such that |{i : f i = g i }| = 1, and all these strings are in R. Thus, we have |E| = 2 n−1 n, and consequently D(S, R) = (n, n). By Lemma 7, player II has a winning strategy in the game EF w (S, R) whenever w < n 2 , and we conclude that S is not definable by any formula of size less than n 2 . Q.E.D.
As noted in the introduction, the parity of strings in {0, 1} n can be expressed by a formula of size at most (n + 1) 2 . Thus, the lower bound n 2 cannot be essentially improved.

A Game for Predicate Logic
We shall next define a game that can be used for measuring the size of a first-order sentence needed for expressing properties of models. For the sake of simplicity, we will only consider models with relational vocabulary.
We need to fix some notation first. The universe of a model A is denoted by A, of B by B, etc. We use x j , j ∈ N, to denote variables. A variable assignment for a model A is a finite partial mapping α : N → A. The finite domain of α is denoted by dom(α). If φ is a formula, then (A, α) |= φ means that the assignment α satisfies the formula φ in the model A. For this to be meaningful the domain of the assignment α has to include all the j for which the variable x j is free in φ.
We shall discuss classes A of structures (A, α), where A is a model and α is an assignment. We assume that whenever (A, α), (B, β) ∈ A, then A and B have the same vocabulary, and α and β have the same domain, which we denote by dom(A). If α is an assignment on A, a ∈ A and j ∈ N, then α(a/j) is the assignment that maps j to a and agrees with α otherwise. If F is a choice function on A, that is, F is a function defined on A such that This is a game of perfect information and the concept of winning strategy is defined as usual. The game is determined by the Gale-Stewart theorem.
We define the size w(φ) of the formula φ of predicate logic as follows: Note that there are for each w, up to logical equivalence, only finitely many formulas of size ≤ w. (1) w Player I has a winning strategy in the game EF w (A, B).
(2) w There is a formula φ of predicate logic of size ≤ w such that (A, B) |= φ.
Proof. We prove the equivalence of (1) w and (2) w by induction on w. Consider first the case w = 1. By Definition 9, there are no moves in the game EF 1 (A, B), and player I wins if and only if there is an atomic formula φ such that either (A, B) |= φ or (A, B) |= ¬φ. Since w(φ) = w(¬φ) = 1, we have (1) 1 =⇒ (2) 1 . On the other hand, if w(φ) = 1, then φ is, up to logical equivalence, either an atomic formula, or the negation of an atomic formula. Thus, (2) 1 implies (1) 1 .
Let us then consider the case w > 1, and assume (1) v ⇐⇒ (2) v for all v < w as an induction hypothesis. To prove (1) w ⇐⇒ (2) w , assume first that player I has a winning strategy in the game EF w (A, B). We have the following four cases according to the type of the first move in the winning strategy of player I. Case 3: Player I makes a left supplementing move by choosing a natural number j and a choice function F for A. The next position in the game is then (w − 1, A(F/j), B(⋆/j)). Since this move is given by a winning strategy, player I has a winning strategy in the game EF w−1 (A(F/j), B(⋆/j)). By induction hypothesis there is a formula ψ such that w(ψ) ≤ w − 1 and (A(F/j), B(⋆/j)) |= ψ. Let φ be the formula ∃x j ψ. Then w(φ) = w(ψ) + 1 ≤ w, and it suffices to show that (A, B) |= φ. Note first that for all (A, α) ∈ A, (A, α(a/j)) |= ψ, where a = F ((A, α)). Thus we have (A, α) |= φ for all (A, α) ∈ A. On the other hand, for all (B, β) ∈ B and all b ∈ B, we have (B, β(b/j)) |= ψ, whence (B, β) |= φ.
Case 4: Player I makes a right supplementing move by choosing a natural number j and a choice function F for B. The next position in the game is then (w − 1, A(⋆/j), B(F/j)). Since this move is given by a winning strategy, player I has a winning strategy in the game EF w−1 (A(⋆/j), B(F/j)). By induction hypothesis there is a formula ψ such that w(ψ) ≤ w − 1 and (A(⋆/j), B(F/j)) |= ψ. Let φ be the formula ∀x j ψ. Then w(φ) = w(ψ) + 1 ≤ w, and it suffices to show that (A, B) |= φ. Note first that for all (A, α) ∈ A and all a ∈ A, we have (A, α(a/j)) |= ψ. Thus we have (A, α) |= φ for all (A, α) ∈ A. On the other hand, for all (B, β) ∈ B, (B, β(b/j)) |= ψ, where b = F ((B, β)). Thus we have (B, β) |= φ for all (B, β) ∈ B.
To prove the converse implication (2) w =⇒ (1) w , assume that there is a formula φ of size ≤ w such that (A, B) |= φ. We show that then player I has a winning strategy in the game EF w (A, B). As in the case of propositional logic, we can assume without loss of generality that φ is in negation normal form. The strategy of player I depends on φ as follows.
Case 1: φ is an atomic formula or the negation of an atomic formula. Then by Definition 9, player I wins the game EF w (A, B) without making any moves.
Case 2: φ is ψ ∨ θ. Let C be the class of structures (A, α) ∈ A such that (A, α) |= ψ, and let D be the class of structures (A, α) ∈ A such that (A, α) |= θ. Since (A, α) |= φ for every (A, α) ∈ A, we have A = C ∪ D. Moreover, since (B, β) |= φ for every (B, β) ∈ B, we have (C, B) |= ψ and (D, B) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (C, B) and EF v (D, B). Thus, using w = u + v, A = C ∪ D as his first move and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (A, B).
Corollary 11 Suppose K is a class of models of the same vocabulary. Then the following conditions are equivalent: (1) K is the class of models of a first order sentence φ of size ≤ w.
(2) Player I has a winning strategy in the game EF w (A, B) for all A and B such that A ⊆ K and B ∩ K = ∅.
Proof. Suppose K is the class of models of φ and w(φ) ≤ w. Let A and B be given so that We get the following method for showing that a model class K is not definable by a first order sentence of size ≤ w: We find classes A and B such that 3. Player II has a winning strategy in EF w (A, B).

A Game for Existential Formulas
The game EF w can be used for solving questions of the type Given a property of P models, what is the size of the smallest first order formula that defines P?
But in some applications we are interested in definability by some restricted type of of formulas, rather than arbitrary first order formulas. For example, if a property P of models is known to be definable by an existential formula, it is natural to ask, what is the size of the smallest existential formula defining P. We will now define a variant of the game EF w that can be used in studying this question.
Here we say that a first order formula is existential if it is in negation normal form, and it does not contain any universal quantifiers. In other words, existential formulas are built from atomic formulas and negations of atomic formulas by using the connectives ∨, ∧ and the quantifier ∃.
Intuitively, in the definition of the game EF w , left and right splitting moves correspond to the connectives ∨ and ∧, while left and right supplementing moves correspond to the quantifiers ∃ and ∀. Thus, we obtain a game for existential formulas simply by dropping right supplementing moves. (1) w Player I has a winning strategy in the game EF ∃ w (A, B).

Definition 12 Let
(2) w There is an existential formula φ of size ≤ w such that (A, B) |= φ.
Proof. The claim is proved by a straightforward adaptation of the proof of Lemma 10. In the proof of (1) w =⇒ (2) w it suffices to note that omitting Case 4, the formula φ separating the classes A and B will always be existential. Similarly, in the proof of the opposite implication, Case 5 never occurs as the separating formula φ is existential, whence the winning strategy of player I does not use right supplementing moves. Q.E.D.
As in the case of the full first order game EF w , we get again a method for showing that a model class K is not definable by an existential formula of size ≤ w: We find classes A and B such that

The Existential Complexity of Non-Emptiness of Boolean Combinations
We observed in the introduction that non-emptiness of all Boolean combinations of n unary predicates can be defined with a sentence of size 8n + 4 if a quantifier alternation is allowed. If only existential sentences are allowed, this can be expressed with a sentence of size (n + 1)2 n . We use now our game for existential formulas to show that (n + 1)2 n is the best possible value. For each binary string s ∈ {0, 1} n , let B s be the {P 1 , . . . , P n }-structure such that for each r ∈ {0, 1} n , the Boolean combination of P Bs 1 , . . . , P Bs n corresponding to r contains exactly two elements, b r and c r , except that the combination corresponding to s is empty. Furthermore, let A be the structure in which each Boolean combination contains exactly one element; let a r be the element in the Boolean combination corresponding to r ∈ {0, 1} n . Let We will show that player II has a winning strategy in the existential game EF ∃ w (A 0 , B 0 ) for all w < (n + 1)2 n . Since the game is existential, in any position (u, A, B), the set A contains only one structure (A, α), where α is the variable assignment that results from the moves of player I. We say that a structure (B s , β) is flawless (with respect to α), if dom(β) = dom(α), and for all j ∈ dom(α) and all r ∈ {0, 1} n , we have Note that if a s ∈ ran(α), then there is no β such that (B s , β) is flawless. On the other hand, if a s ∈ ran(α), then there is a unique β such that (B s , β) is flawless; we denote this β by β s,α . Furthermore, we say that a structure (B s , β) is good enough (with respect to α), if it is not flawless, but dom(β) = dom(α), and (10) holds for all j ∈ dom(α) and all r = s, and there is a string t ∈ {0, 1} n with |{i : for all j ∈ dom(α). Thus, if a s ∈ ran(α), then for each t ∈ {0, 1} n with |{i : s i = t i }| = 1 there is a unique β such that (B s , β) is good enough; we denote this β by β s,t,α . Assume then, that (B s , β s,t,α ) and (B s ′ , β s ′ ,t ′ ,α ) are two distinct good enough structures in B. Let φ be an atomic formula. If φ is an identity x j = x k (with j, k ∈ dom(α)), then it follows easily from (10) and (11) that (A, α) |= φ ⇐⇒ (B s , β s,t,α ) |= φ. Thus, φ does not separate A and B.
Thus, we see that if B does not contain a flawless structure of the form (B r , β r,α ), then f (B ′ ) = f (B) and g(B ′ ) = g(B), whence the claim is true.
Assume finally, that there is a flawless structure (B r , β r,α ) in B. Since α ′ (j) = a r , no structure (B r , β) is flawless with respect to α ′ . On the other hand, for each t ∈ {0, 1} n with |{i : r i = t i }| = 1, there is a new good enough structure (B r , β r,α (c t /j)) = (B r , β r,t,α ′ ) in B ′ . Thus, in this case Consider now the classes A 0 and B 0 defined in the beginning of this section. Since the variable assignment in the only structure in A 0 is empty, all the 2 n structures (B s , ∅) in B 0 are flawless. Thus, M(B 0 ) = (n+1)f (B 0 )+ g(B 0 ) = (n + 1)2 n , and by Lemma 16, player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) whenever w < (n + 1)2 n . As all Boolean combinations of the predicates P 1 , . . . , P n are non-empty in A, but each structure in B 0 has an empty Boolean combination, we get the desired lower bound result: Corollary 17 If φ is an existential first order sentence expressing the property that all Boolean combinations of n unary predicates are non-empty, then the size of φ is at least (n + 1)2 n .
Q.E.D. 6 The Existential Complexity of the Length of Linear Order As we noted in the introdution, for each n there is first order sentence φ n of logarithmic size with respect to n which expresses the property that the length of a linear order is at least n. However, the sentence φ n has an unbounded number of quantifier alternations. In this section we show that 2n−1 is the minimum size of an existential sentence expressing this property.
Clearly ψ n is true in a linear order if and only if its length is at least n, and an easy induction shows that w(ψ n ) = 2n − 1.
To prove the lower bound, we will use again the existential game EF ∃ w . Let where B is a linear order of length n − 1. Our aim is to show that player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) for all w < 2n − 1. Consider a position (u, A, B) in the game EF ∃ w (A 0 , B 0 ). Since the game is existential, A consists of a single structure (A, α). Let a 1 < A · · · < A a l be the elements in ran(α), and let a 0 and a l+1 be the least and the largest element in A, respectively. We say that a variable assignment β in B is acceptable (with respect to α) if dom(β) = dom(α), there are elements b 1 ≤ B · · · ≤ B b l such that ran(β) = {b 1 , . . . , b l } and for all i ∈ {1, . . . , l} and all j ∈ dom(α) In other words, β is acceptable if and only if the mapping α(j) → β(j), j ∈ dom(α), preserves the relation ≤. Furthermore, we say that β is nice (with respect to α), if it is acceptable, and in addition |{i ≤ l : d(a i , a i+1 ) = d(b i , b i+1 )}| = 1, where d(x, y) is the distance between x and y in the given linear order, and b 0 and b l+1 are the least and the largest element in B, respectively. The distance from defect of β is defined by . Note also, that for each i ≤ l there is exactly one nice β such that i(β) = i.
For the rest of this section, we assume that A is a singleton set {(A, α)} and B is a set of structures of the form (B, β). The niceness measure of B is defined to be where N is the set of all nice variable assignments β such that (B, β) ∈ B. Proof. If N(B) > 1, then either there is a nice assignment β ∈ N such that δ(β) ≥ 1, or there are two distinct nice assignments β, β ′ ∈ N . Assume first that β is a nice assignment in N , and δ(β) ≥ 1. Then there are elements a 1 , . . . , a l , b 1 , . . . , b l such that ran(α) = {a 1 , . . . , a l }, ran(β) = {b 1 , . . . , b l }, a 1 < A · · · < A a l and b 1 ≤ B · · · ≤ B b l . Since β is nice, d(b i , b i+1 ) = δ(β) ≥ 1 for i = i(β), and d(b i , b i+1 ) = d(a i , a i+1 ) ≥ 1 for all other i ≤ l. Thus, we have b 1 < B · · · < B b l . It follows easily from condition (12) that (A, α) and (B, β) satisfy the same atomic formulas, whence no atomic formula separates A and B. Assume then that β, β ′ ∈ N , and β = β ′ . As noted above, this means that i(β) = i(β ′ ). Let a 1 , . . . , a l be as above, and let ran(β) = {b 1 , . . . , b l } and ran(β ′ ) = {b ′ 1 , . . . , b ′ l } with b 1 ≤ B · · · ≤ B b l and b ′ 1 ≤ B · · · ≤ B b ′ l . As above, we see that b i < B b i+1 for all i ≤ l except i = i(β), and similarly b for all i ≤ l except i = i(β ′ ). Moreover, since i(β) = i(β ′ ), for all i, j ≤ l, we have either ( . Using condition (12), it is now easy to see that no atomic formula separates the sets A and B.
Q.E.D. (b) Let N and N ′ be the sets of nice β such that (B, β) is in B and B ′ , respectively. Let ran(α) = {a 1 , . . . , a l } with a 1 < A · · · < A a l , where α is the assignment such that A = {(A, α)}. As usual, we denote by a 0 and a l+1 the least and the largest element in A, respectively. Furthermore, we denote F ((A, α)) by c.
Assume next that c = a 0 or c = a l+1 . Then as above, we see that β ∈ N ⇐⇒ β(d/j) ∈ N ′ , where d is the least or the largest element in B, respectively, and δ(β(d/j)) = δ(β). Thus, also in this case we conclude that N(B ′ ) = N(B).
Assume finally, that c ∈ {a 0 , . . . , a l+1 }. Then there is an index h ≤ l such that a h < A c < A a h+1 . Let β be a nice assignment in N , and let ran(β) = {b 1 , . . . , b l } with b 1 ≤ B · · · ≤ B b l . As noted earlier, there is exactly one nice assignment β h such that i(β h ) = h. If β = β h , then d(b h , b h+1 ) = d(a h , a h+1 ), whence there is an element d such that d(b h , d) = d(a h , c) and d(d, b h+1 ) = d(c, a h+1 ). This means that δ(β(d/j)) = δ(β), and clearly β(d/j) is in N ′ .
Lemma 20 If w < N(B), then player II has a winning strategy in EF ∃ w (A, B).
Proof. The proof is verbatim the same as for Lemma 16; just replace M(B) by N(B). Q.E.D.
The proof of the lower bound result is also similar to that in the previous section. Consider the sets A 0 = {(A, ∅)} and B 0 = {(B, ∅)}. Clearly δ(∅) = n − 1, and so N(B 0 ) = 2(n − 1) + 1 = 2n − 1. Thus, by Lemma 20, player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) for all w < 2n − 1. Since the length of the linear order A is n, while the length of B is less than n, we have proved Corollary 21 If φ is an existential first order sentence expressing the property that the length of a linear order is at least n, then the size of φ is at least 2n − 1. Q.E.D.