indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
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.)
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.
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$.
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$.
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.)
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.
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$.
(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.
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).
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:
(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.
(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}$.
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.
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.
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$.
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.
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:
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.
Wilfrid Hodges, Model Theory, Cambridge University Press 1993
Jouko Väänänen, Models and Games, Cambridge University Press 2011
Wikipedia, Ehrenfeucht–Fraïssé game
Last revised on May 27, 2017 at 09:42:34. See the history of this page for a list of all contributions to it.