diff --git a/goedel.tex b/goedel.tex
index c301f17..cdb5631 100644
--- a/goedel.tex
+++ b/goedel.tex
@@ -153,8 +153,54 @@
   \end{gather*}
 \end{example}
 
+\begin{notation}
+  Für eine Sprache $\mathcal{S}$ und ein Axiomensystem $\mathcal{A}$ schreiben wir
+  $A \shows \varphi $, falls sich aus $A$ und $\lnot \varphi $ eine geschlossenes
+  Tableau herleiten lässt.
+\end{notation}
 
+\begin{definition}[Korrektheit]
+  Wir sagen, dass eine Kombination aus Sprache und Schlussregeln \vocab{korrekt}
+  ist, wenn alle Formeln, die sich herleiten lassen (die also syntaktisch folgerbar sind),
+  auch sematisch folgebar sind.
 
+  Kompakter geschrieben sprechen wir von Korrektheit, wenn aus $\mathcal{A} \shows \varphi $ auch stets $\mathcal{A} \models \varphi $ folgt.
+\end{definition}
+
+\begin{remark}
+  Das zu beweisen ist letztendlich nicht schwer. Man muss sich \enquote{nur} davon überzeugen, dass jede einzelne der syntaktischen Schlussregeln so gestaltet ist,
+  dass sich auch in $S$-Strukturen die entsprechenden Schritte durchführen lassen.
+\end{remark}
+
+\begin{definition}[Vollständigkeit]
+  Ähnlich sprechen wir von \vocab{Vollständigkeit}, wenn jede Formel,
+  die sich semantisch herleiten lässt, auch syntaktisch herleiten lässt,
+  d.h.~ wenn aus $A \models \varphi $ auch schon $A \shows \varphi $ folgt.
+\end{definition}
+
+\begin{theorem}[Gödel'scher Vollständigkeitssatz]
+  Das Tableau-Kalkül ist korrekt und vollständig für jede Sprache $\mathcal{S}$.
+\end{theorem}
+
+\begin{remark}
+  Vollständigkeit zu beweisen ist weitaus schwieriger: Wir müssen über \emph{alle} $\mathcal{S}$-Strukturen etwas aussagen, haben aber nur eine fixe Menge an syntaktischen Regeln zur Verfügung.
+\end{remark}
+
+\begin{corollary}
+  Ist jede \emph{endliche} Teilmenge eines Axiomensystems konsistent,
+  so ist auch das Axiomensystem selbst konsistent.
+\end{corollary}
+
+\begin{proof}
+  Sei $\mathcal{A}$ dieses System und nimm an, dass man $\mathcal{A}$ nicht interpretieren kann, ich also keine $\mathcal{S}$-Struktur finde, in der $\mathcal{A}$ gilt.
+  Dann gilt insbesondere $\mathcal{A} \models \bot$, wobei $\bot$ irgendeine falsche Aussage sei, denn in jeder $\mathcal{S}$-Struktur, in der $\mathcal{A}$ gilt (es gibt keine solchen), gilt ja auch $\bot$.
+  Nach dem Vollständigkeitssatz gibt es dann auch schon eine Herleitung $\mathcal{A} \shows \bot$.
+  Eine Herleitung besteht allerdings aus endlich vielen Schritten,
+  also gibt es auch schon eine endliche Teilmenge $\mathcal{B} \subset \mathcal{A}$,
+  sodass $\mathcal{B} \shows \bot$.
+  Nach Korrektheit ist dann auch $\mathcal{B} \models \bot$,
+  also ist $\mathcal{B}$ inkonsistent, ein Widerspruch zu unserer Annahme.
+\end{proof}
 
 
 \end{document}