Der Gödelsche Unvollständigkeitssatz beschäftigt sich mit der Beweisbarkeit von Aussagen in formalen Theorien. Aussagen, für die man einen Beweis kennt, gelten als wahr. Unter Umständen kann man auch nachweisen, dass ein Beweis existiert, ohne diesen selbst zu kennen. Solche Aussagen bezeichnet man als beweisbar. Aussagen, deren Gegenteil beweisbar ist, heißen widerlegbar. Der Mathematiker Kurt Gödel wies im Jahre 1930 nach, dass man erstaunlicherweise nicht immer alle Aussagen oder ihr Gegenteil beweisen kann. Sein Satz besagt
- Nicht in jedem formalen System sind alle Sätze beweisbar oder widerlegbar, selbst wenn man das System erweitert
Die möglichen Beweise sind also unvollständig, daher wird der Satz auch Unvollständigkeitssatz genannt.
Gödels Argumentation läuft auf eine Abzählung aller Sätze innerhalb des formalen Systems hinaus, jeder Satz erhält eine eigene Nummer. Er konstruiert dann eine Aussage der Form: Der Satz mit der Nummer x ist nicht beweisbar und setzt für x die Nummer dieser Aussage ein. Insgesamt erhält er einen beweisbaren Satz der Form "Ich bin nicht beweisbar". Durch Verwendung von formalen, mathematisch strengen Beweismethoden kann Gödel den Widerspruch zweifelsfrei nachweisen.
Das zugrundegelegte formale System muss also mindestens Zählungen erlauben. Für einfache Systeme gilt der Unvollständigkeitssatz daher nicht. Die Möglichkeit von Zählungen ist aber die einzige wesentliche Eigenschaft einer formalen Theorie, für die der Satz gilt. Dies ist für relativ viele mathematische Theorien erfüllt.
Normalerweise könnte man sich dadurch behelfen, dass man für alle Sätze, die weder bewiesen noch widerlegt werden können, einfach definiert, ob sie als wahr oder falsch gelten und die Definition dem formalen System hinzufügt. Im neuen, erweiterten System existiert dann für diese Sätze ein Beweis, nämlich einfach die hinzugefügte Definition. Gödel zeigte jedoch, dass dies unmöglich ist, da stets unbeweisbare Sätze übrigbleiben. Auch das erweiterte System bleibt unvollständig.
Hilberts Programm
Gödel versetzte mit seinem Unvollständigkeitssatz einem Ansatz von David Hilbert zur vollständigen Begründung und Formalisierung der Mathematik einen schweren Schlag. Dieser Ansatz ist als Hilberts Programm bekannt geworden und wurde von ihm im Jahre 1921 veröffentlicht. Hilbert schlug vor, die Widerspruchsfreiheit von komplexeren Systemen durch einfachere Systeme zu zeigen. Eine streng formalisierte Prädikatenlogik erster Stufe war dazu ein Ansatz Hilberts. Am Ende seines Programms sollte die gesamte Mathematik auf die einfache Arithmetik zurückgeführt und auf ein axiomatisches System gestellt werden, aus dem alle mathematischen Sätze streng ableitbar sind.
Gödels Arbeit war durch Hilberts Programm motiviert. Er verwendete die von Hilbert entwickelten Methoden, um seinen Unvollständigkeitssatz zu zeigen. Gödel bewies auch den folgenden Satz
- Ein System kann nicht zum Beweis seiner eigenen Widerspruchsfreiheit verwendet werden
Gödel hatte damit gewissermaßen Hilbert mit seinen eigenen Methoden geschlagen.
Ein anderer Ansatz, der unüberbrückbare Lücken in Hilberts Programm nachweist, stammt von dem Mathematiker Alan Turing. Er erfand die Turingmaschine und formulierte deren Halteproblem.
Genauere Formulierung
Der Gödelsche Satz besagt genauer, dass jedes Beweissystem für die Menge der wahren arithmetischen Formeln unvollständig ist (sofern man voraussetzt, dass die Arithmetik widerspruchsfrei ist - was, wie Gödel auch zeigt, nicht mit Mitteln der untersuchten Theorie alleine bewiesen werden kann). Das heißt:
In jeder formalen Theorie, welche mindestens so mächtig wie die Theorie der natürlichen Zahlen (Peano-Arithmetik) ist, bleiben wahre (und falsche) arithmetische Formeln übrig, die nicht innerhalb der Theorie beweisbar (widerlegbar) sind.
Damit eine Theorie (in der Prädikatenlogik erster Stufe, PL1) die Voraussetzungen für die Unvollständigkeit erfüllt, muss gelten:
- Zu jeder durch einen Ausdruck G(x) beschriebenen Menge ist das Komplement beschreibbar.
- Zu jeder durch einen Ausdruck G(x) beschriebenen Menge M ist die Menge M*={n|d(x)∈M} beschreibbar; Dabei ist d(x) die Diagonalisierung von x.
- Die Menge der beweisbaren Ausdrücke der Theorie ist durch einen Ausdruck der Form G(x) beschreibbar.
Nach dem Satz von Löwenheim-Skolem findet man zu jeder Theorie in PL1 ein Modell mit der Mächtigkeit der Signatur. Für "normale" Theorien existiert also ein abzählbares Modell, z.B. die natürlichen Zahlen. Die Idee von Gödel war, Formeln der Theorie selbst zum Objekt derselben zu machen. Dazu wurden die Formeln gödelisiert, d.h. eine (umkehrbar eindeutige) Abbildung von Formeln auf natürliche Zahlen gebildet. Das kann man z.B. dadurch erreichen, dass jedem Symbol der Signatur eine Zahl zugeordnet wird, die dann verkettet werden. Ordnet man der 0 die 1 und = die 2 zu, so ist die Gödelnummer der Formel (in dem Spezialfall) 0=0 die 121. Die Verkettungsoperation ist einfach durch Exponentieren zu realisieren. Es lassen sich auch die syntaktisch wohlgeformten, und schließlich die beweisbaren Formeln durch arithmetische Ausdrücke (Addition, Multiplikation, Exponentiation) beschreiben.
Die Diagonalisierung in Gödels Beweis ist nun eine Anwendung eines Ausdrucks P(x) auf die eigene Gödelnummer. Ist die Gödelnummer des Ausdrucks (und damit der Zeichenreihe) P(x) zum Beispiel 12345, so ist die Diagonalisierung der Zahl 12345 die Gödelnummer von P(12345) (selbstverständlich hat eine Zahl, hier 12345, auch eine Gödelnummer, die entsteht, indem man alle vorkommenden Ziffern gödelisiert).
"Besagt" der Ausdruck B(x) also, dass x beweisbar ist, und ist zum Beispiel 12345 die Gödelnummer von B(x), so ist ¬B(12345) eine unbeweisbare Aussage. Diese Aussage besagt dann nämlich: Die Formel mit der Gödelnummer 12345 ist nicht beweisbar. 12345 ist aber die Gödelnummer von B(x). Also sagt ¬B(12345): Ich bin nicht beweisbar. Wenn PA korrekt ist, so ist dieser Satz wahr, aber nicht beweisbar.
Gödels ursprünglicher Beweis ging noch weiter. Er wollte Rückgriffe auf die Semantik, insbesondere die Korrektheit, vermeiden. Deswegen bewies er seinen Unvollständigkeitssatz unter der Voraussetzung der ω-Konsistenz: Eine Theorie ist ω-inkonsistent, wenn ein Ausdruck mit einer einzigen freien Variable x existiert, für den beweisbar ist, zugleich aber für alle beweisbar ist.
Rosser erweiterte das Gödelsche Resultat, indem er einen Unvollständigkeitsbeweis lieferte, für den nicht die Menge der Ausdrücke, deren Diagonalisierung beweisbar ist, beschrieben wird, sondern eine zu dieser Menge disjunkte Obermenge der Ausdrücke, deren Diagonalisierung widerlegbar ist. Dadurch ist auch der Bezug auf die ω-Konsistenz überflüssig.
Durch diesen erstaunlichen Satz ist der Mathematik eine prinzipielle Grenze gesetzt: Nicht jeder wahre mathematische Satz kann aus den wie auch immer gewählten Axiomen eines mathematischen Teilgebietes (z. B. Arithmetik, Geometrie, Algebra etc.) formal abgeleitet werden.
Literatur
- Kurt Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatsheft für Math. und Physik 38, 1931, S.173-198.
- Kurt Gödel, Diskussion zur Grundlegung der Mathematik, Erkenntnis 2, Monatsheft für Math. und Physik, 1931-32, S.147-148.
- Ernest Nagel, James R. Newmann, Der Gödelsche Beweis, Scientia Nova, Oldenburg (ISBN 3-486-45214-2)
- Douglas R. Hofstadter, Gödel, Escher, Bach, ein Endloses Geflochtenes Band, Dt. Taschenbuch Verlag, München, 1991 (ISBN 3-423-30017-5)
- Max Woitschach, Gödel, Götzen und Computer; Eine Kritik der unreinen Vernunft., Poller, Stuttgart, 1986 (ISBN 3-87959-294-2)
- Wolfgang Stegmüller, Unvollständigkeit und Unentscheidbarkeit; Die mathematischen Resultate von Gödel, Church, Kleene, Rosser und ihre erkenntnistheoretische Bedeutung., Springer-Verlag, Wien, 1973 (ISBN 3-211-81208-3 Springer Wien-New York; ISBN 0-387-81208-3 Springer New York-Wien; Library of Congress Catalog Card Number 73-14357)
- Sybille Krämer, Symbolische Maschinen; d. Idee d. Formalisierung in geschichtl. Abriß, Wissenschaftliche Buchgesellschaft, Darmstadt, 1988 (ISBN 3-534-03207-1)
- Ludwig Fischer, Die Grundlagen der Philosophie und der Mathematik, Felix Meiner Verlag, Leipzig, 1933.
- Norbert Domeisen, Logik der Antinomien. Bern etc.: Peter Lang. 142 S. 1990. (ISBN 3-261-04214-1), Zentralblatt MATH
Siehe auch: Formales System (Logik)