indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
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 ). 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 on and , . It is a game of perfect information played as follows. The ordinal is the length of the game, and at step , the spoiler chooses an element of either or ; then the duplicator chooses an element of the other structure. Between them they choose and . At the end of the game we have a play which is a pair of sequences of length . We count this play as a win for the duplicator if there is an isomorphism such that for . (The notation denotes the substructure of generated by the sequence .)
An alternative way of phrasing the winning condition is to say that the play is a win for the duplicator if and only if , i.e., the expansions of the two structures by the given sequences satisfy the same atomic (or the same quantifier-free) sentences.
We write to mean that the duplicator has a winning strategy in the game .
It is easy to see that this is an equivalence relation on structures, and always holds when and are isomorphic. Note the is an infinite game if .
For the game we have the following alternative characterization of .
A back-and-forth system from to is an inhabited set of pairs of equal length sequences from and such that
for every we have , and
for every and every , there is a such that , and
for every and every , there is an such that .
There is a back-and-forth system from to if and only if .
For this reason we say that and are back-and-forth equivalent if and only if . (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 and are at most countable back-and-forth equivalent structures. Then and are isomorphic, and if the play is a win for the duplicator in , then there is an isomorphism with for .
(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 on and , is played exactly like , but a play counts as a win for the duplicator if and only and satisfy the same unnested atomic formulas.
Recall that an unnested atomic formula for a first-order language of one of the following forms:
for variables and ,
for variable and constant symbol ,
for variables and and function symbol ,
for variables and relation symbol .
Any atomic formula is equivalent to a -formula built from unnested atomic formulas (but the quantifier rank grows with the size of the involved terms).
We write to mean that the duplicator has a winning strategy in the game .
Note that implies 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 has finitely many symbols. Then we can effectively find for each a finite set of unnested formulas in free variables of quantifier rank at most , such that
for every -structure , all , and all -tuples from , there is exactly one formula in with ,
for all and all -structures and and corresponding -tuples and we have if and only if there is satisfied by both and ,
for all it holds that every unnested formula in free variables of quantifier rank at most is equivalent to a disjunction of formulas in .
This appears as Theorem 3.3.2 in Hodges 93.
(Fraïssé‘s theorem) Two structures and in a finite language are elementarily equivalent, , if and only if for every , .
The condition occurring in Fraïssé‘s theorem, that for every , , is nicely captured by another variation of either the ordinary or the unnested Ehrenfeucht-Fraïssé game. Namely, instead of taking an ordinal to be the length of the game, we can let an ordinal 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 on and , , to be a finite game of perfect information, defined by induction on as follows:
for there is a unique play (i.e., the players do nothing) that is a win for the duplicator if and only if ,
for , 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 , where and are the two elements picked, and this play in is a win for duplicator if and only if the play in is a win for duplicator,
for a limit ordinal, a play consists of the spoiler picking an ordinal , and then a continued play in , and this play in is a win for duplicator if and only if the play in is a win for duplicator.
The game is defined similarly, using unnested atomic formulas in the base case.
We write to mean that the duplicator has a winning strategy in the game and to mean that the duplicator has a winning strategy in the game .
We use a subscript to indicate that the relations and form approximations to and , respectively.
There is an alternative characterization of the relations in terms of back-and-forth sequences.
We define a back-and-forth sequence of length from to to be a sequence of inhabited sets of pairs of equal length sequences from and such that
for ,
for every and every we have , and
for every and every and every , there is a such that , and
for every and every and every , there is an such that .
There is a back-and-forth sequence of length from to if and only if .
Clearly, if and 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 can be built using infinitary disjunctions and conjunctions. We write (resp. ) to mean that and satisfy the same sentences of (resp. of quantifier rank at most ).
There is a close relationship between the expressivity of this infinitary logic and the relations and , as the following theorem shows:
We have if and only if and if and only if .
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 July 14, 2021 at 15:41:20. See the history of this page for a list of all contributions to it.