Ehrenfeucht–Fraïssé game

Summary

The Ehrenfeucht–Fraïssé game is a two-player game played on two structures of the same signature. One player, Spoiler, tries to show that the structures differ, and the other, Duplicator, tries to show that they look alike. For a finite relational signature, Duplicator wins the $n$-round game exactly when the structures satisfy the same sentences of quantifier depth at most $n$. The game is a main tool to prove that a property is not first-order definable, in particular in finite model theory.