On the Freedom of Spoiler in the EF Game
On the Freedom of Spoiler in
Ehrenfeucht-Fraïssé Games
Wafik Boulos Lotfallah1
and
Maha Ragab Youssef 2
Abstract
We analyze the freedom of the first player (Spoiler) in the (first and second order) Ehrenfeucht-Fraïssé games. This freedom is restricted by patterns specifying where Spoiler plays. For each such pattern (as well as classes of such patterns), we define both a game and a logic, and then show their equivalence.
The results here reveal the "anatomy" of the Ehrenfeucht-Fraïssé games and subsume the known theorems stating the equivalence between these games and their corresponding logics.
As a byproduct we show that, in the original game, Spoiler can be forced to announce how he is planning to play without loss of his winning power. As far as the authors know, this result has not been shown before.
The setting of this paper is similar to that of [13], but it carries the study in a different direction, where we were mostly concerned with a theoretical analysis of the winning strategies of the players, when Spoiler’s moves are restricted.
ملخص
سوف نحلل حرية الحركة للاعب الأول في مبارياتEhrenfeucht-Fraïssé . هذه الحرية مقيدة بنموذج يحدد اختيارات اللاعب الأول. لكل نموذج سوف نعرف المباراة الخاصة به و كذلك المنطق الذي يعرفه و العلاقة بينهم.
بعض النتائج سوف تظهر التصنيفات المختلفة للمباريات و العلاقة بين هذه المباريات و المناطق المناظرة. و كنتيجة لهذا سوف نوضح أن اللاعب الأول لن يفقد فرصه في الفوز في حالة إذا أجبر على إعلان خطته من البداية.
1- Department of Engineering Mathematics and physics, Faculty of Engineering, cairo university.
2- Department of Mathematics, Faculty of science, Helwan university.
1
1- Introduction
The Ehrenfeucht-Fraïssé game (or EF-game) for first order logic was defined (in two different ways) in [7] and [4], where they showed that first order logic with quantifier rank n is characterized by the EF-game of n-rounds. More precisely, for each pair of (relational) models A and B over the same vocabulary, A and B agree on all first order sentences of quantifier rank n if and only if the second player (Duplicator) has a winning strategy for the EF-game of n rounds (see [3]).
This game has been extended in several ways:
- First order logic was replaced by more powerful logics, e.g. (existential monadic) second order logic, logic with generalized quantifiers, infinitary logics with finitely many variables, etc. and the E-F game has to be modified to capture the expressive power of such logics (see [5], [2], [17], [8], [12], [9], [10]).
- The game had some restrictions on the moves of Spoiler, where Spoiler can only move within a prescribed distance from the elements already chosen in the two models (see [14], [15]).
- The game was played on two classes of models instead of just two models (see [1], [6], [16].)
In this paper we introduce another variant of the game where the restrictions on the moves of Spoiler allow him only to play in a particular model (which may change throughout the game). These restrictions generalize the game for the existential monadic second order game first introduced by [5] and further modified by [1], and extend the work done in [11] and [13].
2- Basic Definitions
The main theme of this paper is the interplay between logics, i.e. languages with different expressive powers, and games played on pairs of models.
We consider only relational vocabularies containing several unary predicates and constant symbols. All of the results in this paper hold for the class of finite models as well as the class of all models.
For simplicity we consider only monadic second order extensions of first order logic, where second order variables are unary, even though the results here easily carry over to non-unary second order logics.
The Ehrenfeucht-Fraïssé game (or EF-game) for First-Order logic was defined (in two different ways) in [7] and [4], where they showed that First-Order logic with quantifier rank m is characterized by the EF-game of m-rounds. We begin with a definition of a regular EF-games for First-Order logic, the players, their moves, the winning strategy, and finally the main theorem which shows why these games are of interest.
The main idea of The EF-game Gm is that it is played by two players, Spoiler and Duplicator on a pair of structures A and B of the same relational vocabulary τ. Spoiler tries to prove that the two structures look different, while Duplicator tries to prove that they look alike.
More precisely, the EF-game Gm(A, B) of m rounds is defined by recursion on m as follows:
(1) If m > 0, then:
- Spoiler chooses an element aA (bB).
- Duplicator chooses an element bB (aA).
- The game continues from the new position
Gm-1((A,a),(B,b)).
(2) If m=0, the game ends and Duplicator wins if and only if A and B satisfy the same first-order atomic sentences, i.e. the substructure of A generated by its constant symbols {a1, …, am} is isomorphic to the substructure of B generated by its constant symbols {b1, …, bm} by an isomorphism that maps each ai onto bi.
A winning strategy for Duplicator is a rule, according to which Duplicator plays to guarantee a win for her. This can be described by a sequence of functions that take Spoiler’s choices up to the current move, and produces Duplicator’s choice.
Notation: We write A ~m B if Duplicator wins the EF-game starting from the position Gm( A, B).
Two structures A, B are m-equivalence, written A B if they satisfy the same first-order formulas of quantifier rank at most m.
The main theorem of the regular EF-games for first-order logic is:
Theorem 2.1 [3]: Let A and B be structures of the same vocabulary. Then the following two conditions are equivalent:
- A B.
- A B
■
By a logic we will mean a set of monadic second order formulas which is positive Boolean closed, that is, closed under finite conjunctions and disjunctions. As usual, sentences are formulas with no free variables.
For any set of MSO formulas S, define PB(S) to be the set of all positive Boolean combinations of formulas of S, i.e. it contains all finite conjunctions of finite disjunctions of formulas of S. Thus, PB(S) is positive Boolean closed and is the least logic containing S.
To clarify the different roles of universal and existential quantifiers, we assume that all negation signs are pushed inside.
We shall sometimes view formulas as trees with nodes labeled by conjunction signs, disjunction signs, first order and monadic second order quantifications, and leafs labelled by literals, i.e. atomic and negation of atomic formulas.
Letting , be the first order and , be the monadic second order quantifiers, we will say that a quantifier word (or pattern) w over the alphabet {, , , } supports a sentence φ if the quantifiers which occur on any path in φ from the root to a leaf form a substring of w (i.e. the quantifiers occur in w in the right order).
The following example and proposition was mentioned in [13].
Example 2.2: The prenex sentence (x)(y)(Y)(p(y)Y(x)) is supported by the quantifier word , while the sentence (x)((y)P(y)(Y)Y(x)) is supported by the word as well as.
We let L(w) be the set of all MSO formulas supported by w. One can then easily see:
Proposition 2.3: L(w) is positive Boolean closed (i.e. PB(L(w))=L(w)).
■
We will thus call L(w) the logic supported by w.
Equivalently, one can define the logic L(w) inductively as follows:
(1) The empty word supports the set of all quantifier free MSO-formulas.
(2) L(w) = PB(L(w){(x)φ: φL (w)}).
(3) L(w) = PB(L(w){(x) φ: φL (w)}).
(4) L(w) = PB(L(w) {(X)φ: φL (w)}).
(5) L (w) = PB(L (w) {(X) φ: φL (w)}).
Define a class W to be a set of words over {, , , }. W is sometimes defined by a regular expression using the following rules:
1- W = = {} where is the empty word (pattern),
2- W = q = {q} where q {, , , },
and recursively:
3- W = UV= {uv : uU and vV},
4- W = U+V= UV = {w: wU or wV},
5- W = U* = {un: uU, and n},
where U and V are regular expressions denoting two pattern classes.
Now define the logic L(W) supported by a pattern class W to be
L(W) = PB({φ : φ is supported by some wW}) = PB(wWL(w)).
Examples 2.4:
1) First order logic FO is the logic supported by the class ()* = (+)*, i. e. FO = L(()*).
2) First order logic of quantifier rank n FOn is the logic supported by the class (+)n, i. e. FOn = L((+)n).
3) Monadic second order logic MSO is the logic supported by the class ()* = (+)* or by the class (+++)*, i.e. MSO = L(()*)
4) Monadic existential second order logic MSO (monadic NP) is the logic supported by the class *()* , i.e. MSO = L(*()*)
5) Closed monadic existential second order logic (closed monadic NP) is the logic supported by the class (+)* or by (++)*.
Note that for certain prefix classes W, some formulas φL (W) are not equivalent to any formula ψL (W) in prenex normal form. The reason is that, to transform φ into the prenex form, we pull all quantifiers out, thus forming a rich quantifier prefix out of all quantifier paths through the formula tree.
3- The freedom of Spoiler
In this section we will use quantifier patterns to restrict the freedom of Spoiler, where in each round of the EF-game he is forced to play in a specific model determined by the pattern.
For each pattern w over {, , , } we will define a w-game on the pair of models (A, B). This w-game is an EF-like game and is played between two players Spoiler and Duplicator such that in existential moves Spoiler must choose in A and Duplicator responds in B, but in universal moves Spoiler must choose in B and Duplicator responds in A. More precisely the w-game is defined by recursion on the length of w as follows:
• If w =v (v), then:
(3) Spoiler chooses an element aA (bB).
(4) Duplicator chooses an element bB (aA).
(5) The two players play the v-game on (A, a), (B, b).
• If w =v (v), then:
(1) Spoiler chooses a subset C A (D B).
(2) Duplicator chooses a subset D B (C A).
(3) The two players play the v-game on (A, C), (B, D).
• If w = Ø (the empty word), then the game is over, and Duplicator wins the Ø-game iff A and B satisfy the same atomic sentences.
The idea here is that a quantifier pattern imposes some restriction on Spoiler’s moves, and specifies what kind of moves (first order, second order) are to be played in each round.
If some (but not total) freedom is given to Spoiler, we use a class W of patterns, and define a W-game played on a model pair (A, B) as follows:
(1) Spoiler starts by choosing a word wW (and announce it to Duplicator).
(2) Spoiler and Duplicator then play the w-game on (A, B).
Thus, a class of patterns draws the picture of Spoiler’s freedom on where and how to move. The next section will clarify the relationship between logics defined by (classes of) patterns and their corresponding games.
4- The Equivalence Theorems
We now show that the w-game corresponds to the logic L(w). More precisely:
Theorem 4.1: Let A, B be a pair of models over the same relational vocabulary. Then the following are equivalent:
1) For all φ in L(w), A╞ φ → B╞ φ .
2) Duplicator wins the w- game on the model pair (A, B).
Proof: We proceed by induction on the length m of the pattern w.
(1)→(2): We prove that Duplicator has a winning strategy for the w-game.
When m=0 (w is empty word) the game is over and Duplicator wins iff A and B satisfy the same atomic sentences. Since L(w) is the set of quantifier free sentences, this follows easily from (1).
Now assume that (1)→(2) holds for m, and prove that it also holds for m+1. Let w be of length m+1. We want to prove that Duplicator has a winning strategy for the w-game. We have four cases according to the kind of the quantifier in the first move.
Case a: w=v, where v is a pattern of length m.
Let Spoiler's first move in this game to choose an element a in A and let ψ(x) be the conjunction of all formulas in L(v) in the free variable x that (A, a) satisfy (where a interprets the variable x). Note that L(v) is finite up to logical equivalence. Thus ψ is also in L(v) and is the complete description of the formulas supported by v that (A, a) satisfies. Since (A, a)╞ ψ(x), we have A╞ x ψ(x) and so by our assumption (1) we also have B╞ x ψ(x). Now Duplicator responds by choosing an element b in B witnessing that ψ is true, i.e. (B, b)╞ ψ(x). Since ψ(x) is the complete description of the formulas supported by pattern v that (A, a) satisfies, it follows that for all φ in L(v), (A, a) ╞ φ → (B, b) ╞ φ. Then by the inductive hypothesis, Duplicator has a winning strategy for the remaining v– game.
Case b: w=v, where v is pattern of length m.
Let Spoiler's first move in this game to choose an element b in B and let ψ(x) be the (finite) disjunction of all formulas in L(v) in the free variable x that (B, b) does not satisfy (where b interprets the variable x). Thus ψ is also in L(v) and is the complete description of the formulas supported by v that (B, b) not satisfies. Since (B, b)╞/ ψ (x), we have B╞/x ψ (x) and so by our assumption (1) we also have A╞/x ψ (x). Now Duplicator responds by choosing an element a in A witnessing that ψ is not true, i.e. (A, a) ╞/ ψ(x). Since ψ(x) is the complete description of the formulas supported by pattern v that (B, b) not satisfies, it follows that for all φ in L(v), (B, b)╞/ φ (x) → (A, a) ╞/ φ (x). Then by the inductive hypothesis, Duplicator has a winning strategy for the remaining v– game.
Case c: w=v, where v is pattern of length m.
Let Spoiler's first move in this game to choose a (unary) relation R in A and let ψ(R) be the conjunction of all formulas in L(v) that (A, R) satisfy (where R interprets the second order variable R). By the same way, ψ(R) is in L(v) and is the complete description of the formulas supported by v that (A, R) satisfies. Since (A, R)╞ ψ(R), we have A╞ R ψ(R) and so by our assumption (1) we also have B╞ R ψ(R). Now Duplicator responds by choosing a (unary) relation R in B (interpretation of R in B) witnessing that ψ is true, i.e. (B, R)╞ ψ(R). Since ψ(R) is the complete description of the formulas supported by pattern v that (A, R) satisfies, it follows that for all φ in L(v), (A, R) ╞ φ(R) → (B, R) ╞ φ(R). Then by the inductive hypothesis, Duplicator has a winning strategy for the remaining v– game.
Case d: w=v, where v is pattern of length m.
Let Spoiler's first move in this game to choose a (unary) relation R in B and let ψ(R) be the disjunction of all formulas in L(v) that (B, R) does not satisfy (where R interprets the second order variable R). ψ(R) is also in L(v) and is the complete description of the formulas supported by v that (B, R) does not satisfy. Since (B, R)╞/ ψ(R), we have B╞/R ψ(R) and so by our assumption (1) we also have A╞/ R ψ(R). Now Duplicator responds by choosing a (unary) relation R in A (interpretation of R in A) witnessing that ψ is not true, i.e. (A, R) ╞/ ψ(R). Since ψ(R) is the complete description of the formulas supported by pattern v that (B, R) does not satisfy, it follows that for all φ in L(v), (B, R)╞/ φ(R) → (A, R) ╞/ φ(R). Then by the inductive hypothesis, Duplicator has a winning strategy for the remaining v– game.
(2)→(1): This is proved by contraposition. Let (1) be not true. We show that (2) is not true by describing Spoiler's winning strategy in the w-game. As before, we will use induction on the length m of the pattern w.
When m=0 (w is empty word), the game is over. Since (1) is not true, for some quantifier free sentence φ, A╞ φ but B╞/ φ. Thus Spoiler wins the Ø-game.
Now assume the implication holds for m and prove that it also holds for m+1.
Let A╞ φ but B╞/ φ, for some sentence φ supported by a pattern w with length m+1. We also have four cases:
Case a: w= v, where v is a pattern of length m.
Since φ is supported by w, it is equivalent to the conjunction of disjunctions of formulas of the formx ψ(x) (i.e. φ = (x ψ (x)) ), where each ψ( x) is in L(v).
We first find a value of i such that:
A╞ (x ψ (x)), but B╞/ (x ψ (x)).
Then find a value of j such that:
A╞ x ψ (x), but B╞/ x ψ (x).
Spoiler's first move in this game is to choose an element a in A witnessing that ψ(x) is true, i.e. (A, a)╞ ψ(x). Now let Duplicator respond by any element b in B. Since B╞/x ψ(x), we must have (B, b)╞/ ψ(x). Since ψ(x) is in L(v), we can use the inductive hypothesis to show that Spoiler has a winning strategy for the remaining v-game.
Case b: w=v, where v is a pattern of length m.
Since φ is supported by w, it is equivalent to the conjunction of disjunctions of formulas of the formx ψ(x) (i.e. φ = (x ψ (x)) ), where each ψ(x) is in L(v).
We first find a value of i such that:
A╞ (x ψ (x)), but B╞/ (x ψ (x)).
Then find a value of j such that:
A╞ x ψ (x), but B╞/ x ψ (x).
Spoiler's first move in this game is to choose an element b in B witnessing that ψ(x) is not true, i.e. (B, b)╞/ ψ(x). Now let Duplicator respond by any element a in A. Since A╞xψ(x), we must have (A, a)╞ ψ(x). Since ψ(x) is in L(v), we can use the inductive hypothesis to show that Spoiler has a winning strategy for the remaining v-game.
Case c: w=v, where v is a pattern of length m.
Since φ is supported by w, it is equivalent to the conjunction of disjunctions of formulas of the formR ψ(R) (i.e. φ = (R ψ(R)) ), where each ψ(R) is in L(v).
We first find a value of i such that:
A╞ (R ψ(R)), but B╞/ (R ψ(R)).
Then find a value of j such that:
A╞ R ψ(R), but B╞/ R ψ(R).
Spoiler's first move in this game is to choose a relation R in A witnessing that ψ(R) is true, i.e. (A, R)╞ ψ(R). Now let Duplicator respond by any relation R in B. Since B╞/ Rψ(R), we must have (B, R)╞/ ψ(R). Since ψ(R) is in L(v), we can use the inductive hypothesis to show that Spoiler has a winning strategy for the remaining v-game.
Case d: w=v, where v is a pattern of length m.
Since φ is supported by w, it is equivalent to the conjunction of disjunctions of formulas of the formR ψ(R) (i.e. φ = (Rψ(R)) ), where each ψ(R) is in L(v).
We first find a value of i such that:
A╞ (Rψ(R)), but B╞/ (Rψ(R)).
Then find a value of j such that:
A╞ Rψ(R), but B╞/ R ψ(R).
Spoiler's first move in this game is to choose a relation R in B that witnesses that ψ(R) is not true, i.e. (B, R)╞/ ψ(R). Now let Duplicator respond by any relation R in B. Since A╞ R ψ(R), we must have (A, R)╞ ψ(R). Since ψ(R) is in L(v), we can use the inductive hypothesis to show that Spoiler has a winning strategy for the remaining v-game. ■
Now let us show the equivalence between the W-game and the logic L(W). More precisely:
Theorem 4.2: Let A, B be a pair of models over the same relational vocabulary. Then the following are equivalent:
1) For all φ in L(W), A ╞ φ → B╞ φ .
2) Duplicator wins the W- game on the model pair (A, B).
Proof: (1)→(2): Assuming (1), let first Spoiler choose a pattern wW and announce this choice to Duplicator. We show that Duplicator has a winning strategy for the w-game.
Since L(W) includes L(w), we know by (1) that for all φ in L(w), A ╞ φ → B╞ φ. since φ supported by wW, But then, by Theorem 4.1, Duplicator wins the w-game for all wW and then he can win W- game .
(2)→(1): Assuming not (1), there is a φ in L(W) such that A ╞ φ but B╞/φ . By definition of L(W) = PB(wWL(w)), φ is equivalent to the (finite) conjunction of (finite) disjunctions of formulas in wWL(w), (i.e. φ = ψ ), where each ψ is in L(w) for some w in W.
Here again we find a value of i such that:
A╞ ψ (x), but B╞/ ψ (x).
Then find a value of j such that:
A╞ ψ, but B╞/ ψ .
Since ψ is in L(w) for some w in W, let Spoiler choose this pattern wW and announce this choice to Duplicator. Now A and B disagree on a formula ψ supported by w in W then by the second implication of Theorem 4.1, Spoiler wins the w-game and so he wins the W- game (since he wins w-game for every w in W ). ■
5- The Corollaries
The following corollaries are now immediate:
Corollary 5.1: A class of models C can be expressed by a sentence φ L(W) if and only if for all models A and B, such that AC and BC, Spoiler wins the W-game on (A,B).
Equivalently: A class of models C can Not be expressed by a sentence φ L(W) if and only if for some models A and B, such that AC and BC, Duplicator wins the W-game on (A,B). ■
Corollary 5.1 makes a tight connection between the W-game and the logic L(W). We say in such case that the W-game characterizes the logic L(W).
In the following corollaries we will show that the W-games include all other kinds of EF-game in FO and in MSO logics.
Corollary 5.2: FO with quantifier rank n is characterized by the (+)n-game. ■
Note: The (+)n-game here is slightly different than the regular n-round EF game, as Spoiler must choose some pattern of length n and announce it to Duplicator. This leads to a somewhat surprising fact: