Wir betrachten die Abbildung
-
die durch
-
festgelegt ist. Bei der Berechnung von wird also zuerst geschaut, ob das erste Argument, also , die Gödelnummer eines arithmetischen Ausdrucks mit genau einer freien Variablen ist. Falls nicht, so ist
,
unabhängig von . Falls ja, so ist also
mit
.
In diesem Ausdruck wird dann die einzige freie Variable durch das zweite Argument der Abbildung, also , ersetzt, wobei man einen Satz erhält. Dessen Gödelnummer ist nach Definition der Wert der Abbildung . In diesem Fall ist also
.
Diese Erläuterungen zeigen zugleich, dass
berechenbar
ist.
Da nach Voraussetzung Repräsentierungen erlaubt, gibt es einen Ausdruck mit drei freien Variablen, der diese Abbildung repräsentiert. D.h. es gilt für jede Belegung der Variablen mit natürlichen Zahlen die Beziehungen
(wir können annehmen, dass
widerspruchsfrei
ist, da andernfalls das Resultat trivial ist)
-
-
und
(für jede Belegung für und )
-
Den Fixpunkt zu einem vorgegebenen
erhalten wir nun durch eine trickreiche Anwendung von . Wir setzen
-
Der Ausdruck besitzt die Gödelnummer . Wir behaupten nun, dass der Satz
-
die zu beweisende Ableitungsbeziehung erfüllt.
Der Ausdruck besitzt die einzige freie Variable , daher gilt
-
Aufgrund der Repräsentierungseigenschaft ist daher
-
Aus der Allaussage erhält man durch
Spezialisierung
(man ersetzt die Variable durch den Term )
-
Da das Antezedens der rechten Implikation aus ableitbar ist, folgt
-
Dies besagt also die Ableitbarkeit der Hinrichtung.
Die aufgrund der Repräsentierbarkeit oben angeführte eindeutige Existenzaussage führt zu
-
Durch
Substitution
ergibt sich
-
und somit nach einer prädikatenlogischen Umformulierung
-
Da hierbei keine freie Variablen besitzt, ist auch
-
und das Sukzedens ist gerade
, sodass auch die Rückrichtung ableitbar ist.