Gödelscher Vollständigkeitssatz

Der Gödelsche Vollständigkeitssatz (benannt nach Kurt Gödel) ist der Hauptsatz der mathematischen Logik. Er zeigt für den Hilbert-Kalkül (ein formales System der Prädikatenlogik erster Stufe) die Korrektheit und Vollständigkeit: Jeder Satz, der semantisch aus einer Formelmenge folgt, lässt sich mit den Schlussregeln des Systems aus der Formelmenge herleiten, und umgekehrt. Für die Logik erster Stufe sind also syntaktische und semantische Folgerung gleichbedeutend.

Grundbegriffe

Formeln: Zunächst muss eine Menge von Konstanten-, Funktions- und Relationssymbolen festgelegt werden. Neben diesen Symbolen stehen dann aussagenlogische Junktoren, die Quantoren, das Gleichheitszeichen sowie Variablen zum Formelaufbau zur Verfügung.

Semantik: Eine Struktur ist eine nichtleere Menge, in der die Konstanten-, Funktions- und Relationssymbole durch Elemente, Funktionen und Relationen interpretiert werden. Zu einer Interpretation gehört außerdem eine Belegung der Variablen mit Werten aus der Struktur. Eine Formel ist allgemeingültig, wenn sie in jeder Interpretation wahr ist. Eine Interpretation, die jede Formel aus einer Formelmenge ${\displaystyle \Gamma \ }$ wahr macht, nennt man ein Modell von ${\displaystyle \Gamma \ }$. Eine Formel ${\displaystyle \varphi }$ ist eine semantische Folgerung aus ${\displaystyle \Gamma \ }$ (in Zeichen ${\displaystyle \Gamma \vDash \varphi }$), wenn ${\displaystyle \varphi }$ in jedem Modell von ${\displaystyle \Gamma \ }$ wahr ist.

Herleitungen: Ein Hilbert-Kalkül ist durch Axiome und Schlussregeln gegeben. Die wichtigste Schlussregel ist dabei der modus ponens: Von den Formeln ${\displaystyle \varphi }$ und ${\displaystyle \varphi \rightarrow \psi }$ darf man zu ${\displaystyle \psi \ }$ übergehen. Eine Formel ${\displaystyle \varphi }$ ist aus einer Formelmenge ${\displaystyle \Gamma \ }$ herleitbar (in Zeichen ${\displaystyle \Gamma \vdash \varphi }$), wenn es eine endliche, mit ${\displaystyle \varphi }$ endende Folge von Formeln gibt, wobei für jedes Glied der Folge gilt: Es ist ein Axiom oder ein Element von ${\displaystyle \Gamma \ }$ oder es wird mit einer Schlussregel aus früheren Gliedern der Folge gebildet.

Der Satz

Kurt Gödel bewies 1929 den Vollständigkeitssatz im Wesentlichen in der folgenden Form:

Es gibt einen Kalkül der Prädikatenlogik erster Stufe derart, dass für jede Formelmenge ${\displaystyle \Gamma }$ und für jede Formel ${\displaystyle \varphi }$ gilt:

${\displaystyle \varphi }$ folgt genau dann aus ${\displaystyle \Gamma }$, wenn ${\displaystyle \varphi }$ im Kalkül aus ${\displaystyle \Gamma }$ hergeleitet werden kann.

Verwendet man ${\displaystyle \vDash }$ als Zeichen für die semantische Folgerung und ${\displaystyle \vdash }$ für die Herleitbarkeit im Kalkül, ergibt sich die kurze Formulierung:

${\displaystyle (\Gamma \vDash \varphi )\Longleftrightarrow (\Gamma \vdash \varphi )}$

Der Schluss von rechts nach links bedeutet die Korrektheit des Kalküls: Alles, was sich mit dem Kalkül aus vorgegebenen Annahmen herleiten lässt, folgt auch wirklich logisch aus diesen Annahmen. Jeder sinnvolle Logikkalkül muss diese Forderung erfüllen.

Der Schluss von links nach rechts ist die eigentliche Vollständigkeit: Es wird behauptet, dass zu jedem Satz, der aus einer Menge von vorgegebenen Annahmen logisch folgt, tatsächlich ein Beweis aus diesen Annahmen im Kalkül existiert.

Eine abgeschwächte Fassung des Vollständigkeitssatzes wird oft so formuliert:

Es gibt einen Kalkül der Prädikatenlogik erster Stufe derart, dass für jede Formel ${\displaystyle \varphi }$ gilt:

${\displaystyle \varphi }$ ist genau dann allgemeingültig, wenn ${\displaystyle \varphi }$ im Kalkül bewiesen werden kann.

In Zeichen lautet diese Fassung kurz:

${\displaystyle (\vDash \varphi )\Longleftrightarrow \ (\vdash \varphi )}$

Sie ist ein Spezialfall der obigen Aussage, wobei die Formelmenge ${\displaystyle \Gamma }$ leer ist.

Es ist wichtig, sich zu vergegenwärtigen, dass Vollständigkeit eine Eigenschaft eines Kalküls ist. Das Symbol ${\displaystyle \vdash }$ für die Herleitbarkeit ist also eigentlich eine Abkürzung für ${\displaystyle \vdash _{K}}$, wobei ${\displaystyle K}$ den Kalkül bezeichnet. Zum Beweis des Satzes muss ein konkreter Kalkül angegeben werden. Gödel hat dies mit einem Hilbert-Kalkül, bestehend aus Axiomen und Schlussregeln, getan. Ebenfalls vollständig ist zum Beispiel der von Gerhard Gentzen eingeführte Sequenzenkalkül.

