Ehrenfeucht Fraïssé Games on Linear Orderings

The Ehrenfeucht Fraïssé Game on Finite Linear Orderings: A game about First-Order Logic and the inevitable end of all things.

The Ehrenfeuchts (dots above the river) and Fraïssés (dots below the river) are separated by a river! Together, two players will work to connect the Ehrenfeuchts and Fraïssés by bridges. This is an asymmetric game for two players with very distinct roles: 

• Player 1 is called Selector. On their turn, Selector selects either an Ehrenfeucht or a Fraïssé (dot above or below the river) that hasn't been connected by a bridge yet. 

• Player 2 is called Bridger. On their turn, Bridger picks a dot on the other side of the river that hasn't been connected yet, and connects it to the dot Selector picked via a bridge. Bridges cannot cross. 

If either player cannot pick a dot, the game is over.

The two players also have very distinct goals: Player 1 (Selector)'s goal is to end the game as quickly as possible. Player 2 (Bridger)'s goal is to keep the game going as long as possible.

What's going on? Ehrenfeucht Fraïssé Games are a key tool in Model Theory, a branch of mathematical logic concerned with what logical statements are true or false for various mathematical structures. Player 1 (who is called Spoiler in Model Theory)'s goal is to exploit the differences between the collection of dots above the river and the collection of dots below. Player 2 (who is called Duplicator in Model Theory) then tries to take advantage of the similarities between the two collections of dots.

For instance, suppose that there are 2 dots above the river and three dots below. The difference Player 1 will try to exploit is that in the 3 dot collection, there is a point which is neither furthest to the left or to the right, or, written in the language of logic, there is a dot x such that there is a dot y with y > x and there is a dot y with y < x. This difference has two variables in it, and it takes Player 1 two turns to exploit it. This isn't a coincidence: any difference becomes a strategy for player 1, and it takes one turn for each variable needed to write it down.

Hence the purpose of the game: it's sometimes easier to figure out the winning strategy on a game than it is to figure out the logical difference between two structures. A model theorist can then turn that strategy into a logical formula describing the difference.

The collections of dots above and below the river do not have to be finite: any subset of the real number line will do, including the positive integers, the integers, the rational numbers, etc.