= Solution
The <quantifier rank> measures maximum nesting depth:
$$
\begin{aligned}
\operatorname{qr}(\theta)&=0 &&\text{for atomic }\theta,\\
\operatorname{qr}(\neg\varphi)&=\operatorname{qr}(\varphi),\\
\operatorname{qr}(\varphi\wedge\psi)&=\operatorname{qr}(\varphi\vee\psi)=\max(\operatorname{qr}(\varphi),\operatorname{qr}(\psi)),\\
\operatorname{qr}(\exists x\varphi)&=\operatorname{qr}(\forall x\varphi)=1+\operatorname{qr}(\varphi).
\end{aligned}
$$
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: \b[for a finite relational language, allowing finitely many constants,]
$$
\boxed{\mathcal M\equiv_n\mathcal N\iff\text{II has a winning strategy in }G_n(\mathcal M,\mathcal N).}
$$
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.
Back to article page
