Ehrenfeucht-Fraisse Theorem

The Ehrenfeucht-Fraisse Theorem describes a back-and-forth game, with the back-and-forth method introduced by Roland Fraisse and formulated as a game by Andrzej Ehrenfeucht, used to determine whether two mathematical structures are elementarily equivalent, meaning they satisfy exactly the same first-order sentences. Two players, conventionally called Spoiler and Duplicator, alternately choose elements from each structure, and the theorem states that Duplicator has a winning strategy in the game of every finite length exactly when the two structures are elementarily equivalent, making the game one of the principal tools for proving that certain properties cannot be expressed in first-order logic.