Computer beweist die Existenz Gottes

Neue Perspektiven für eine Computer-assistierte Metaphysik: Wissenschaftler aus Berlin und Wien haben Kurt Gödels berühmten Gottesbeweis mit einem Computerprogramm bestätigt

Wissenschaftlern der Freien Universität Berlin und der TU Wien ist es gelungen, Kurt Gödels berühmten Gottesbeweis mit Computern zu überprüfen. Die Wissenschaftler haben Automatisches Theorembeweisen eingesetzt , eine Technik , die bis heute vor allem für mathematische Fragestellungen verwendet wurde. Einen ersten Bericht von Christoph Benzmüller und Bruno Woltzenlogel Paleo zum neuen, automatisierten Gottesbeweis Gödels findet man in arXiv: Formalization, Mechanization and Automation of Gödel's Proof of God's Existence.Der KI-Wissenschaftler Prof. Dr. Raul Rojas hat mit Prof. Dr. Christoph Benzmüller vom Fachbereich Mathematik und Informatik, AG Intelligente Systeme und Robotik, für Telepolis gesprochen.

Herr Benzmüller, was hat Ihr Computer bewiesen?

Christoph Benzmüller: Im Nachlass von Kurt Gödel findet sich ein so genannter Gottesbeweis --- man spricht auch von einem ontologischen Beweis bzw. ontologischen Argument. Eigentlich sind zwei Varianten von Gödels ontologischem Beweis bekannt und diese Varianten unterscheiden sich in Details. Gödels ontologischer Beweis wurde in zahlreichen Publikationen von Philosophen studiert. Dabei wurden die Wahl der Begriffe, die einzelnen Argumentationsschritte und auch der verwendete Logikformalismus kritisch hinterfragt. Solche Studien erfolgten bisher ausschließlich mit Papier und Bleistift, was bekanntlich recht fehleranfällig ist.

Mit meinem Kollegen Bruno Woltzenlogel-Paleo von der TU Wien ist es mir nun gelungen, eine Variante von Gödels Gottesbeweis zu formalisieren und im Computer mit höchster mathematischer Präzision zu überprüfen. Sogar die Konsistenz der Grundannahmen wurde dabei von vom Computer belegt. Wir können nun also mit großer Gewissheit behaupten: Die logische Argumentationskette in diesem Gottesbeweis ist nachweisbar korrekt. Zudem konnten wir zeigen, dass die nicht-triviale Beweisführung vom Computer größtenteils vollautomatisch erzeugt werden kann. Das hatten wir nicht erwartet.

Was nennt man ein ontologisches Argument?

Christoph Benzmüller: Ein ontologisches Argument bzw. ein ontologischer Beweis verfolgt das Ziel die Existenz Gottes allein mit Mitteln des reinen Denkens zu hinterfragen und zu belegen. Ausgehend von abstrakten (a priori) Begriffen, die von der Erfahrung abstrahieren, insbesondere einer abstrakten Definition des Göttlichen bzw. Gott-artigen, wird mit analytischen Methoden die notwendige Existenz Gottes gefolgert. Man kann also vereinfachend sagen, dass die Existenz Gottes sich aus der abstrakten Definition des Gottesbegriffes ergibt.

Was hat Gödel dazu getrieben, sich mit dieser Frage zu beschäftigen?

Christoph Benzmüller: Über Gödels Religiosität wurde vereinzelt spekuliert, daran möchte ich mich nicht beteiligen. Gesicherte Quellen sind mir nicht bekannt. Lediglich von seiner Frau Adele weiß man, dass er die Bibel regelmäßig las. Gödel pflegte wohl einen sehr privaten Umgang mit dem Thema Religion, und vermutlich aus diesem Grund hat er seinen Beweis auch nie publiziert. Unabhängig von einer nicht auszuschließenden religiösen Motivation gehe ich aber fest davon aus, dass Gödel ein sehr tiefes Interesse an den logischen und begrifflichen Aspekten ontologischer Beweise hatte. Es ist auch wenig verwunderlich, dass er sich insbesondere mit der Arbeit von Leibniz beschäftigte. Leibniz' Arbeiten und Visionen zur Logik waren seiner Zeit weit voraus gewesen und hatten starken Einfluss auf die rasanten Entwicklungen im Gebiet gegen Ende des 19. und zu Beginn des 20. Jahrhunderts. Gödel kann man durchaus als Logik-Rockstar des frühen 20. Jahrhunderts bezeichnen.

Ontologische Beweise sind recht alt. Was ist neu beim Rockstar Gödel?

Christoph Benzmüller: Zahlreiche namhafte Philosophen haben sich mit Gottesbeweisen beschäftigt, unter anderem auch Descartes und Spinoza. Das Proslogion von St. Anselm von Canterbury wird oft als ein Ausgangspunkt dieser Arbeiten genannt.

Gödels ontologischer Beweis ist, wie bereits angedeutet, angelehnt an die Arbeit von Leibniz. Gödel verwendet abstrakte Begriffe wie "positive Eigenschaft", "Gott-artig", "Essenz", und "notwendige Existenz". Auf eine Diskussion von Instanzen "positiver Eigenschaften" lässt er sich aber beispielsweise nicht ein. Ein Gott-artiges Wesen bei Gödel hat zudem alle positiven Eigenschaften, bei Leibniz nicht unbedingt. Gödel arbeitet mit wenigen Grundannahmen. Diese Grundannahmen bestehen bei ihm aus 5 Axiomen und den abstrakten Definitionen für "Gott-artig", "Essenz", und "notwendige Existenz".

Können Sie mit einfachen Worten ein, zwei Gödel-Axiome erläutern?

Christoph Benzmüller: Nehmen wir die beiden ersten Gödelschen Axiome. Das erste Axiom sagt, dass eine Eigenschaft positiv ist oder ihre Negation, niemals aber beides. Das zweite Axiom sagt, dass Eigenschaften, die notwendigerweise aus einer positiven Eigenschaften folgen, ebenfalls positiv sein müssen. Das ist auch schon alles, was Gödel über positive Eigenschaften in seinem ontologischen Beweis voraussetzt. Beide Axiome drückt er dann in der formalen Sprache der Logik aus.

Die Rahmenbedingungen für logische Formalisierungen stimmten bei Gödel. Seine Arbeit entstand nämlich zu einer Zeit, in der die formale Logik einen hohen Reifegrad erlangt hatte, nicht zuletzt durch Gödels bahnbrechende eigene Beiträge. Insbesondere mit der so genannten "Modallogik" stand ein gut entwickelter Logikformalismus zu Verfügung, der einen adäquaten und gut untersuchten Umgang mit den Begriffen "notwendig" und "möglich" unterstützte. Gödel beschreibt den von ihm gewählten Logikformalismus aber leider nicht mit letzter Konsequenz.

In diesem Punkt konnten unseren aktuellen Arbeiten interessante Einsichten liefern. Wir haben festgestellt, dass eine sehr schwache Modallogik, die so genannte Logik KB, die auf vergleichsweise wenigen Grundannahmen beruht, bereits eine erfolgreiche Beweisführung ermöglicht. Viele Arbeiten über Gödels Gottesbeweis erwähnen hier aber die stärkere Logik S5, und diese wurde in diesem Zusammenhang auch kritisiert. Wir wissen nun also, dass diese Kritik wohl gegenstandslos ist.