nLab
Ehrenfeucht-Fraïssé games

Contents

Idea

Ehrenfeucht-Fraïssé games are a technique in model theory for studying whether to structures are elementary equivalent. Variations can be used to study equivalence with respect to logics other than first-order logic.

The games are played by two players: the spoiler, whose objective is to establish a difference between the two structures, and the duplicator, whose objective is to show that the two structures are similar.

A game is played in turns for a number of rounds (in general an ordinal, but usually a finite number or ω\omega). In each round the spoiler picks an element of one of the structures and then the duplicator responds by picking an element of the other structure. At the end of the game they have together selected two sequences of equal length of elements of the two structures, and the duplicator wins if the sequences generate isomorphic substructures of the given structures. (See below for variations in the winning conditions.)

Definition

We first define the Ehrenfeucht-Fraïssé game of length γ\gamma on 𝔄\mathfrak{A} and 𝔅\mathfrak{B}, EF γ(𝔄,𝔅)EF_\gamma(\mathfrak{A},\mathfrak{B}). It is a game of perfect information played as follows. The ordinal γ\gamma is the length of the game, and at step i<γi\lt\gamma, the spoiler chooses an element of either 𝔄\mathfrak{A} or 𝔅\mathfrak{B}; then the duplicator chooses an element of the other structure. Between them they choose a iAa_i\in A and b iBb_i\in B. At the end of the game we have a play which is a pair (a¯,b¯)(\bar a,\bar b) of sequences of length γ\gamma. We count this play as a win for the duplicator if there is an isomorphism f:a¯ 𝔄b¯ 𝔅f : \langle\bar a\rangle_{\mathfrak{A}} \to \langle\bar b\rangle_{\mathfrak{B}} such that f(a i)=b if(a_i)=b_i for i<γi\lt\gamma. (The notation a¯ 𝔄\langle\bar a\rangle_{\mathfrak{A}} denotes the substructure of 𝔄\mathfrak{A} generated by the sequence a¯\bar a.)

An alternative way of phrasing the winning condition is to say that the play (a¯,b¯)(\bar a,\bar b) is a win for the duplicator if and only if (𝔄,a¯) 0(𝔅,b¯)(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b), i.e., the expansions of the two structures by the given sequences satisfy the same atomic (or the same quantifier-free) sentences.

Definition

We write 𝔄 γ𝔅\mathfrak{A} \sim_\gamma \mathfrak{B} to mean that the duplicator has a winning strategy in the game EF γ(𝔄,𝔅)EF_\gamma(\mathfrak{A},\mathfrak{B}).

It is easy to see that this is an equivalence relation on structures, and 𝔄 γ𝔅\mathfrak{A} \sim_\gamma \mathfrak{B} always holds when 𝔄\mathfrak{A} and 𝔅\mathfrak{B} are isomorphic. Note the EF γ(𝔄,𝔅)EF_\gamma(\mathfrak{A},\mathfrak{B}) is an infinite game if γω\gamma\ge\omega.

Back-and-forth systems

For the game EF ω(𝔄,𝔅)EF_\omega(\mathfrak{A},\mathfrak{B}) we have the following alternative characterization of 𝔄 ω𝔅\mathfrak{A} \sim_\omega \mathfrak{B}.

A back-and-forth system from 𝔄\mathfrak{A} to 𝔅\mathfrak{B} is an inhabited set II of pairs (a¯,b¯)(\bar a,\bar b) of equal length sequences from 𝔄\mathfrak{A} and 𝔅\mathfrak{B} such that

  • for every (a¯,b¯)I(\bar a,\bar b)\in I we have (𝔄,a¯) 0(𝔅,b¯)(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b), and

  • for every (a¯,b¯)I(\bar a,\bar b)\in I and every aAa\in A, there is a bBb\in B such that (a¯a,b¯b)I(\bar a a, \bar b b)\in I, and

  • for every (a¯,b¯)I(\bar a,\bar b)\in I and every bBb\in B, there is an aAa \in A such that (a¯a,b¯b)I(\bar a a, \bar b b)\in I.

