„Gott existiert notwendigerweise.“ Das ist das Theorem, das der große Logiker Kurt Gödel mit rein formalen Argumenten ableitete. Seine logische Beweisführung ist recht kompliziert und schwer nachzuvollziehen. Einem Forschungsteam von TU Wien und FU Berlin gelang es aber nun, mit einem Computerprogramm zu zeigen, dass Gödels Beweis in sich logisch richtig ist. Philosophische oder theologische Grundsatzfragen werden damit zwar nicht beantwortet, für die Theorie der automatischen Beweisführung ist das aber ein bemerkenswerter Schritt.

Der Gottesbeweis aus dem Computer
Drei Definitionen und fünf Grund-Axiome, mehr benötigte Gödel nicht, um die Existenz Gottes logisch zwingend abzuleiten - vorausgesetzt natürlich, man glaubt an die Richtigkeit seiner Grundannahmen. „Auf den ersten Blick ist allerdings nicht klar, ob Gödels Axiome überhaupt logisch miteinander verträglich sind, und ob seine Schlussfolgerungen tatsächlich logisch zwingend aus den Axiomen folgen“, erklärt Bruno Woltzenlogel-Paleo vom Institut für Computersprachen der TU Wien. Gemeinsam mit seinem Kollegen Christoph Benzmüller von der Freien Universität Berlin entwickelte er eine Methode, den Beweis durch Computerprogramme überprüfen zu lassen.

Gödel definiert in der Sprache der Logik Gott als das Wesen mit allen positiven Eigenschaften. Er unterscheidet in seinem Beweis außerdem zwischen Möglichem und Notwendigem: So ist es etwa möglich, dass der Himmel blau ist, der Himmel hat aber nicht notwendigerweise diese Eigenschaft. Hingegen hat ein Quadrat notwendigerweise vier Ecken. Zunächst leitet Gödel das Theorem ab, dass Gott möglicherweise existiert. Gottähnlich zu sein definiert Gödel als positiv, ebenso wie die Eigenschaft „aus der notwendigen Realisierung seiner Essenzen heraus notwendigerweise zu existieren“. Daraus schlussfolgert er schließlich, dass Gott sogar notwendigerweise existieren muss.

Moderne Logik für mittelalterliche Ideen
Gödels Beweis war nicht der erste Versuch, die Existenz Gottes rein ontologisch abzuleiten (also mit einer Theorie des Seins, ohne Bezug auf sinnliche Erfahrungen). Ähnliches hatten bereits andere Philosophen versucht – Descartes und Leibnitz hatten darüber geschrieben, der große islamische Philosoph Avicenna (Abu Ibn Sina) skizzierte einen Gottesbeweis, der den Überlegungen von Gödel nicht unähnlich ist. Besonders bekannt ist der Beweis des mittelalterlichen Philosophen Anselm von Canterbury: Gott ist jenes Wesen, über das hinaus größer nicht mehr gedacht werden kann. Über ein nicht existentes Wesen hinaus kann noch größer gedacht werden – denn man kann sich dasselbe Wesen vorstellen, mit der zusätzlichen Eigenschaft zu existieren. Daher muss Gott existieren.

Die Computerprogramme, mit denen Gödels Beweisführung nun analysiert wurde, arbeiten natürlich auf einer rein formalen Ebene: Ob eine ihrer Variablen nun für „Gott“ oder für etwas viel Banaleres steht, spielt logisch betrachtet keine Rolle. Nachdem Gödels Gottesbeweis formal recht kompliziert ist, war er ein guter Kandidat um die Fähigkeiten von automatischen Theorem-Beweisprogrammen zu testen. „Tatsächlich konnten wir zeigen, dass die Axiome widerspruchsfrei sind“, sagt Bruno Woltzenlogel-Paleo. „Und es gelang uns, den Computer die Beweisführung der einzelnen Theoreme reproduzieren zu lassen – bis hin zur Schlussfolgerung, dass Gott notwendigerweise existiert.“

