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

Aus Wikiversity
Zur Navigation springen Zur Suche springen
Beweis

Es sei eine -entscheidbare Relation und es sei ein Registerprogramm mit den Registern das diese Relation entscheidet. Aufgrund von Fakt gibt es einen arithmetischen Ausdruck in freien Variablen, der den Programmablauf arithmetisch modelliert. Es gilt also genau dann, wenn , angesetzt auf (strenggenommen angesetzt auf , wenn man die vollständige Registerbelegung angibt) anhält mit der Ausgabe (d.h. ; andernfalls wird mit der Ausgabe angehalten), genau dann, wenn gilt.

Wegen der Vollständigkeit von bedeutet dies, dass

die Relation repräsentiert.
Es sei

eine -berechenbare Abbildung und es sei ein Registerprogramm, dass berechnet. Aufgrund von Fakt gibt es einen arithmetischen Ausdruck in freien Variablen, der den Programmablauf arithmetisch modelliert. D.h. für jedes -Tupel gilt

genau dann, wenn das Programm bei jeder Eingabe anhält und angesetzt auf (in den ersten Registern, die Eingabe ist also ) die Ausgabe (also ) besitzt, genau dann, wenn

gilt. Von daher ist der Ausdruck (in den freien Variablen )

Da eine Funktion vorliegt und vollständig ist, gilt auch