Ehrenfeucht-Fraïssé Games

We start this chapter by giving a few examples of inexpressibility proofs, using the standard model-theoretic machinery (compactness, the Löwenheim-Skolern theorem). We then show that this machinery is not generally applicable in the finite model theory context, and introduce the notion of Ehrenfeucht-Fraïssé games for first-order logic. We prove the EhrenfeuchtFraïssé theorem, characterizing the expressive power of FO via games, and introduce the notion of types, which will be central throughout the book.