Proposition

There is a back-and-forth system from 𝔄\mathfrak{A} to 𝔅\mathfrak{B} if and only if 𝔄 ω𝔅\mathfrak{A} \sim_\omega \mathfrak{B}.

For this reason we say that 𝔄\mathfrak{A} and 𝔅\mathfrak{B} are back-and-forth equivalent if and only if 𝔄 ω𝔅\mathfrak{A} \sim_\omega \mathfrak{B}. (Other names for back-and-forth equivalence are partial isomorphism or potential isomorphism.)

Example

Any two algebraically closed fields of equal characteristic and infinite transcendence degree over their respective prime subfields are back-and-forth equivalent. A back-and-forth system is in this case given by the pairs of generating sequences for isomorphic finitely generated subfields.

Theorem

Suppose 𝔄\mathfrak{A} and 𝔅\mathfrak{B} are at most countable back-and-forth equivalent structures. Then 𝔄\mathfrak{A} and 𝔅\mathfrak{B} are isomorphic, and if the play (a¯,b¯)(\bar a,\bar b) is a win for the duplicator in EF ω(𝔄,𝔅)EF_\omega(\mathfrak{A},\mathfrak{B}), then there is an isomorphism f:𝔄𝔅f : \mathfrak{A} \to \mathfrak{B} with f(a i)=b if(a_i)=b_i for i<ωi\lt\omega.

Corollary

(Cantor’s Theorem) Any two countable dense linear orders without endpoints are isomorphic. A back-and-forth system is given by the pairs of finite sequences of isomorphic finite suborders.

Unnested Ehrenfeucht-Fraïssé games

One major application of Ehrenfeucht-Fraïssé games is to study elementary equivalence. For languages without (non-constant) function symbols, however, we need a slight modification to the above definitions.

The unnested Ehrenfeucht-Fraïssé game of length γ\gamma on 𝔄\mathfrak{A} and 𝔅\mathfrak{B}, EF γ[𝔄,𝔅]EF_\gamma[\mathfrak{A},\mathfrak{B}] is played exactly like EF γ(𝔄,𝔅)EF_\gamma(\mathfrak{A},\mathfrak{B}), but a play (a¯,b¯)(\bar a,\bar b) counts as a win for the duplicator if and only (𝔄,a¯)(\mathfrak{A},\bar a) and (𝔅,b¯)(\mathfrak{B},\bar b) satisfy the same unnested atomic formulas.

Recall that an unnested atomic formula for a first-order language of one of the following forms:

  • x=yx = y for variables xx and yy,

  • x=cx = c for variable xx and constant symbol cc,

  • x=f(y¯)x = f(\bar y) for variables xx and y¯\bar y and function symbol ff,

  • R(x¯)R(\bar x) for variables x¯\bar x and relation symbol RR.

Any atomic formula is equivalent to a Δ\Delta-formula built from unnested atomic formulas (but the quantifier rank grows with the size of the involved terms).

Definition

We write 𝔄 γ𝔅\mathfrak{A} \approx_\gamma \mathfrak{B} to mean that the duplicator has a winning strategy in the game EF γ[𝔄,𝔅]EF_\gamma[\mathfrak{A},\mathfrak{B}].

Note that 𝔄 γ𝔅\mathfrak{A} \sim_\gamma \mathfrak{B} implies 𝔄 γ𝔅\mathfrak{A} \approx_\gamma \mathfrak{B} and the converse holds whenever the language has no constant and function symbols (as in that case every atomic formula is automatically unnested).

The key reason to introduce the unnested formulas and games is the following theorem:

Theorem

