Arithmetische Satzmenge/Repräsentierungen/Fixpunktsatz/Fakt/Beweis

Beweis

Wir betrachten die Abbildung

$F\colon \mathbb {N} \times \mathbb {N} \longrightarrow \mathbb {N} ,\,(m,n)\longmapsto F(m,n),$

die durch

$F(m,n):={\begin{cases}GN(\alpha (n)),\,{\text{ falls }}m{\text{ die }}GN{\text{ eines }}\alpha \in L_{1}^{\rm {Ar}}{\text{ ist}}\,,\\0{\text{ sonst}}\,,\end{cases}}\,$

festgelegt ist. Bei der Berechnung von ${}F$ wird also zuerst geschaut, ob das erste Argument, also ${}m$, die Gödelnummer eines arithmetischen Ausdrucks mit genau einer freien Variablen ist. Falls nicht, so ist ${}F(m,n)=0$, unabhängig von ${}n$. Falls ja, so ist also ${}m=GN(\alpha )$ mit ${}\alpha \in L_{1}^{\rm {Ar}}$. In diesem Ausdruck wird dann die einzige freie Variable durch das zweite Argument der Abbildung, also ${}n$, ersetzt, wobei man einen Satz ${}\alpha (n)$ erhält. Dessen Gödelnummer ist nach Definition der Wert der Abbildung ${}F(m,n)$. In diesem Fall ist also ${}F(m,n)=GN(\alpha (n))$. Diese Erläuterungen zeigen zugleich, dass ${}F$ berechenbar ist.
Da ${}\Gamma$ nach Voraussetzung Repräsentierungen erlaubt, gibt es einen Ausdruck ${}\varphi (x,y,z)$ mit drei freien Variablen, der diese Abbildung repräsentiert. D.h. es gilt für jede Belegung der Variablen mit natürlichen Zahlen ${}m,n,k$ die Beziehungen (wir können annehmen, dass ${}\Gamma$ widerspruchsfrei ist, da andernfalls das Resultat trivial ist)

$F(m,n)=k{\text{ genau dann, wenn }}\Gamma \vdash \varphi (m,n,k),$

$F(m,n)\not =k{\text{ genau dann, wenn }}\Gamma \vdash \neg \varphi (m,n,k)$

und (für jede Belegung ${}m,n$ für ${}x$ und ${}y$)

$\Gamma \vdash \exists !z\varphi (m,n,z).$

Den Fixpunkt zu einem vorgegebenen ${}\alpha \in L_{1}^{\rm {Ar}}$ erhalten wir nun durch eine trickreiche Anwendung von ${}\varphi$. Wir setzen

${}s:=\forall z{\left(\varphi (x,x,z)\rightarrow \alpha (z)\right)}\,.$

Der Ausdruck ${}s$ besitzt die Gödelnummer ${}GN(s)$. Wir behaupten nun, dass der Satz

${}q:=s{\frac {GN(s)}{x}}=\forall z{\left(\varphi (GN(s),GN(s),z)\rightarrow \alpha (z)\right)}\,$

die zu beweisende Ableitungsbeziehung ${}\Gamma \vdash q\leftrightarrow \alpha (GN(q))$ erfüllt.
Der Ausdruck ${}s$ besitzt die einzige freie Variable ${}x$, daher gilt

${}F(GN(s),GN(s))=GN{\left(s{\frac {GN(s)}{x}}\right)}=GN(q)\,.$

Aufgrund der Repräsentierungseigenschaft ist daher

$\Gamma \vdash \varphi (GN(s),GN(s),GN(q)).$

Aus der Allaussage ${}q$ erhält man durch Spezialisierung (man ersetzt die Variable ${}z$ durch den Term $GN(q)$)

$\vdash q\rightarrow {\left(\varphi (GN(s),GN(s),GN(q))\rightarrow \alpha (GN(q))\right)}.$

Da das Antezedens der rechten Implikation aus ${}\Gamma$ ableitbar ist, folgt

$\Gamma \vdash q\rightarrow \alpha (GN(q)).$

 Dies besagt also die Ableitbarkeit der Hinrichtung.

Die aufgrund der Repräsentierbarkeit oben angeführte eindeutige Existenzaussage führt zu

$\Gamma \vdash \forall z{\left(\varphi (GN(s),GN(s),z)\rightarrow (z=GN(q))\right)}.$

Durch Substitution ergibt sich

$\vdash (z=GN(q))\rightarrow (\alpha (GN(q))\rightarrow \alpha (z))$

und somit nach einer prädikatenlogischen Umformulierung

$\Gamma \vdash \forall z{\left(\varphi (GN(s),GN(s),z)\wedge \alpha (GN(q))\rightarrow \alpha (z)\right)}.$

Da hierbei ${}\alpha (GN(q))$ keine freie Variablen besitzt, ist auch

$\Gamma \vdash \alpha (GN(q))\rightarrow {\left(\forall z(\varphi (GN(s),GN(s),z)\rightarrow \alpha (z))\right)},$

und das Sukzedens ist gerade ${}q$, sodass auch die Rückrichtung ableitbar ist.

Zur bewiesenen Aussage