Sit B {\displaystyle B} . Volumus facere series ( ( Φ p , X ¯ p ) ) p ∈ ω {\displaystyle ((\Phi _{p},{\bar {X}}_{p}))_{p\in \omega }} , quorum:
Φ p {\displaystyle \Phi _{p}} est copia finita rerum sicut ( a , b , X ) {\displaystyle (a,b,X)} , in qua a , b ∈ ω {\displaystyle a,b\in \omega } , X ∈ 2 < ω {\displaystyle X\in 2^{<\omega }} . Φ p ( X ) {\displaystyle \Phi _{p}(X)} est functio ab 2 ω {\displaystyle 2^{\omega }} in 2 ω {\displaystyle 2^{\omega }} , ut Φ p ( X ) ( a ) = b {\displaystyle \Phi _{p}(X)(a)=b} si et tantum si ( a , b , X ) ∈ Φ p {\displaystyle (a,b,X)\in \Phi _{p}} ,
X ¯ p {\displaystyle {\bar {X}}_{p}} est copia finita rerum X ∈ 2 ω {\displaystyle X\in 2^{\omega }} ,in qua serie, si q > p {\displaystyle q>p} :
(a) Cuique ( x q , y q , η ) ∈ Φ q ∖ Φ p {\displaystyle (x_{q},y_{q},\eta )\in \Phi _{q}\backslash \Phi _{p}} et ( x p , y p , σ ) ∈ Φ p {\displaystyle (x_{p},y_{p},\sigma )\in \Phi _{p}} , | η | > | σ | {\displaystyle \vert \eta \vert >\vert \sigma \vert } ,
(b) Φ p ⊆ Φ q {\displaystyle \Phi _{p}\subseteq \Phi _{q}} et X ¯ p ⊆ X ¯ q {\displaystyle {\bar {X}}_{p}\subseteq {\bar {X}}_{q}} ,
(c) Cuique X ∈ X ¯ p {\displaystyle X\in {\bar {X}}_{p}} , Φ q ( X ) = Φ p ( X ) {\displaystyle \Phi _{q}(X)=\Phi _{p}(X)} . ita ut, si Φ := ⋃ p ∈ ω Φ p {\displaystyle \Phi :=\bigcup _{p\in \omega }\Phi _{p}} , tum Φ ( B ) = Φ ′ {\displaystyle \Phi (B)=\Phi ^{\prime }} . Sit Φ 0 = X ¯ 0 = ∅ {\displaystyle \Phi _{0}={\bar {X}}_{0}=\varnothing } . Si habemus ( Φ p , X ¯ p ) {\displaystyle (\Phi _{p},{\bar {X}}_{p})} , sic agamus ut ( Φ p + 1 , X ¯ p + 1 ) {\displaystyle (\Phi _{p+1},{\bar {X}}_{p+1})} faciamus:
Sit ∃ n θ p ( n , Z | n ) {\displaystyle \exists n\,\theta _{p}(n,Z\vert n)} formula numero p {\displaystyle p} . Si nancisci possumus copiam Ψ ⊇ Φ {\displaystyle \Psi \supseteq \Phi } quae (a) satisfaciat, ut cuique X ∈ X ¯ p ∪ { B } {\displaystyle X\in {\bar {X}}_{p}\cup \{B\}} , Ψ ( X ) = Φ ( X ) {\displaystyle \Psi (X)=\Phi (X)} , tum sit Φ p + 1 := Ψ ∪ { ( p , 1 , B ) } {\displaystyle \Phi _{p+1}:=\Psi \cup \{(p,1,B)\}} et X ¯ p + 1 := X ¯ p {\displaystyle {\bar {X}}_{p+1}:={\bar {X}}_{p}} .
Sin nancisci non possumus Ψ {\displaystyle \Psi } , tum sciamus cuique copiae Ψ ⊆ Φ {\displaystyle \Psi \subseteq \Phi } quae (a) satisfaciat esse X ∈ X ¯ p ∪ { B } {\displaystyle X\in {\bar {X}}_{p}\cup \{B\}} ut Ψ ( X ) ≠ Φ ( X ) {\displaystyle \Psi (X)\neq \Phi (X)} . Sit igitur collectio Z {\displaystyle {\mathcal {Z}}} ut: Z ¯ ∈ Z ⟺ Sit Ψ ⊇ Φ quae (a) satisfaciat, tum si ∃ n < | Ψ | θ p ( n , Ψ | n ) , tum ∃ ( a , b , X ) ∈ Ψ ∖ Φ , ut X ∈ Z ¯ {\displaystyle {\bar {Z}}\in {\mathcal {Z}}\iff {\text{Sit }}\Psi \supseteq \Phi {\text{ quae (a) satisfaciat, tum si }}\exists n<\vert \Psi \vert \,\theta _{p}(n,\Psi \vert n){\text{, tum }}\exists (a,b,X)\in \Psi \backslash \Phi {\text{, ut }}X\in {\bar {Z}}}
Sed scilicet X ¯ p ∪ { B } ∈ Z {\displaystyle {\bar {X}}_{p}\cup \{B\}\in {\mathcal {Z}}} , ergo Z ≠ ∅ {\displaystyle {\mathcal {Z}}\neq \varnothing } . Lemma habemus:
Lemma. (de conis vitandis ) Sit collectio non vacua A {\displaystyle {\mathcal {A}}} ut X ∈ A ⟺ ∀ n θ ( n , X | n ) {\displaystyle X\in {\mathcal {A}}\iff \forall n\,\theta (n,X\vert n)} , in quo θ ∈ Δ 0 {\displaystyle \theta \in \Delta _{0}} (vide pagina de hierarchia arithmetica ). Sit D ≰ T 0 {\displaystyle D\not \leq _{T}\mathbf {0} } . Tum est G ∈ A {\displaystyle G\in {\mathcal {A}}} ut G ≱ T D {\displaystyle G\not \geq _{T}D} .
Ergo, sit D ¯ = B {\displaystyle {\bar {D}}=B} , tum est Z ¯ ∈ Z {\displaystyle {\bar {Z}}\in {\mathcal {Z}}} ut Z ¯ ≱ T B {\displaystyle {\bar {Z}}\not \geq _{T}B} , id est, B ∉ Z ¯ {\displaystyle B\not \in {\bar {Z}}} . Igitur sit Φ p + 1 = Φ p ∪ { ( p , 0 , B ) } {\displaystyle \Phi _{p+1}=\Phi _{p}\cup \{(p,0,B)\}} et X ¯ p + 1 := X ¯ p ∪ Z ¯ {\displaystyle {\bar {X}}_{p+1}:={\bar {X}}_{p}\cup {\bar {Z}}} . Nunc tota serie facta habemus Φ {\displaystyle \Phi } ut Φ ( B ) = Φ ′ {\displaystyle \Phi (B)=\Phi ^{\prime }} . Ergo Φ ⊕ B ≡ T Φ ′ {\displaystyle \Phi \oplus B\equiv _{T}\Phi ^{\prime }} , quod erat demonstrandum.