(Fraïssé-Hintikka theorem) Suppose the language LL has finitely many symbols. Then we can effectively find for each k,n<ωk,n\lt\omega a finite set Θ n,k\Theta_{n,k} of unnested formulas in nn free variables of quantifier rank at most kk, such that

  • for every LL-structure 𝔄\mathfrak{A}, all k,n<ωk,n\lt\omega, and all nn-tuples a¯\bar a from 𝔄\mathfrak{A}, there is exactly one formula θ\theta in Θ n,k\Theta_{n,k} with (𝔄,a¯)θ(\mathfrak{A},\bar a) \vDash \theta,

  • for all k,n<ωk,n\lt\omega and all LL-structures 𝔄\mathfrak{A} and 𝔅\mathfrak{B} and corresponding nn-tuples a¯\bar a and b¯\bar b we have (𝔄,a¯) k(𝔅,b¯)(\mathfrak{A},\bar a) \approx_k (\mathfrak{B},\bar b) if and only if there is θΘ n,k\theta\in\Theta_{n,k} satisfied by both (𝔄,a¯)(\mathfrak{A},\bar a) and (𝔅,b¯)(\mathfrak{B},\bar b),

  • for all k,n<ωk,n\lt\omega it holds that every unnested formula in nn free variables of quantifier rank at most kk is equivalent to a disjunction of formulas in Θ n,k\Theta_{n,k}.

This appears as Theorem 3.3.2 in Hodges 93.

Corollary

(Fraïssé‘s theorem) Two structures 𝔄\mathfrak{A} and 𝔅\mathfrak{B} in a finite language are elementarily equivalent, 𝔄𝔅\mathfrak{A} \equiv \mathfrak{B}, if and only if for every k<ωk\lt\omega, 𝔄 k𝔅\mathfrak{A} \approx_k \mathfrak{B}.

Dynamic Ehrenfeucht-Fraïssé games

The condition occurring in Fraïssé‘s theorem, that for every k<ωk\lt\omega, 𝔄 k𝔅\mathfrak{A} \approx_k \mathfrak{B}, is nicely captured by another variation of either the ordinary or the unnested Ehrenfeucht-Fraïssé game. Namely, instead of taking an ordinal γ\gamma to be the length of the game, we can let an ordinal α\alpha be part of the playing field, so to speak, indicating in a sense how many times the spoiler can change his mind about the length of the game, yet keeping the game finite.

More precisely, we define the dynamic Ehrenfeucht-Fraïssé game measured by α\alpha on 𝔄\mathfrak{A} and 𝔅\mathfrak{B}, EFD α(𝔄,𝔅)EFD_\alpha(\mathfrak{A},\mathfrak{B}), to be a finite game of perfect information, defined by induction on α\alpha as follows:

  • for α=0\alpha=0 there is a unique play (i.e., the players do nothing) that is a win for the duplicator if and only if 𝔄 0𝔅\mathfrak{A} \equiv_0 \mathfrak{B},

  • for α=β+1\alpha=\beta+1, a play consists of the spoiler picking an element of one structure, followed by the duplicator picking an element of the other structure, followed by a play of EFD β((𝔄,a),(𝔅,b))EFD_\beta((\mathfrak{A},a),(\mathfrak{B},b)), where aAa\in A and bBb\in B are the two elements picked, and this play in EFD α(𝔄,𝔅)EFD_\alpha(\mathfrak{A},\mathfrak{B}) is a win for duplicator if and only if the play in EFD β((𝔄,a),(𝔅,b))EFD_\beta((\mathfrak{A},a),(\mathfrak{B},b)) is a win for duplicator,

  • for α\alpha a limit ordinal, a play consists of the spoiler picking an ordinal β<α\beta\lt\alpha, and then a continued play in EFD β(𝔄,𝔅)EFD_\beta(\mathfrak{A},\mathfrak{B}), and this play in EFD α(𝔄,𝔅)EFD_\alpha(\mathfrak{A},\mathfrak{B}) is a win for duplicator if and only if the play in EFD β(𝔄,𝔅)EFD_\beta(\mathfrak{A},\mathfrak{B}) is a win for duplicator.

The game EFD α[𝔄,𝔅]EFD_\alpha[\mathfrak{A},\mathfrak{B}] is defined similarly, using unnested atomic formulas in the base case.

Definition

