 Solution

The quantifier rank measures maximum nesting depth:Two first-order structures are rank-n equivalent if they agree on all first-order sentences of quantifier rank at most $n$. For tuples one similarly compares all such formulas evaluated at the tuples.

In the $n$-round Ehrenfeucht-Fraïssé game, player I, the Spoiler, chooses an element from either structure each round; player II, the Duplicator, chooses an element in the other. After $n$ rounds the corresponding chosen tuples must define a partial isomorphism of structures: all atomic formulas, including equality and the interpretations of constants, have matching truth values. Repetitions must be respected. Failure of this condition is a loss for II.

The precise finite-vocabulary Ehrenfeucht-Fraïssé theorem is: for a finite relational language, allowing finitely many constants,The tuple version has the same conclusion when the corresponding tuples are fixed before play. The implication from a winning strategy to rank equivalence holds for arbitrary languages, by induction on formulas. For the converse, finite relational vocabulary ensures only finitely many rank-bounded types in a fixed tuple of variables; their defining formulas let one transfer the type of the next move. Without a finiteness hypothesis, the converse for the full atomic-diagram game need not hold. This qualification matters in the next part.