• Games used to show that two structures are rank-q equivalent in FOL via game semantics.
• We make a restriction: we assume that the theory contains no function symbols. Recall that function symbols can be encoded via relations, so no expressive power is lost, merely annoynance is thwarted.
• If we had function symbols also, then we would need to perform induction on function call nesting depth as well as quantifier depth, and our completion of the substructre would need to complete by function symbols also.

• One direction is easy: if two models are rank q equivalent, then they are also game-round-q equivalent.

§ Game equivalence implies rank equivalence

• We prove by contrapositive. Assume the two models are rank-k disequivalent (so there is a formula of that rank that distinguishes the models), we will show that the models are game-k disequivalent (so there is a winning strategy for spoiler.)

§ Example 0: Rank 0 equivalence

• Suppose we have a theory with no constant symbols. Then, at rank 0, it's impossible to tell them apart, because we cannot write any propositional equations about them!
• So suppose a theory $T$ does have a constant symbol c. Now suppose we have two model M, M' which are not rank-0 equivalent. This means that some propositional formula, involving c, can tell the two models apart. Call the formula f. Then it must be the case that WLOG, M |= f and M' !|= f.
• Now, from the view of the game, this means that we play a round 0 game, and build an empty partial isomorphism between the two models M, M'. What do we compare?
• Fear not, we must generate the substructure from the empty partial iso, which will be the submodel of M (say C for contradiction) which only has the symbol c, and similarly M' has submodel C' which has only c'.
• Now, the formula f, when evaluated on the submodel C will be true, and when evaluated on C' will be false!
• Thus, game-0 equivalence iff rank-0 equivalence.

§ Example 1: Existential Rank 1 equivalence

• Suppose the two models are rank-1 disequivalent, and this formula that shows their disequivalence is an existential formula. Let the formula be f := exists x, f'. Suppose WLOG that M |= f and M' !|= f.
• What does this mean? This means that there is some element m in M such that M |= f'(m). It also means that for all m' in M', M' !|= f'(m').
• So, for the spoiler to win, it needs to pick a submodel C of M that contains m, since any submodel C' of M' will not be able to model f'!
• that's exactly what the spoiler does: it pick m in M. Now whatever m' duplicator chooses, the formula exists x, f' can tell them apart: the formula is true in C'and will be false in all choices of C' that duplicator can make!
• Note that in this case, spoiler chose an element m in M.

§ Example 2: Universal Rank 1 equivalence

• Suppose the two models are rank-1 disequivalent, and this formula that shows their disequivalence is a universal formula. Let the formula be f := forall x, f'. Suppose WLOG that M |= f and M' !|= f.
• What does this mean? This means that for every element m in M, it is true that M |= f'(m). It also means that there is some element m' in M' such that M' !|= f'(m').
• So, now, spoiler chooses m'. This way, spoiler ensures that it gets a submodel C' where C' !|= forall x, f' since we have m' in c' such that C' |= f'(m').
• Duplicator cannot win, since for any submodel C of M it chooses, it must be the case that C' |= forall m, f', since for every element m in M (and thus m in C), we have that M |= f'(m), and thus C |= f'(m).
• Note that in this case, spoiler chose an element m' in M'.

§ Full Proof Sketch

• See that spoiler really needs the ability to pick from both M and M' to corner duplicator.
• Clearly, one can see how to generalize this to an induction. So perform the induction, replacing the level 1 case with an inductive case.
• Note that the spoiler needs to be able to choose elements from either set to be able to correctly.