Beweisidee

Gödel bewies den Satz ursprünglich, indem er das Problem auf die Vollständigkeit für eine eingeschränkte Klasse von Formeln reduzierte, für die die Vollständigkeit dann auf die Vollständigkeit der Aussagenlogik zurückgeführt werden kann. Heute wird meist ein von Leon Henkin 1949 veröffentlichter Beweis benutzt. Dazu wird zunächst folgender Satz bewiesen:

Jede konsistente Formelmenge hat ein Modell.

Konsistenz ist dabei ein syntaktischer Begriff und bedeutet für eine Formelmenge ${\displaystyle \Gamma \ }$, dass aus ihr kein Widerspruch im Kalkül hergeleitet werden kann (formal: Es gibt keine Formel ${\displaystyle \varphi }$ mit ${\displaystyle \Gamma \vdash \varphi }$ und ${\displaystyle \Gamma \vdash \neg \varphi }$).

Die Existenz des Modells wird bewiesen, indem mithilfe des Satzes von Lindenbaum eine gegebene konsistente Formelmenge ${\displaystyle \Gamma \ }$ zu einer sogenannten maximalkonsistenten Menge erweitert wird, die keine konsistente echte Obermenge hat. Dann wird die Sprache durch sogenannte Henkinkonstanten erweitert und die Formelmenge so erweitert, dass für jede Formel der Form ${\displaystyle \exists x\varphi (x)}$ auch ${\displaystyle \varphi (c)}$ (c eine Henkinkonstante) enthalten ist. Dann gibt es nach dem Satz von Henkin eine Terminterpretation, deren Grundmenge aus den Termen der Sprache besteht und die alle Elemente der entstehenden Formelmenge erfüllt, und damit auch die ursprüngliche konsistente Formelmenge ${\displaystyle \Gamma \ }$.

Dann lässt sich die Vollständigkeit leicht zeigen: Angenommen, es gilt zwar ${\displaystyle \Gamma \vDash \varphi }$, aber nicht ${\displaystyle \Gamma \vdash \varphi }$. Der Kalkül hat die Eigenschaft, dass man die Negation einer aus einer konsistenten Formelmenge nicht herleitbaren Formel zu der Formelmenge hinzunehmen kann und die Konsistenz dabei erhalten bleibt. Im vorliegenden Fall ist also ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ konsistent und hat nach dem Satz von Henkin ein Modell. In diesem Modell ist aber nun ${\displaystyle \varphi }$ falsch, im Widerspruch zur Voraussetzung, dass ${\displaystyle \varphi }$ in allen Modellen von ${\displaystyle \Gamma \ }$ wahr ist.

Bedeutung

Dass sich das inhaltliche logische Folgern durch Ableitungen in einem rekursiven Kalkül vollständig abbilden lässt, ist eine herausragende Eigenschaft der Prädikatenlogik erster Stufe. Diese Vollständigkeit gilt für viele andere Logiken nicht, zum Beispiel nicht für die Prädikatenlogik höherer Stufe.

Der Kompaktheitssatz, ein zentraler Satz der Modelltheorie, ergibt sich als Korollar aus dem Vollständigkeitssatz.

Im Rahmen des Hilbertprogramms (zur Schaffung eines widerspruchsfreien und vollständigen Kalküls für die Mathematik) schien der Satz zunächst ein Schritt zum Ziel zu sein. Das Programm scheiterte allerdings, weil Gödel mit seinem Unvollständigkeitssatz zeigen konnte, dass eine genügend ausdrucksstarke Theorie nicht jeden wahren Satz beweisen kann. (Man beachte, dass sich der Unvollständigkeitssatz auf eine andere Art von Vollständigkeit bezieht als der hier vorgestellte Vollständigkeitssatz.)

Stellung in der Mengenlehre

Für abzählbare (oder allgemeiner: wohlgeordnete) Mengen von Symbolen lässt sich der Vollständigkeitssatz aus den Axiomen der Zermelo-Fraenkel-Mengenlehre ohne Auswahlaxiom beweisen. Der Beweis für beliebige Symbolmengen lässt sich mit dem Auswahlaxiom führen, der Satz ist allerdings nicht äquivalent zum Auswahlaxiom, sondern (relativ zu den Axiomen der Mengenlehre ohne Auswahlaxiom) u. a. zu:

• Ultrafilterlemma
• Kompaktheitssatz
• Satz von Lindenbaum
• Darstellungssatz für Boolesche Algebren

Literatur

• Leon Henkin: The Completeness of the First-Order Functional Calculus. In: Journal of Symbolic Logic, 14, 1949, S. 159–166
• K Gödel: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. In: Monatshefte für Mathematik. 37. Jahrgang, Nr. 1, 1930, S. 349–360, doi:10.1007/BF01696781. 
• Wolfgang Rautenberg: Einführung in die Mathematische Logik. 3. Auflage. Vieweg+Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2. 
• K Gödel: Über die Vollständigkeit des Logikkalküls. In: Dissertation. University Of Vienna., 1929. 
• Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik. Spektrum Akademischer Verlag, Heidelberg 2007, ISBN 3-8274-1691-4.