Kodowanie lematu Moschovakisa

Lemat kodujący Moschovakisa jest lematem z opisowej teorii mnogości obejmującej zbiory liczb rzeczywistych zgodnie z aksjomatem determinacji (zasada — niezgodna z wyborem — że każda dwuosobowa gra całkowita jest wyznaczona). Lemat został rozwinięty i nazwany na cześć matematyka Yiannisa N. Moschovakisa .

Lemat można ogólnie wyrazić następująco:

Niech Γ będzie niesamodualną klasą punktów zamkniętą pod rzeczywistą kwantyfikacją i ∧ , oraz ≺ Γ -dobrze umotywowaną relacją na ω ^ω rangi θ ∈ ON . Niech R ⊆ dom(≺) × ω ^ω będzie takie, że (∀ x ∈dom(≺))(∃ y )( x R y ) . Wtedy istnieje zbiór Γ A ⊆ dom(≺) × ω ^ω który jest zbiorem wyborów dla R , czyli:

1. (∀ α < θ )(∃ x ∈dom(≺), y )(| x | _≺ = α ∧ x ZA y ) .
2. (∀ x , y ) ( x ZA y → x R y ) .

Dowód przebiega w następujący sposób: załóżmy, że sprzeczność θ jest minimalnym kontrprzykładem, oraz ustalonym ≺ , R , oraz dobrym uniwersalnym zbiorem U ⊆ ( ω ^ω ) ³ dla Γ -podzbiorów ( ω ^ω ) ² . Łatwo, θ musi być graniczną liczbą porządkową. Dla δ < θ , mówimy, że u ∈ ω ^ω koduje zbiór δ -wybór pod warunkiem, że właściwość (1) zachodzi dla α ≤ δ używając A = U u i własność (2) zachodzi dla A = U u gdzie zastępujemy x ∈ dom(≺) przez x ∈ dom(≺) ∧ | x | ≺ [≤ δ ] . Przy minimalności θ dla wszystkich δ < θ istnieją zbiory δ -wyboru.

Teraz zagrajmy w grę, w której gracze I, II wybierają punkty u , v ∈ ω ^ω i II wygrywają, gdy u koduje zbiór δ ₁ -wybór dla pewnego δ ₁ < θ implikuje v koduje zbiór δ ₂ -wybór dla pewnego δ ₂ > δ ₁ . Zwycięska strategia dla I definiuje zbiór Σ
¹ ₁ B kodowania liczb rzeczywistych δ -zbiory wyboru dla dowolnie dużych δ < θ . Zdefiniuj więc

x ZA y ↔ (∃ w ∈ b ) U ( w , x , y ) ,

który z łatwością działa. Z drugiej strony załóżmy, że τ jest zwycięską strategią dla II. Z twierdzenia smn niech s :( ω ^ω ) ² → ω ^ω będzie takie ciągłe , że dla wszystkich ϵ , x , t i w ,

U ( s ( ϵ , x ), t , w ) ↔ (∃ y , z ) ( y ≺ x ∧ U ( ϵ , y , z ) ∧ U ( z , t , w )) .

Z twierdzenia o rekurencji istnieje ϵ ₀ takie, że ₀₀ U ( ϵ , x , z ) ↔ z = τ ( s ( ϵ , x )) . Prosta indukcja po | x | _≺ dla x ∈ dom(≺) to pokazuje

₀ (∀ x ∈dom(≺))(∃! z ) U ( ϵ , x , z ) ,

I

₀ (∀ x ∈dom(≺), z )( U ( ϵ , x , z ) → z koduje zbiór liczb porządkowych do wyboru ≥| x | _≺ ) .

Więc pozwól

₀ x ZA y ↔ (∃ z ∈dom(≺), w )( U ( ϵ , z , w ) ∧ U ( w , x , y )) .