tableu kalkül

goedel.tex

@@ -1,20 +1,26 @@
 \documentclass[ngerman]{scrartcl}
 
-\usepackage{mkessler-math}
 \usepackage{babel}
+
+\usepackage{mkessler-math}
+\usepackage{mkessler-vocab}
+\usepackage{mkessler-enumerate}
+\usepackage{fancythm}
 \usepackage{csquotes}
 
 \title{Kurt Goedel - Leben und Werk}
 \subtitle{Kurs auf der CdE-Winteraka 2023/2024}
 \author{Merlin Carl\thanks{Mitschrift von Maximilian Keßler}}
 
+\def\shows{\leftadjoint}
+
 \begin{document}
   \maketitle
 
 
 \section{Einleitung}
 
-\large{Steckbrief von Kurt Gödel}
+\large{Steckbrief von Kurt Friedrich Gödel}
 
 \begin{itemize}
   \item Geboren am 28.06.1906 (Brünn, Mähren (Tschechien, damals Österreich-Ungarn))
@@ -26,12 +32,129 @@
   \item 1935: Relative Konsistenz des Auswahlaxioms \\
     Heirat mit Adele Nimbursky (geb. Porkert)
   \item 1937: Relative Konsistenz der Kontinuumshypothese
-  \item 1940: Emigration in die USA (Princeton); Mitglied des IAS Geschlossene zeitartige Kuriven
+  \item 1940: Emigration in die USA (Princeton), Mitglied des IAS \\
+    Arbeit zu \enquote{Geschlossene zeitartige Kurven}
   \item 1941: Ontologischer Gottesbeweise
   \item 1948: Amerikanische Staatsbürgerschaft
   \item 1951: Albert Einstein Award; 1957 National Medal of Science etc.
   \item 1953: Professur am IAS
   \item 1956: Emeritierung
+  \item Diverse philosophische Aufsätze, ontologischer Gottesbeweis, Überlegungen zur Kontinuumshypothese
+  \item Gestorben 14.01.1978 (Princeton)
 \end{itemize}
 
