In the mathematical discipline of
model theory, the
Ehrenfeucht–Fraïssé game (also called back-and-forth games) is a technique for determining whether two
structures are
elementarily equivalent. The main application of Ehrenfeucht–Fraïssé games is in proving the inexpressibility of certain properties in first-order logic. Indeed, Ehrenfeucht–Fraïssé games provide a complete methodology for proving inexpressibility results for first-order logic. In this role, these games are of particular importance in
finite model theory and its applications in computer science (specifically
Computer Aided Verification and
database theory), since Ehrenfeucht–Fraïssé games are one of the few techniques from model theory that remain valid in the context of finite models. Other widely used techniques for proving inexpressibility results, such as the
compactness theorem, do not work in finite models.