nLab Ehrenfeucht-Fraïssé games

Idea

Ehrenfeucht-Fraïssé games are a technique in model theory for studying whether two 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_\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\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_i\in A$ and $b_i\in B$. At the end of the game we have a play which is a pair $(\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 : \langle\bar a\rangle_{\mathfrak{A}} \to \langle\bar b\rangle_{\mathfrak{B}}$ such that $f(a_i)=b_i$ for $i\lt\gamma$. (The notation $\langle\bar a\rangle_{\mathfrak{A}}$ denotes the substructure of $\mathfrak{A}$ generated by the sequence $\bar a$.)

An alternative way of phrasing the winning condition is to say that the play $(\bar a,\bar b)$ is a win for the duplicator if and only if $(\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_\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_\gamma(\mathfrak{A},\mathfrak{B})$ is an infinite game if $\gamma\ge\omega$.

Back-and-forth systems

For the game $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 $I$ of pairs $(\bar a,\bar b)$ of equal length sequences from $\mathfrak{A}$ and $\mathfrak{B}$ such that

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

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

• for every $(\bar a,\bar b)\in I$ and every $b\in B$, there is an $a \in A$ such that $(\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 $(\bar a,\bar b)$ is a win for the duplicator in $EF_\omega(\mathfrak{A},\mathfrak{B})$, then there is an isomorphism $f : \mathfrak{A} \to \mathfrak{B}$ with $f(a_i)=b_i$ for $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_\gamma[\mathfrak{A},\mathfrak{B}]$ is played exactly like $EF_\gamma(\mathfrak{A},\mathfrak{B})$, but a play $(\bar a,\bar b)$ counts as a win for the duplicator if and only $(\mathfrak{A},\bar a)$ and $(\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 = y$ for variables $x$ and $y$,

• $x = c$ for variable $x$ and constant symbol $c$,

• $x = f(\bar y)$ for variables $x$ and $\bar y$ and function symbol $f$,

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

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_\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 $L$ has finitely many symbols. Then we can effectively find for each $k,n\lt\omega$ a finite set $\Theta_{n,k}$ of unnested formulas in $n$ free variables of quantifier rank at most $k$, such that

• for every $L$-structure $\mathfrak{A}$, all $k,n\lt\omega$, and all $n$-tuples $\bar a$ from $\mathfrak{A}$, there is exactly one formula $\theta$ in $\Theta_{n,k}$ with $(\mathfrak{A},\bar a) \vDash \theta$,

• for all $k,n\lt\omega$ and all $L$-structures $\mathfrak{A}$ and $\mathfrak{B}$ and corresponding $n$-tuples $\bar a$ and $\bar b$ we have $(\mathfrak{A},\bar a) \approx_k (\mathfrak{B},\bar b)$ if and only if there is $\theta\in\Theta_{n,k}$ satisfied by both $(\mathfrak{A},\bar a)$ and $(\mathfrak{B},\bar b)$,

• for all $k,n\lt\omega$ it holds that every unnested formula in $n$ free variables of quantifier rank at most $k$ is equivalent to a disjunction of formulas in $\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\lt\omega$, $\mathfrak{A} \approx_k \mathfrak{B}$.

Dynamic Ehrenfeucht-Fraïssé games

The condition occurring in Fraïssé‘s theorem, that for every $k\lt\omega$, $\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_\alpha(\mathfrak{A},\mathfrak{B})$, to be a finite game of perfect information, defined by induction on $\alpha$ as follows:

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

• for $\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_\beta((\mathfrak{A},a),(\mathfrak{B},b))$, where $a\in A$ and $b\in B$ are the two elements picked, and this play in $EFD_\alpha(\mathfrak{A},\mathfrak{B})$ is a win for duplicator if and only if the play in $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_\beta(\mathfrak{A},\mathfrak{B})$, and this play in $EFD_\alpha(\mathfrak{A},\mathfrak{B})$ is a win for duplicator if and only if the play in $EFD_\beta(\mathfrak{A},\mathfrak{B})$ is a win for duplicator.

The game $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_\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_\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_\beta)_{\beta\lt\alpha}$ of inhabited sets of pairs $(\bar a,\bar b)$ of equal length sequences from $\mathfrak{A}$ and $\mathfrak{B}$ such that

• $I_\beta \subseteq I_\gamma$ for $\gamma\lt\beta\lt\alpha$,

• for every $\beta\lt\alpha$ and every $(\bar a,\bar b)\in I_\beta$ we have $(\mathfrak{A},\bar a) \equiv_0 (\mathfrak{B},\bar b)$, and

• for every $\beta+1\lt\alpha$ and every $(\bar a,\bar b)\in I_{\beta+1}$ and every $a\in A$, there is a $b\in B$ such that $(\bar a a, \bar b b)\in I_\beta$, and

• for every $\beta+1\lt\alpha$ and every $(\bar a,\bar b)\in I_{\beta+1}$ and every $b\in B$, there is an $a \in A$ such that $(\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_{\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_{\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.

Related concepts

• type in model theory
• Ehrenfeucht-Fraïssé comonad

References

• Wilfrid Hodges, Model Theory, Cambridge University Press 1993

• Jouko Väänänen, Models and Games, Cambridge University Press 2011

• Wikipedia, Ehrenfeucht–Fraïssé game