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.