Moschovakis coding lemma
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 principle — incompatible with choice — that every two-player integer game is determined). The lemma was developed and named after the mathematician Yiannis N. Moschovakis.
The lemma may be expressed generally as follows: :Let be a non-selfdual pointclass closed under real quantification and , and a -well-founded relation on of rank . Let be such that . Then there is a -set which is a choice set for R, that is:
. # . 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 (1) holds for using and property (2) 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 :.