Ehrenfeucht-Fraïssé Games on Läuchli-Leonard Linear Orderings

Gaze into the infinite with Ehrenfeucht-Fraïssé Games on Läuchli-Leonard Linear Orderings

Playing

The Ehrenfeucht-Fraïssé Game is a game about first order logic. Players take turns matching up the points of two linear orderings. The two linear orderings are shown above each other in the same window, one in the top half and the other in the bottom half.

1. First, Player I (Spoiler) selects a point in either linear ordering that has yet to be selected, and colors it a new color.
2. Next, Player II (Duplicator) selects a point in the other linear ordering that has yet to be selected, and colors it the same color and draws a line between the two points.

Lines cannot cross, and players cannot select points that have already been picked. The game ends if either player cannot move. Spoiler's (Player I's) goal is to end the game as quickly as possible. Duplicator's (Player II's) goal is to last as long as possible.

Controls

Many of the linear orderings in this game are infinite and in order to access all their points, you're going to need to zoom in. The top and bottom linear orderings pan and zoom independently.

• Zoom in or out with the mouse wheel.
• Pan by clicking and dragging.
• Click on a point to move there.
• Arrows will appear on the left and right edges of the linear orderings to indicate that the linear ordering continues in that direction. Click on them to zoom out in that direction.

Turns Remaining

Because the linear orderings are infinite, it's possible for the game to go on forever. There are three possible ways of resolving this:

• Players determine between themselves if the game will go on forever, and if it does, duplicator is declared victor.
• Players agree before starting the game a maximum number of turns. If duplicator can last that number of turns, they win.
• Spoiler decides before starting the game a maximum number of turns. If duplicator can last that number of turns, they win.

For the later two options, a turn timer is available. Check the "Show Turns Timer" box under options.

Linear Order Creator

The linear orderings you can play on are those which appear in the theorem of Läuchli and Leonard, which, in some sense capture the interesting linear orderings to play EF games on. They include some basic linear orderings:

• Finite linear orderings (n): We use numbers to represent the linear ordering with that many points (including 0).
• Omega (ω): An infinite linear ordering that goes off infinitely to the right (the ordering of the positive integers): 
• Omega-Star (ω*): An infinite linear ordering that goes off infinitely to the left (the ordering of the negative integers): 
• Zeta (ζ): An infinite linear ordering that goes off infinitely to the left and right (the ordering of the integers): 
• Eta (η): An infinite linear ordering where between any two points can be found another point (the ordering of the rational numbers, although points have been spread out for clarity): 

From these basic linear orderings, one can obtain the full collection of Läuchli-Leonard linear orderings by freely applying the following operations:

• Concatenation (+): This operation puts linear orderings next to each other, in the order that they are added.
• Omega Copies (⋅ω): This operation starts with the linear order ω and replaces every point by the linear order being copied, producing infinitely many copies of the original linear ordering going off to the right.
• Omega-Star Copies (⋅ω*): This operation starts with the linear order ω* and replaces every point by the linear order being copied, producing infinitely many copies of the original linear ordering going off to the left.
• Shuffle (σ): This operation takes any number of linear orderings and replaces the points of η in such a way that between every two points of the original η is a copy of each of the linear orderings being shuffled together.