# Arithmetische Satzmenge/Repräsentierungen/Fixpunktsatz/Fakt/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)).$
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.