the language, the union of which forms the language itself. For instance, for FO consider classes FO[m] for each m. For each m the above core idea then has to be shown. That is: and with a pair for each and α (in ≡) from FO[m]. It may be appropriate to choose the classes FO[m] to form a partition of the language. 3. One common way to define FO[m] is by means of the quantifier rank qr(α) of a FO formula α, which expresses the depth of quantifier nesting. For example, for a formula in prenex normal form, qr is simply the total number of its quantifiers. Then FO[m] can be defined as all FO formulas α with qr(α) ≤ m (or, if a partition is desired, as those FO formulas with quantifier rank equal to m). 4. Thus it all comes down to showing on the subsets FO[m]. The main approach here is to use the algebraic characterization provided by Ehrenfeucht–Fraïssé games. Informally, these take a single partial isomorphism on A and B and extend it m times, in order to either prove or disprove , dependent on who wins the game. Example We want to show that the property that the size of an ordered structure A = (A, ≤) is even, can not be expressed in FO. 1. The idea is to pick A ∈ EVEN and B ∉ EVEN, where EVEN is the class of all structures of even size. 2. We start with two ordered structures A2 and B2 with universes A2 = {1, 2, 3, 4} and B2 = {1, 2, 3}. Obviously A2 ∈ EVEN and B2 ∉ EVEN. 3. For m = 2, we can now show* that in a 2-move Ehrenfeucht–Fraïssé game on A2 and B2 the duplicator always wins, and thus A2 and B2 cannot be discriminated in FO[2], i.e. A2 α ⇔ B2 α for every α ∈ FO[2]. 4. Next we have to scale the structures up by increasing m. For example, for m = 3 we must find an A3 and B3 such that the duplicator always wins the 3-move game. This can be achieved by A3 = {1, ..., 8} and B3 = {1, ..., 7}. More generally, we can choose Am = {1, ..., 2m} and Bm = {1, ..., 2m-1}; for any m the duplicator always wins the m-move game for this pair of