From 586d1018c32c3fc166184f69c20721348cc219e9 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:10:47 +0100
Subject: [PATCH] =?UTF-8?q?in=20richtung=20unvollst=C3=A4ndigkeit?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 2024_CdE_Goedel.tex | 80 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

diff --git a/2024_CdE_Goedel.tex b/2024_CdE_Goedel.tex
index d7a65f8..10d6f92 100644
--- a/2024_CdE_Goedel.tex
+++ b/2024_CdE_Goedel.tex
@@ -14,6 +14,9 @@
 
 \def\shows{\leftadjoint}
 \DeclareSimpleMathOperator{prim}
+\DeclareSimpleMathOperator{suc}
+\DeclareSimpleMathOperator{digit}
+\DeclareSimpleMathOperator{bew}
 
 \begin{document}
   \maketitle
@@ -338,6 +341,83 @@ Die Church-Turing-These motiviert die folgende Definition:
   terminiert und eine korrekte Ausgabe auf das Band schreibt.
 \end{definition}
 
+\begin{corollary}
+  Es gibt ein Turing-Programm, das von einer Zeichenfolge $S$ feststellt,
+  ob sie ein korrekter Tableau-Beweis für eine Aussage $\varphi $
+  aus den Axiomen $\mathcal{A}$ ist.
+\end{corollary}
+
+Wir wollen nun ansehen, wie Gödel zu seinem Unvollständigkeitssatz kam:
+
+\underline{Schritt 1: Axiomatisierung}
+Zu einem gegebenen Turingprogramm $P$ funde eine arithmetische Formel $\varphi _P$ so,
+dass $\varphi _P(a,b)$ wahr ist genau dann, wenn $P$ bei Eingabe $a$ Ausgabe $b$ liefert.
+
+Die Zustände seien mit $\set{ S_1, \dotsc, S_n } $ bezeichnet,
+wir können $S_i$ durch die natürliche Zahl $i$ kodieren.
+Die Kopfposition ist ebenfalls eine natürliche Zahl, genauso wie der Bandinhalt.
+Die gesamte Konfiguration einer Turing-Maschine, die gerade ein Programm ausführt,
+ist also durch ein Tripel natürlicher Zahlen beschreibbar.
+
+Die Formel $\varphi^P _{\suc}(z_0, b_0, k_0, z_1, b_1, k_1)$ soll nun beschreiben,
+dass bei Ausführung des States $(z_0, b_0, k_0)$ sich im nächsten Schritt
+$(z_1, b_1, k_1)$ ergibt.
+
+Die Formel $\digit(z, i, j)$ ist erfüllt genau dann,
+wenn $j$ die $i$-te Ziffer von $z$ ist (wobei $i$-te Ziffer einer Zahl von hinten gezählt wird, die $1$-te Ziffer ist also die Einerziffer).
+
+Dann können wir zum Beispiel die Regel
+\[
+  (s_1, 0) \mapsto (s_2, 0, \text{rechts})
+\]
+durch die Formel
+\[
+  (z_0 = 1 \land \digit(b_0, k_0, 0)) \to (z_1 = 2 \land k_1 = k_0 + 1 \land b_1 = b_0)
+\]
+ausdrücken.
+Um Zustandsänderungen des Bandes auszudrücken, benötigen wir noch eine Formel
+$\operatorname{digitChange}(z_0, i, z_1)$, die ausdrückt, dass sich $z_0$ und $z_1$ genau
+in der $i$-ten Ziffer unterscheiden.
+Die Regel
+\[
+  (s_1, 1) \mapsto (s_0, 0, \text{links})
+\]
+können wir dann als
+\[
+  (z_0 = 1 \land \digit(b_0, k_0, 1) \to (z_1 = 9 \land k_1 = k_0 - 1 \land \operatorname{digitChange}(b_0, k_0, b_1))
+\]
+realisieren.
+
+Das Prädikat $\varphi ^P_{\suc}$ lässt sich nun als großes \enquote{Und} all dieser
+Zustandsimplikationen.
+
+Wir wollen nun noch Zustandsfolgen betrachten, um über den gesamten Berechnungsverlauf
+der Turingmaschine reden zu können.
+Hierzu kodieren wir Listen $(x_1, x_2, \dotsc, )$ von natürlichen Zahlen als das Produkt $2^{x_1} \cdot  3^{x_2} \cdot  \dotsb p_k^{x_k}$, wobei $p_k$ die $k$-te Primzahl sein.
+
+Jetzt können wir die ursprüngliche Formel $\varphi _P(a,b)$ ausdrücken als
+\begin{itemize}
+  \item Es gibt eine Zahl $m = p_1^{x_1} \cdot p_2^{x_2} \dotsc p_n^{x_n}$, sodas
+  \item $x_1$ kodiert die Konfiguration $(1,1,a)$.
+  \item $x_n$ kodiert die Konfiguration der Form $(-, -, b)$.
+  \item Für alle $2 \leq i \leq n$ gilt: $\varphi ^P_{\suc}(x_{i-1}, x_i)$.
+\end{itemize}
+
+Damit haben wir also Berechenbarkeit und somit auch Beweisbarkeit formalisiert.
+
+\begin{corollary}
+  Es existiert eine arithmetische Formel $\bew(a,b)$, die genau dann wahr ist,
+  wenn $a$ einen Tableaubeweis für die von $b$ kodierte Formel kodiert.
+\end{corollary}
+
+\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 )
+    .
+  \]
+\end{goal}
+
 
 %\[
 %  \begin{tikzpicture}