+
+\section{Semantik}
+
+\begin{definition}[Sprache]
+  Eine \vocab{Sprache} $\mathcal{S}$ besteht aus
+  \begin{enumerate}[1.]
+    \item Prädikatensymbolen $P$, $Q$, $R$, alle mit fester Arität (auf wie viele Terme man das Prädikat anwendet)
+    \item Funktionszeichen $f$, $g$, $h$, ebenfalls jeweils mit Arität.
+    \item Konstantenzeichen $a$, $b$, $c$, \ldots
+  \end{enumerate}
+\end{definition}
+
+\begin{definition}[S-Struktur]
+  Eine \vocab{S}-Struktur für eine Sprache $\mathcal{S}$ besteht aus
+  \begin{itemize}
+    \item einer Domäne (Menge) $M$
+    \item Für jedes Prädikatenzeichen von $\mathcal{S}$ eine Relation über $M$
+    \item Für jedes Funktionszeichen und jede Konstante von $\mathcal{S}$ eine Funktion bzw.~ein Element aus $M$.
+  \end{itemize}
+\end{definition}
+
+\begin{definition}
+  Sei $\mathcal{S}$ eine Sprache und $\mathcal{A}$ ein Axiomensystem, d.h.~eine Menge an Formeln über $\mathcal{S}$.
+ Für eine Formel $\varphi $ schreiben wir $\mathcal{A} \models \varphi $,
+ falls aus $\mathcal{A}$ \vocab{semantisch} die Formel $\varphi $ folgt,
+ d.h.~falls für alle $\mathcal{S}$-Strukturen, in denen $\mathcal{A}$ wahr ist,
+ auch $\varphi $ wahr ist.
+\end{definition}
+
+
+\subsection{Ableitungsregeln: Tableau-Kalkül}
+
+\begin{definition}[Tableu-Kalkül]
+  Eine \vocab{Herleitung} für eine Formel $\varphi $ im \vocab{Tableau-Kalkül}
+  besteht immer daraus, mit der Formel $\lnot \varphi $ anzufangen
+  und dann durch Anwendung von Schlussregeln einen Baum zu erzeugen.
+  Ein Ast des Baumes gilt als \vocab{abgeschlossen}, wenn auf ihm sowohl $\psi $ als auch $\lnot \psi $ stehen, sich also ein Widerspruch ergeben hat.
+  Eine Herleitung von $\varphi $ ist es, alle Äste des Baumes, an dessen Wurzel $\lnot \varphi $ steht, zu schließen.
+
+  Folgende formale Regeln erlauben wir für logische Schlussfolgerungen:
+  \begin{itemize}
+    \item Steht $\lnot \lnot \varphi $ auf einem Ast, füge $\varphi $ hinzu.
+    \item Steht $α_1 \land α_2$ auf einem Ast, füge $α_1$ und $α_2$ hinzu
+    \item Steht $α_1 \lor α_2$ auf einem Ast, spalte in einen Ast mit $α_1$ und einen mit $α_2$
+    \item Steht $α_1 \to  α_2$ auf einem Ast, spalte in $\lnot α_1$ und $α_2$
+    \item Ergänze $\lnot (\varphi  \to \psi )$ durch $\varphi $ und $\lnot \psi $
+    \item Ergänze $\lnot (\varphi  \varphi  \lor \psi )$ durch $\lnot \varphi $ und $\lnot \psi $
+    \item Spalte $\lnot (\varphi  \land \psi )$ in $\lnot \varphi $ und $\lnot \psi $
+  \end{itemize}
+  Folgende Regeln sind für Quantoren erlaubt:
+  \begin{itemize}
+    \item Ergänze $\exists x \varphi $ durch $\varphi ^{[ x \leftarrow  a]}$ für ein neues Konstantenzeichen $a$. Hierbei steht $\varphi ^{[ x \leftarrow a]}$ für die Formel, in der wir $x$ durch $a$ ersetzen
+    \item Ergänze $\lnot \forall x \varphi $ durch $\lnot \varphi ^{[ x \leftarrow a]}$ für ein neues Konstantenzeichen $a$
+    \item Ergänze $\forall x \varphi $ durch $\varphi [ x \leftarrow l]$ für einen Term $t$
+    \item Ergänze $\lnot \exists x \varphi $ durch $\lnot \varphi ^{[ x \leftarrow t]}$ für einen Term $t$
+  \end{itemize}
+\end{definition}
+
+\begin{remark}
+  Man sollte sich den entstehenden Baum so vorstellen, dass man auf jedem Ast wissen sammelt. Jede neue Zeile fügt neues Wissen hinzu, man kann also jederzeit Wissen des eigenen Astes verwenden.
+  Wenn wir einen Ast in 2 neue Aufteilen, entspricht das einer üblichen Fallunterscheidung.
+
+  Wenn wir alle Äste schließen, haben wir alle Fälle zum Widerspruch geführt.
+\end{remark}
+
+\begin{exercise}
+  Man mache sich für alle obigen formalen Schlussfolgerungen Gedanken,
+  was diese \emph{intuitiv} sagen.
+  Das heißt, welches Wissen wird hier in welches neue Wissen verwandelt,
+  und warum macht das Sinn, bzw.~warum würden wir erwarten, dass dies eine
+  sinnvolle logische Schlussregel ist.
+\end{exercise}
+
+\begin{example}[Logische Folgerungen]
+  Wir wollen die Aussage $(\varphi  \land \psi ) \to  \lnot (\lnot \varphi  \land \lnot \psi )$ zeigen.
+
+  \[
+    \begin{tikzcd}[column sep = tiny, row sep = tiny]
+      & \lnot ((\varphi \land \psi ) \to \lnot (\lnot \psi  \land \lnot \psi ) \ar[-]{d} \\
+      & \varphi  \land \psi  \ar[-]{d}\\
+      & \lnot \lnot (\lnot \psi  \lor \lnot \psi )  \ar[-]{d}\\
+      & \varphi   \ar[-]{d}\\
+      & \psi   \ar[-]{d}\\
+      & \lnot \varphi  \lor \lnot \psi
+      \ar[-]{dr}
+      \ar[-]{dl}
+      \\
+      \lnot \varphi  & & \lnot \psi 
+    \end{tikzcd}
+  \]
+\end{example}
+
+\begin{example}[Quantoren]
+  Sei $L(x,y)$ die Aussage \enquote{$x$ liebt $y$}.
+  Wir wollen zeigen: $\exists x \forall y L(x,y) \to \forall y \exists x L(x,y)$.
+  In gesprochener Sprache: Wenn es eine Person ($x$) gibt, die alle liebt,
+  dann wird jede Person von jemandem geliebt.
+
+  Eine Herleitung dieser Formel ist die Folgende:
+  \begin{gather*}
+    \lnot (\exists x \forall y \; L(x,y) \to \forall y \exists x \; L(x,y)) \\
+    \exists x \forall y \;L(x,y) \\
+    \lnot \forall y \exists x \; L(x,y) \\
+    \forall y \; L(a,y) \\
+    \lnot \exists x \; L(x,b) \\
+    L(a,b) \\
+    \lnot L(a,b)
+  \end{gather*}
+\end{example}
+
+
+
+
+
 \end{document}