Gödel hat sich also nicht verrechnet. Ob man das allerdings als tiefe theologische Erkenntnis betrachtet, ist eine ganz andere Frage. „Die Motivation für unsere Forschung war sicher keine religiöse“, meint Woltzenlogel-Paleo. Es ist auch nicht klar, welche Rolle Religion für Gödel selbst gespielt hat. „Der Ausganspunkt war, dass ich einem befreundeten Priester in Brasilien ein Geschenk machen wollte und deshalb versuchte, den Beweis besonders sauber aufzuschreiben“, erzählt Woltzenlogel-Paleo. Als er erfuhr, dass Christoph Benzmüller von der Freien Universität Berlin überlegte, den Beweis mit Computerunterstützung zu reproduzieren, lag es nahe, diese Aufgabe gemeinsam anzupacken.

Nach welcher Logik ist das logisch?
Besonders interessant war, dass Gödels Beweis auf die sogenannte „modale Logik“ zurückgreift, die im Gegensatz zu anderen Logik-Systemen Begriffe wie „möglich“ oder „notwendigerweise“ verwendet. „Es gibt heute unüberblickbar viele Logiken“, erklärt Bruno Woltzenlogel-Paleo. „Manche kommen mit sehr wenigen Grundannahmen und Regeln aus, andere benötigen mehr, sind dann allerdings auch mächtiger.“ Es zeigte sich, dass Gödels Schlussfolgerungen nicht nur in der „Modallogik S5“ möglich sind, sondern auch in der „Modallogik KB“, die mit weniger starken Annahmen auskommt.
Automatisierte Beweisführung am Computer ist heute ein wichtiges Forschungsgebiet in der Informatik. Computer können längst komplizierte Gleichungen lösen, doch logische Beweise zu führen ist eine noch viel schwierigere Aufgabe. Eine wichtige Rolle spielen solche automatischen Beweisprogramme nicht nur für die Mathematik, sondern auch für das Überprüfen von Computerprogrammen, etwa wenn man beweisen möchte, dass ein bestimmter Computer-Algorithmus mit allen logisch möglichen Eingaben zurechtkommt, ohne abzustürzen.

Rückfragehinweis:
Dr. Bruno Woltzenlogel-Paleo
Institut für Computersprachen
Technische Universität Wien
Favoritenstraße 9-11, 1040 Wien
T: +43-1-58801-18547
<link>bruno.woltzenlogel-paleo@tuwien.ac.at

Eine Übersetzung von Gödels Beweisskizze aus der formalen Logik in die natürliche Sprache (in der Version des Gödel-Schülers Dana Scott).
Annahme 1: Entweder eine Eigenschaft oder ihre Negation ist positiv.
Annahme 2: Eine Eigenschaft, die notwendigerweise durch eine positive Eigenschaft impliziert wird, ist positiv.
Theorem 1: Positive Eigenschaften kommen möglicherweise einer existenten Entität zu.
Definition 1: Eine gottesähnliche Existenz enthält alle positiven Eigenschaften.
Annahme 3: Die Eigenschaft, gottähnlich zu sein, ist positiv.
Schlussfolgerung: Möglicherweise existiert Gott.
Annahme 4: Positive Eigenschaften sind notwendigerweise positiv.
Definition 2: Die Essenz einer Entität ist eine Eigenschaft, die der Entität zukommt und notwendigerweise alle seine Eigenschaften impliziert.
Theorem 2: Gottähnlich zu sein ist eine Essenz von jeder gottähnlichen Existenz
Definition 3: Eine Entität existiert genau dann notwendigerweise, wenn all seine Essenzen notwendigerweise in einer existenten Entität realisiert sind.
Annahme 5: Notwendigerweise zu existieren ist eine positive Eigenschaft
Theorem 3: Gott existiert notwendigerweise.