Natürliche Arithmetik/Erlaubt Repräsentierungen/Fakt/Beweis

Beweis

Es sei ${}T\subseteq \mathbb {N} ^{r}$ eine ${}R$ -entscheidbare Relation und es sei ${}P$ ein Registerprogramm mit den Registern ${}R_{0},R_{1},\ldots ,R_{m}$ das diese Relation entscheidet. Aufgrund von Fakt gibt es einen arithmetischen Ausdruck ${}\psi _{P}$ in ${}2m$ freien Variablen, der den Programmablauf arithmetisch modelliert. Es gilt also ${}(n_{1},\ldots ,n_{r})\in T$ genau dann, wenn ${}P$ , angesetzt auf ${}(n_{1},\ldots ,n_{r})$ (strenggenommen angesetzt auf $(1,n_{1},\ldots ,n_{r},0,\ldots ,0)$ , wenn man die vollständige Registerbelegung angibt) anhält mit der Ausgabe ${}0$ (d.h. $(h,0,n'_{2},\ldots ,n'_{m})$ ; andernfalls wird mit der Ausgabe ${}1$ angehalten), genau dann, wenn ${}\mathbb {N} \vDash \psi _{P}(n_{1},\ldots ,n_{r},0,\ldots ,0,0,n'_{2},\ldots ,n'_{m})$ gilt.

Wegen der Vollständigkeit von ${}\mathbb {N}$ bedeutet dies, dass

{}\theta _{P}=\exists y_{2}\ldots \exists y_{m}\psi _{P}(x_{1},\ldots ,x_{r},0,\ldots ,0,0,y_{2},\ldots ,y_{m})\,

die Relation repräsentiert.
Es sei

F\colon \mathbb {N} ^{r}\longrightarrow \mathbb {N} ^{s}

eine ${}R$ -berechenbare Abbildung und es sei ${}P$ ein Registerprogramm, dass ${}F$ berechnet. Aufgrund von Fakt gibt es einen arithmetischen Ausdruck ${}\psi _{P}$ in ${}2m$ freien Variablen, der den Programmablauf arithmetisch modelliert. D.h. für jedes ${}(r+s)$ -Tupel ${}n_{1},\ldots ,n_{r+s}$ gilt

{}F(n_{1},\ldots ,n_{r})=(n_{r+1},\ldots ,n_{r+s})\,

genau dann, wenn das Programm ${}P$ bei jeder Eingabe anhält und angesetzt auf ${}(n_{1},\ldots ,n_{r})$ (in den ersten ${}r$ Registern, die Eingabe ist also $(1,n_{1},\ldots ,n_{r},0,\ldots ,0)$ ) die Ausgabe ${}(n_{r+1},\ldots ,n_{r+s})$ (also $(h,n_{r+1},\ldots ,n_{r+s},\ell _{m+s+1},\ldots ,\ell _{2m})$ ) besitzt, genau dann, wenn