From a5b7579f6f43b0a0f100ea1ab0ae93da67d8d409 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= <git@maximilian-kessler.de>
Date: Thu, 4 Jan 2024 15:54:34 +0100
Subject: [PATCH] Diagonallemma

---
 2024_CdE_Goedel.tex | 98 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 97 insertions(+), 1 deletion(-)

diff --git a/2024_CdE_Goedel.tex b/2024_CdE_Goedel.tex
index 10d6f92..eb2dd30 100644
--- a/2024_CdE_Goedel.tex
+++ b/2024_CdE_Goedel.tex
@@ -14,13 +14,24 @@
 
 \def\shows{\leftadjoint}
 \DeclareSimpleMathOperator{prim}
+\DeclareSimpleMathOperator{Ind}
 \DeclareSimpleMathOperator{suc}
 \DeclareSimpleMathOperator{digit}
 \DeclareSimpleMathOperator{bew}
+\DeclareSimpleMathOperator{beweisbar}
+\DeclareSimpleMathOperator{Subst}
+\DeclareMathOperator\xor{\stackrel{.}{\vee}}
 
 \begin{document}
   \maketitle
 
+  \cleardoublepage
+
+  \tableofcontents
+
+  \cleardoublepage
+
+
 
 \section{Einleitung}
 
@@ -413,11 +424,96 @@ Damit haben wir also Berechenbarkeit und somit auch Beweisbarkeit formalisiert.
 \begin{goal}
   Konstruiere einen arithmetischen Satz $\varphi $, für den folgendes beweisbar ist:
   \[
-    \varphi  \leftrightarrow \lnot \exists a \bew(a, \left\lceil a \right\rceil )
+    \varphi  \leftrightarrow \lnot \exists a \bew(a, \left\lceil \varphi  \right\rceil )
     .
   \]
 \end{goal}
 
+Es wird noch etwas dauern, dass wir genau solch ein $\varphi $ konstruieren können,
+weil wir noch besser $\left\lceil \varphi  \right\rceil $ verstehen müssen,
+um es in $\varphi $ selbst \enquote{einzubetten}.
+
+\subsection{Axiome der Arithmetik: Peano-Arithmetik}
+
+Die \vocab{Peano-Arithmetik} beschreibt (in Prädikatenlogik erster Stufe)
+ein Axiomensystem zur Formalisierung der Arithmetik der natürlichen Zahlen.
+
+Folgendes sind die Axiome von $\text{PA}^{-}$:
+\begin{IEEEeqnarray}{rCl}
+  a + 0 & = &  a \\
+  a + b & = & b + a \\
+  a + ( b + c ) & = & ( a + b ) + c \\
+  1 \cdot a & = & a \\
+  a \cdot  b & = & b \cdot  a \\
+  a \cdot  (b \cdot c) & = & (a \cdot b) \cdot c \\
+  a \cdot (b + c) & = & a \cdot b + a \cdot c \\
+  0 & < & 1 \\
+  a < b & \to & a + c < b + c \\
+  (a < b \land c > 0) & \to & c \cdot a < c \cdot b \\
+  a < b \xor b < a & \xor & a = b \\
+  a < b \land b < c & \to & a < c
+\end{IEEEeqnarray}
+Hierbei ist $\xor$ ein \enquote{exclusives oder},
+d.h. \emph{genau} einer der beiden soll wahr sein.
+
+In der Peano-Arithmetik fordern wir zusätzlich noch, dass \vocab{Induktion} gilt,
+d.h.~für jede Formel $\varphi (x)$ gilt das \vocab{Induktionsaxiom} 
+\begin{equation}
+  \Ind_{\varphi } \coloneqq  [ \varphi (0) \land \forall n \, (\varphi (n) \to \varphi (n+1))] \to \forall n \, \varphi (n)
+  .
+\end{equation}
+
+\begin{notation}
+  Wir führen das Prädikat $\beweisbar (\left\lceil \varphi  \right\rceil ) \coloneqq \exists a \bew(a, \left\lceil \varphi  \right\rceil )$ ein.
+\end{notation}
+
+\begin{lemma}[Gödel'sches Diagonallemma]
+  Sei $\psi (x)$ eine arithmetische Formel mit einer freien Variable $x$.
+  Dann existiert eine Formel $\varphi $, sodass
+  \[
+    \text{PA} \shows \varphi  \leftrightarrow \psi (\left\lceil \varphi  \right\rceil )
+    .
+  \]
+\end{lemma}
+
+Etwas salopp könnte man sagen, dass die Aussage von $\varphi $ ist,
+dass $\varphi $ die Eigenschaft $\psi $ besitzt.
+
+\begin{proof}
+  $\Subst(\left\lceil \varphi \right\rceil , a, \left\lceil \chi  \right\rceil )$ bedeute:
+  Wenn man für alle freien Variablen von $\varphi $ die Zahl $a$ einsetzt,
+  so erhält man $\chi $.
+  Wegen der Church-Turing These und unseren vorherigen Überlegungen
+  gibt es ein solches Prädikat in $\text{PA}$.
+
+  Betrachte nun die Formel
+  \[
+    \exists n (\Subst(\left\lceil \varphi  \right\rceil , \left\lceil \varphi  \right\rceil , n) \land \psi (n))
+    .
+  \]
+  Man könnte diese verbalisieren als \enquote{$\psi $ trifft auf die Selbsteinsetzung von $\varphi $ zu}.
+  Diese Formel hat selbst eine freie Variable und eine Gödelnummer $g$.
+  Wir können also folgende Aussage betrachten:
+  \[
+    G \coloneqq \exists n (\Subst(g, g, n) \land \psi (n))
+    .
+  \]
+  Die Aussage $G$ ist nun, was wir suchen:
+
+  Angenommen, $G$ ist wahr, dann gibt es ein $n$, sodass $\Subst(g,g,n) \land \psi (n)$ gilt.
+  Nach der Definition von $\Subst$ ist dann $n$ die Gödelnummer von $G$
+  (denn $G$ ist gerade dadurch enstanden, in die Formel mit Nummer $g$ die Zahl $g$ für alle freien Variablen einzusetzen). Es gilt also $\psi (n) = \psi (\left\lceil G \right\rceil )$. Das zeigt $G \to \psi (\left\lceil G \right\rceil )$.
+  
+  Angenommen, $\psi (\left\lceil G \right\rceil )$ ist wahr:
+  Dann gibt es ein $n$, nämlich $\left\lceil G \right\rceil $,
+  sodass $\Subst(g, g, n) \land \psi (n)$ erfüllt ist, also haben wir $G$ gefolgert.
+
+  Es gilt also $G \leftrightarrow \psi (\left\lceil G \right\rceil )$
+  wie gewünscht.
+\end{proof}
+
+
+
 
 %\[
 %  \begin{tikzpicture}