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 {{mvar|Γ}} be a non-selfdual pointclass closed under real quantification and {{math|∧}}, and {{math|≺}} a {{mvar|Γ}}-well-founded relation on {{math|ω^ω}} of rank {{math|θ ∈ ON}}. Let {{math|R ⊆ dom(≺) × ω^ω}} be such that {{math|(∀x∈dom(≺))(∃y)(x R y)}}. Then there is a {{mvar|Γ}}-set {{math|A ⊆ dom(≺) × ω^ω}} which is a choice set for R, that is:

1. {{math|(∀α<θ)(∃x∈dom(≺),y)({{mabs|x}}_≺{{=}}α ∧ x A y)}}.
2. {{math|(∀x,y)(x A y → x R y)}}.

A proof runs as follows: suppose for contradiction {{mvar|θ}} is a minimal counterexample, and fix {{math|≺}}, {{math|R}}, and a good universal set {{math|U ⊆ (ω^ω)³}} for the {{mvar|Γ}}-subsets of {{math|(ω^ω)²}}. Easily, {{mvar|θ}} must be a limit ordinal. For {{math|δ < θ}}, we say {{math|u ∈ ω^ω}} codes a {{mvar|δ}}-choice set provided the property (1) holds for {{math|α ≤ δ}} using {{math|A {{=}} U u}} and property (2) holds for {{math|A {{=}} U u}} where we replace {{math|x ∈ dom(≺)}} with {{math|x ∈ dom(≺) ∧ {{mabs|x}} ≺ [≤δ]}}. By minimality of {{mvar|θ}}, for all {{math|δ < θ}}, there are {{math|δ}}-choice sets.

Now, play a game where players I, II select points {{math|u,v ∈ ω^ω}} and II wins when {{mvar|u}} coding a {{math|δ₁}}-choice set for some {{math|δ₁ < θ}} implies {{mvar|v}} codes a {{math|δ₂}}-choice set for some {{math|δ₂ > δ₁}}. A winning strategy for I defines a {{math|Σ{{su|b=1|p=1}}}} set {{mvar|B}} of reals encoding {{mvar|δ}}-choice sets for arbitrarily large {{math|δ < θ}}. Define then

:{{math|x A y ↔ (∃w∈B)U(w,x,y)}},

which easily works. On the other hand, suppose {{mvar|τ}} is a winning strategy for II. From the s-m-n theorem, let {{math|s:(ω^ω)² → ω^ω}} be continuous such that for all {{mvar|ϵ}}, {{mvar|x}}, {{mvar|t}}, and {{mvar|w}},

:{{math|U(s(ϵ,x),t,w) ↔ (∃y,z)(y ≺ x ∧ U(ϵ,y,z) ∧ U(z,t,w))}}.

By the recursion theorem, there exists {{math|ϵ₀}} such that {{math|U(ϵ₀,x,z) ↔ z {{=}} τ(s(ϵ₀,x))}}. A straightforward induction on {{math|{{mabs|x}}_≺}} for {{math|x ∈ dom(≺)}} shows that

:{{math|(∀x∈dom(≺))(∃!z)U(ϵ₀,x,z)}},

and

:{{math|(∀x∈dom(≺),z)(U(ϵ₀,x,z) → z encodes a choice set of ordinal ≥{{mabs|x}}_≺)}}.

So let

:{{math|x A y ↔ (∃z∈dom(≺),w)(U(ϵ₀,z,w) ∧ U(w,x,y))}}.{{cite book

| last =Babinkostova

| first =Liljana

| title =Set Theory and Its Applications

| publisher =American Mathematical Society

| date =2011

| language =English

| isbn =978-0821848128

}}{{cite book

| last1 =Foreman

| first1 =Matthew

| author1-link =Matthew Foreman

| last2 =Kanamori

| first2 =Akihiro

| author2-link =Akihiro Kanamori

| title =Handbook of Set Theory

| publisher =Springer

| date =October 27, 2005

| pages =2230

| url =http://www.math.unt.edu/~sjackson/papers/strad_27.pdf

| isbn =978-1402048432

}}{{cite book

| last =Moschovakis

| first =Yiannis

| contribution =Ordinal games and playful models

| title = Cabal Seminar 77 – 79: Proceedings, Caltech-UCLA Logic Seminar 1977 – 79

| series =Lecture Notes in Mathematics

|editor1= Alexander S. Kechris |editor2=Donald A. Martin |editor3=Yiannis N. Moschovakis

| volume =839

| pages =169–201

| publisher =Springer

| location =Berlin

| date =October 4, 2006

| isbn =978-3-540-38422-9

| doi = 10.1007/BFb0090241

}}