Gödel'scher Vollständigkeitssatz

Der Gödelsche Vollständigkeitssatz (benannt nach Kurt Gödel) ist der Hauptsatz der mathematischen Logik. Er zeigt für 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.

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 Γ und für jede Formel φ gilt:

φ folgt genau dann aus Γ, wenn φ im Kalkül aus Γ hergeleitet werden kann.

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

$\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 φ gilt:

φ ist genau dann allgemeingültig, wenn φ im Kalkül bewiesen werden kann.

In Zeichen lautet diese Fassung kurz:

$\vDash \varphi \Longleftrightarrow \ \vdash \varphi$

Sie ist ein Spezialfall der obigen Aussage, wobei die Formelmenge Γ leer ist.

Es ist wichtig, sich zu vergegenwärtigen, dass Vollständigkeit eine Eigenschaft eines Kalküls ist. Das Symbol $\vdash$ für die Herleitbarkeit ist also eigentlich eine Abkürzung für $\vdash_{K}$, wobei 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.

Erläuterung der Begriffe

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 $\Gamma\$ wahr macht, nennt man ein Modell von $\Gamma\$. Eine Formel $\varphi$ ist eine semantische Folgerung aus $\Gamma\$ (in Zeichen $\Gamma \vDash \varphi$), wenn $\varphi$ in jedem Modell von $\Gamma\$ wahr ist.

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

Beweisidee

Der ursprüngliche Beweis von Gödel wird heute nicht mehr verwendet. Stattdessen wird meistens der folgende, von Leon Henkin 1949 formulierte Satz benutzt (der oft ebenfalls als Hauptsatz der Logik erster Stufe bezeichnet wird):

Jede konsistente Formelmenge hat ein Modell.

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

Setzt man diesen Satz voraus, lässt sich die Vollständigkeit leicht zeigen: Angenommen, es gilt zwar $\Gamma \vDash \varphi$, aber nicht $\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 $\Gamma \cup \{\neg \varphi\}$ konsistent und hat nach dem Satz von Henkin ein Modell. In diesem Modell ist aber nun $\varphi$ falsch, im Widerspruch zur Voraussetzung, dass $\varphi$ in allen Modellen von $\Gamma\$ wahr ist.

Bedeutung

Dass sich das inhaltliche logische Folgern durch Ableitungen in einem 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 zweiter Stufe.

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

Mit dem Vollständigkeitssatz ist auch die theoretische Grundlage für das sog. automatische Beweisen geschaffen, also die Erzeugung oder Überprüfung von Beweisen durch Computerprogramme.

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 ist allerdings gescheitert, 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.)

Literatur

Hans Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik. Spektrum Akademischer Verlag, Heidelberg 2007, ISBN 3-8274-1691-4.