A game-theoretic proof of Fraïssé's Theorem
One of the important outcomes of the Fraïssé approach to model theory is that it is possible, in principle, to develop model theory from a strictly structural perspective, without ever mentioning formulas and their semantics. In practice, nobody really goes that far, but it is very useful to know about this radically different way to think about model theory. The key result that allows one to eliminate formulas is Fraïssé’s Theorem, which gives a combinatorial way to characterize when two structures with the same signature satisfy the same sentences. Ehrenfeucht, a student of Fraïssé, came up with a particularly elegant way to formulate Fraïssé’s ideas in terms of what are now called Ehrenfeucht–Fraïssé (EF) games (defined below).
Fraïssé’s Theorem. Let and be two relational structures with the same signature. Duplicator has a winning strategy in the EF game if and only if and satisfy the same sentences of quantifier depth at most . Therefore, and are elementarily equivalent if and only if Duplicator has a winning strategy in all of the EF games .
There are now many proofs of Fraïssé’s Theorem. Since the theorem mentions formulas and satisfaction, it is impossible to prove this result without talking about syntax and semantics. Most of the proofs I have seen use classical semantics à la Tarski. However, there are some alternatives to classical semantics. One such alternative are game semantics à la Hintikka. Since Fraïssé’s Theorem is so elegantly stated in terms of games, this seems like a very suitable choice.
It turns out that the game-theoretic proof of the forward implication of Fraïssé’s Theorem is rather short and elegant, at least when compared to the classical proof.1 The the approach is certainly not new, but I don’t remember if I got the idea from somewhere or if I pieced it together myself. In any case, since this proof is hard to find, I am posting it here for everyone to enjoy.2
Let’s start with some conventions. Fix a relational first-order language . (Constants can be added without trouble, but functions are a bit of a pain.) Throughout, and will denote two structures for the language . If is an atomic relation symbol, write and for the interpretation of in and respectively.
First, recall the definition of the Ehrenfeucht–Fraïssé (EF) game . This is a -round game between two players Spoiler and Duplicator. On the -th round:
- Spoiler picks some or some .
- Duplicator picks some or some (the opposite of Spoiler’s choice).
After the rounds have been played, Duplicator wins if the correspondence defines a finite partial isomorphism from to ; otherwise, Spoiler wins. In particular, we need that for this map to be well-defined and injective.
To simplify certain technical issues, we will use the fact that every formula is equivalent to a formula with the same quantifier depth wherein negations only occur immediately before atomic relation symbols. It follows that it suffices to prove Fraïssé’s Theorem for the class of formulas obtained by closing the literals (atomic relations and their negations) under conjunction, disjunction, universal and existential quantification. We will call these restricted formulas of .3
Let be a restricted formula of with free variables in and let be a variable assignment in the structure . The semantic game , between two players True and False, is defined by induction on the complexity of .
- If where is a -ary literal and , then True wins if holds, otherwise False wins.
- If then False chooses . Then the two players play the subgame .
- If then True chooses . Then the two players play the subgame .
- If then False chooses and adds to the variable assignment, replacing any previous assignment to . Then the two players play the subgame .
- If then True chooses and adds to the variable assignment, replacing any previous assignment to . Then the two players play the subgame .
Note that the variable assignment is a tacit parameter to the game . It is easy to show that True has a winning strategy in the game if and only if (with the implicit variable assignment).
We are now ready to prove the forward implication of Fraïssé’s Theorem. Suppose that Duplicator has a winning strategy in the game . Let be a restricted sentence of , with quantifier depth at most , such that . Then True has a winning strategy in the game . We will use this strategy together with Duplicator’s winning strategy in to define a winning strategy for True in . The strategy is defined by deconstructing and keeping track of a play of the EF game on the side.
Since is a sentence, we start the games and with the empty variable assignment. We will play and in parallel in such a way that both games see the same formula at all times. Suppose we have reached the subformula of .
- If then we let False play in by choosing , and we copy False’s move to .
- If then we use True’s strategy in to choose , and we copy this move to as part of True’s strategy.
- If then we let False play in by choosing . We let this be Spoiler’s next move in our EF game . We then use Duplicator’s strategy in to pick . We let this be False’s next move in .
- If then we use True’s strategy in to choose . We let this be Spoiler’s next move in our EF game .
We then use Duplicator’s strategy in to pick . We choose this as the next move in True’s strategy for . The game ends when is a literal. Since has quantifier depth at most , we have played at most moves in the EF game . (If desired, finish this game by picking arbitrary moves for Spoiler and using Duplicator’s winning strategy to respond.) Suppose . Since we always used True’s winning strategy to play in , we know that holds.
Now observe that by the way we played the quantifier moves, we have the correspondences in the play of the EF game . Since we always used Duplicator’s winning strategy in , this correspondence is a finite partial isomorphism from to , in particular iff . Therefore, and True wins the play of . Since we always let False play freely in , this shows that we have defined a winning strategy for True. Therefore, , as required.
The original version of this post claimed to have a game-theoretic proof of the backward implication of Fraïssé’s Theorem. Unfortunately, that proof was flawed and it has now been deleted. ↩
This proof was originally developed for a REU that I supervised at Cornell University in Summer 2008. It was originally posted on a blog that I used to maintain some years ago. Since I find this proof very interesting, I decided to salvage it and repost it here. ↩
The use of restricted formulas is a little bit of a cheat. The main reason for this was to simplify the definition of the semantic games. Negations can be incorporated in these games by adding the following clause to the definition of : if , then True and False swap roles and play the subgame . The rest of the proof works exactly in the same way, except that because True and False swap roles every time they hit a negation, it becomes tricky to keep track of who is who. ↩
Andreas Blass wrote
It seems to me that you’ve essentially proved one direction of the theorem twice and ignored the other. You’ve shown that if Duplicator has a winning strategy then A and B are n-quantifier equivalent, and that if A and B are not n-quantifier equivalent then Spoiler has a winning strategy. But the theorem also claims that if Duplicator has no winning strategy (equivalently since the game is finite: if Spoiler has a winning strategy) then A and B are not n-quantifier equivalent. As far as I can see, your argument doesn’t establish this. (If I remember correctly, this is the part of the proof where function symbols make life unpleasant. One has to count applications of function symbols as if they were quantifiers, to ensure that there are only finitely many inequivalent formulas of any fixed quantifier depth.)
Thanks Andreas! You are completely correct, I had proved the forward implication and then its contrapositive. I have deleted the redundant proof.
I wonder if there is a game-theoretic proof of the backward implication…