Fontem paginae Theorema Posner–Robinson inspicere

'''Theorema Posner–Robinson''' est theorema [[theoria facultatis calculandi|theoriae facultatis calculandi]] de [[gradus Turing|gradibus Turing]].

== Expositio ==
'''Theorema.''' Sit <math>B</math> copia numerorum naturalium, quae calculari non potest. (Id est <math>B\not\le_T \mathbf{0}</math>.) Tum est copia <math>G</math> ut
<math>G\oplus B\equiv_T G^\prime</math>.

== Demonstratio ==
Sit <math>B</math>. Volumus facere series <math>((\Phi_p,\bar X_p))_{p\in\omega}</math>, quorum:
* <math>\Phi_p</math> est copia finita rerum sicut <math>(a, b, X)</math>, in qua <math>a,b\in\omega</math>, <math>X\in 2^{<\omega}</math>. <math>\Phi_p(X)</math> est functio ab <math>2^\omega</math> in <math>2^\omega</math>, ut <math>\Phi_p(X)(a)=b</math> si et tantum si <math>(a,b,X)\in\Phi_p</math>,
* <math>\bar X_p</math> est copia finita rerum <math>X\in 2^\omega</math>,
in qua serie, si <math>q>p</math>:
* (a) Cuique <math>(x_q,y_q,\eta)\in\Phi_q\backslash\Phi_p</math> et <math>(x_p,y_p,\sigma)\in\Phi_p</math>, <math>\vert\eta\vert>\vert\sigma\vert</math>,
* (b) <math>\Phi_p\subseteq\Phi_q</math> et <math>\bar X_p\subseteq\bar X_q</math>,
* (c) Cuique <math>X\in\bar X_p</math>, <math>\Phi_q(X)=\Phi_p(X)</math>.
ita ut, si <math>\Phi := \bigcup_{p\in\omega}\Phi_p</math>, tum <math>\Phi(B)=\Phi^\prime</math>. Sit <math>\Phi_0 = \bar X_0 = \varnothing</math>. Si habemus <math>(\Phi_p,\bar X_p)</math>, sic agamus ut <math>(\Phi_{p+1},\bar X_{p+1})</math> faciamus:
# Sit <math>\exists n\,\theta_p(n,Z\vert n)</math> formula numero <math>p</math>. Si nancisci possumus copiam <math>\Psi\supseteq\Phi</math> quae (a) satisfaciat, ut cuique <math>X\in\bar X_p\cup\{B\}</math>, <math>\Psi(X)=\Phi(X)</math>, tum sit <math>\Phi_{p+1}:=\Psi\cup\{(p,1,B)\}</math> et <math>\bar X_{p+1}:=\bar X_p</math>.
# Sin nancisci non possumus <math>\Psi</math>, tum sciamus cuique copiae <math>\Psi\subseteq\Phi</math> quae (a) satisfaciat esse <math>X\in\bar X_p\cup\{B\}</math> ut <math>\Psi(X)\ne\Phi(X)</math>. Sit igitur collectio <math>\mathcal{Z}</math> ut:
:::<math>\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</math>
::Sed scilicet <math>\bar X_p\cup\{B\}\in\mathcal{Z}</math>, ergo <math>\mathcal{Z}\ne\varnothing</math>. Lemma habemus:
:::'''Lemma.''' (''de conis vitandis'') Sit collectio non vacua <math>\mathcal{A}</math> ut <math>X\in\mathcal{A}\iff\forall n\,\theta(n,X\vert n)</math>, in quo <math>\theta\in\Delta_0</math> (vide pagina de [[hierarchia arithmetica]]). Sit <math>D\not\le_T\mathbf{0}</math>. Tum est <math>G\in\mathcal{A}</math> ut <math>G\not\ge_T D</math>.
::Ergo, sit <math>\bar D=B</math>, tum est <math>\bar Z\in\mathcal{Z}</math> ut <math>\bar Z\not\ge_T B</math>, id est, <math>B\not\in\bar Z</math>. Igitur sit <math>\Phi_{p+1}=\Phi_p\cup\{(p,0,B)\}</math> et <math>\bar X_{p+1}:=\bar X_p\cup\bar Z</math>.
Nunc tota serie facta habemus <math>\Phi</math> ut <math>\Phi(B)=\Phi^\prime</math>. Ergo <math>\Phi\oplus B\equiv_T\Phi^\prime</math>, quod erat demonstrandum.

== Significatio ==
Hoc theorema naturam omnium copiarum quae calculari non possunt patefacit. Si <math>B</math> est copia quae calculari non potest, tum nancisci possumus copia <math>G</math>, ut differentia inter <math>G</math> et <math>G^\prime</math> sit <math>B</math>.

[[Categoria:Theoremata mathematica]]
[[Categoria:Logica]]