We write 𝔄 ω α𝔅\mathfrak{A} \sim^\alpha_\omega \mathfrak{B} to mean that the duplicator has a winning strategy in the game EFD α(𝔄,𝔅)EFD_\alpha(\mathfrak{A},\mathfrak{B}) and 𝔄 ω α𝔅\mathfrak{A} \approx^\alpha_\omega \mathfrak{B} to mean that the duplicator has a winning strategy in the game EFD α[𝔄,𝔅]EFD_\alpha[\mathfrak{A},\mathfrak{B}].

We use a subscript ω\omega to indicate that the relations ω α{\sim^\alpha_\omega} and ω α{\approx^\alpha_\omega} form approximations to ω{\sim_\omega} and ω{\approx_\omega}, respectively.

Back-and-forth sequences

There is an alternative characterization of the relations ω α{\sim^\alpha_\omega} in terms of back-and-forth sequences.

We define a back-and-forth sequence of length α\alpha from 𝔄\mathfrak{A} to 𝔅\mathfrak{B} to be a sequence (I β) β<α(I_\beta)_{\beta\lt\alpha} of inhabited sets of pairs (a¯,b¯)(\bar a,\bar b) of equal length sequences from 𝔄\mathfrak{A} and 𝔅\mathfrak{B} such that

  • I βI γI_\beta \subseteq I_\gamma for γ<β<α\gamma\lt\beta\lt\alpha,

  • for every β<α\beta\lt\alpha and every (a¯,b¯)I β(\bar a,\bar b)\in I_\beta we have (𝔄,a¯) 0(𝔅,b¯)(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b), and

  • for every β+1<α\beta+1\lt\alpha and every (a¯,b¯)I β+1(\bar a,\bar b)\in I_{\beta+1} and every aAa\in A, there is a bBb\in B such that (a¯a,b¯b)I β(\bar a a, \bar b b)\in I_\beta, and

  • for every β+1<α\beta+1\lt\alpha and every (a¯,b¯)I β+1(\bar a,\bar b)\in I_{\beta+1} and every bBb\in B, there is an aAa \in A such that (a¯a,b¯b)I β(\bar a a, \bar b b)\in I_\beta.

Proposition

There is a back-and-forth sequence of length α\alpha from 𝔄\mathfrak{A} to 𝔅\mathfrak{B} if and only if 𝔄 ω α𝔅\mathfrak{A} \sim^\alpha_\omega \mathfrak{B}.

Clearly, if 𝔄\mathfrak{A} and 𝔅\mathfrak{B} are back-and-forth equivalent, then we can make a back-and-forth sequences of any length by taking the constant sequence at a back-and-forth system.

Use in infinitary logic

Recall that the formulas in the logic L ωL_{\infty\omega} can be built using infinitary disjunctions and conjunctions. We write 𝔄 ω𝔅\mathfrak{A} \equiv_{\infty\omega} \mathfrak{B} (resp. 𝔄 ω α𝔅\mathfrak{A} \equiv_{\infty\omega}^\alpha \mathfrak{B}) to mean that 𝔄\mathfrak{A} and 𝔅\mathfrak{B} satisfy the same sentences of L ωL_{\infty\omega} (resp. of quantifier rank at most α\alpha).

There is a close relationship between the expressivity of this infinitary logic and the relations ω{\sim_\omega} and ω α{\sim_\omega^\alpha}, as the following theorem shows:

Theorem

We have 𝔄 ω α𝔅\mathfrak{A} \equiv_{\infty\omega}^\alpha \mathfrak{B} if and only if 𝔄 ω α𝔅\mathfrak{A} \sim_\omega^\alpha \mathfrak{B} and 𝔄 ω𝔅\mathfrak{A} \equiv_{\infty\omega} \mathfrak{B} if and only if 𝔄 ω𝔅\mathfrak{A} \sim_\omega \mathfrak{B}.

This is Theorem 4.47 and Proposition 7.48 in Väänänen 2011.

References

Last revised on May 27, 2017 at 09:42:34. See the history of this page for a list of all contributions to it.