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: A proof runs as follows: suppose for contradiction θ is a minimal counterexample, and fix ≺, R, and a good universal set U ⊆ (ωω)3 for the Γ-subsets of (ωω)2.
For δ < θ, we say u ∈ ωω codes a δ-choice set provided the property (1) holds for α ≤ δ using A = U u and property (2) holds for A = U u where we replace x ∈ dom(≺) with x ∈ dom(≺) ∧ |x| ≺ [≤δ].
Now, play a game where players I, II select points u,v ∈ ωω and II wins when u coding a δ1-choice set for some δ1 < θ implies v codes a δ2-choice set for some δ2 > δ1.