Friedman–Moschovakis coding game

The Friedman–Moschovakis coding game turns strategies into codes for sets of ordinals. An explicit ${\omega }_1$ instance makes its mechanism visible. Fix $A\subseteq {\omega }_1$. Let a real $y$ code a countable well-order together with a marked subset of its domain. Write $E(y,z)$ when the rank of the well-order code $z$ is the rank of a marked element in that coded order. A suitable $y$ can therefore code $A\cap \eta$ for any particular countable ordinal $\eta$.

Players I and II produce reals $x,y$. Player II wins if $x\notin \mathrm{WF}$, or if $y$ correctly codes membership in $A$ through rank $\Vert x\Vert$: for every $z\in \mathrm{WF}$ with $\Vert z\Vert \le \Vert x\Vert$,A winning strategy for Player I would produce only well-order codes. Its possible outputs form an analytic set, so their ranks are bounded by the boundedness theorem for well-order codes. Player II could then play one real coding $A$ through a larger countable rank, defeating the strategy. Under the axiom of determinacy, Player II consequently has a winning strategy.

Such a strategy determines at most one $A$: play any code of an ordinal $\xi$ against it and inspect its response at rank $\xi$. Strategies themselves are coded by reals, giving the coding consequence for subsets of ${\omega }_1$. The general Friedman–Moschovakis coding lemma replaces these countable-order codes and analytic boundedness by the corresponding uniform coding and covering machinery; independently choosing unrelated codes for every initial segment does not supply that uniformity.^[ref]