Moschovakis coding lemma


The Moschovakis coding lemma is a lemma from descriptive set theory involving sets of real numbers under the axiom of determinacy. The lemma was developed and named after the mathematician Yiannis N. Moschovakis.
The lemma may be expressed generally as follows:
  1. .
  2. .
A proof runs as follows: suppose for contradiction is a minimal counterexample, and fix,, and a good universal set for the -subsets of. Easily, must be a limit ordinal. For, we say codes a -choice set provided the property holds for using and property holds for where we replace with. By minimality of, for all, there are -choice sets.
Now, play a game where players I, II select points and II wins when coding a -choice set for some implies codes a -choice set for some. A winning strategy for I defines a set of reals encoding -choice sets for arbitrarily large. Define then
which easily works. On the other hand, suppose is a winning strategy for II. From the s-m-n theorem, let be continuous such that for all,,, and,
By the recursion theorem, there exists such that. A straightforward induction on for shows that
and
So let