Gott mathematisch bewiesen?

Kurt Gödel ist vor allem bekannt für seinen „Unvollständigkeitssatz“, einen der wichtigsten Sätze der modernen Logik. Er besagt, dass jedes formale System Sätze enthält, die man weder formal beweisen, noch widerlegen kann. Kurz gesagt zeigte Gödel, dass die Mathematik letztendlich nicht eindeutig widerspruchsfrei ist.

Gödel, der 1906 im damals österreichischen, heute tschechischen Brünn geboren wurde, reiste 1939 nach Amerika aus, weil er in Wien irrtümlich für einen Juden gehalten wurde. Nach seiner Einreise in die USA befasste er sich zunehmend mit Philosophie und Theologie. Seinen Gottesbeweis veröffentlichte er jedoch nie.

Gödels Gottesbeweis fußt auf Ansätzen von Gottfried Wilhelm Leibniz. Der Österreicher verwendete  eine Variation des ontologischen Gottesbeweises, der bereits von Anselm von Canterbury (1033 bis 1109) verfasst wurde. Demzufolge gehört es zu einem vollkommenen Wesen wie Gott, dass es auf jeden Fall auch die Eigenschaft besitzt, zu existieren. Denn sonst wäre es nicht vollkommen. Der Gott der Philosophen und Logiker hat dabei allerdings erst einmal nichts mit dem Gott irgendeiner Religion zu tun, sondern ist ein Gedankenkonstrukt, das die Eigenschaft besitzt, vollkommen zu sein.

Wenn mathematische Beweisführungen zu kompliziert werden, um sie mit Stift und Papier zu überprüfen, greifen Mathematiker heutzutage oft zu Computern. Diese „rechnen“ dann den Beweis  präzise nach und geben am Ende aus, ob der Beweis stichhaltig ist oder nicht. Man bezeichnet solche Computerprogramme als „Theorembeweiser“. Diese Methode wandten nun zwei Wissenschaftler auf den Gottesbeweis Gödels an.

Der Computerwissenschaftler Christoph Benzmüller von der Freien Universität Berlin veröffentlichte nun zusammen mit Bruno Woltzenlogel Paleo von der Technischen Universität Wien die Ergebnisse ihrer Untersuchung. Gegenüber dem Internet-Portal Telepolis sagte Benzmüller, ihm und seinem Kollegen sei es gelungen, „eine Variante von Gödels Gottesbeweis zu formalisieren und im Computer mit höchster mathematischer Präzision zu überprüfen“. Das Ergebnis: „Wir können nun also mit großer Gewissheit behaupten: Die logische Argumentationskette in diesem Gottesbeweis ist nachweisbar korrekt.“

Logik-Rockstar des 20. Jahrhunderts las die Bibel

Gödels Beweisführung verwendet dabei abstrakte Begriffe wie „positive Eigenschaft“, „Gott-artig“ und „notwendige Existenz“. Der erste Grundsatz (Axiom) besage, 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“, erklärt Benzmüller.

Die Schwierigkeit bei dem Beweis besteht laut dem Informatiker darin, dass die klassische Logik keinen adäquaten Umgang mit Begriffen hinsichtlich Zeit, Raum, Wissen und Glauben unterstützt. Die Modallogik Gödels erweitere deshalb die klassische Logik um entsprechende logische Operatoren. „Besonders kompliziert wird es bei der klassischen Logik und insbesondere bei der Modallogik, wenn höherstufige Quantoren ins Spiel kommen. Ein Beispiel für einen höherstufigen Quantor findet sich in Gödels Definition von ‚Gott-artig‘. In natürlicher Sprache ausgedrückt besagt diese: Ein Wesen ist ‚Gott-artig‘, falls es alle positiven Eigenschaften aufweist.“ Die Automatisierung von Logik auf dem Computer habe jedoch in den vergangenen Jahren derartig Fortschritte gemacht, dass auch höherstufige Logik verarbeitet werden könne, die normalerweise von theoretischen Informatikern aufgrund ihrer Komplexität oft sogar als nicht handhabbar eingeordnet werde.

Gödel könne man durchaus als „Logik-Rockstar des frühen 20. Jahrhunderts“ bezeichnen, sagt Benzmüller. Wie religiös der Mathematiker selbst gewesen sei, darüber könne man nur spekulieren. „Lediglich von seiner Frau Adele weiß man, dass er die Bibel regelmäßig las.“ Gödel habe offenbar einen sehr privaten Umgang mit dem Thema Religion gepflegt.

Auf die Frage „Müssen wir jetzt alle zur Kirche?“ antwortet der Berliner Forscher: „Es gibt sehr unterschiedliche Möglichkeiten, sich der Frage nach Gottes Existenz zu nähern. Häufig wird sie als eine reine Frage des Glaubens aufgefasst, und diese Sicht steht einer abstrakten, logik-zentrierten Herangehensweise, wie von Gödel praktiziert, entgegen.“ Die Frage, ob es Gott gibt oder nicht, müsse letztlich weiterhin jeder für sich beantworten. Viele lehnten eine formallogische Herangehensweise an diese Frage ohnehin ab. Eine zentrale Frage sei, „ob wir Gödels Grundannahmen sowie deren konkrete Kodierungen in dem zugrunde gelegten Logikformalismus akzeptieren. (…) Akzeptieren wir all diese Punkte (Herangehensweise, Logikformalismus und Grundannahmen), so sollte man sich wohl auch mit der Konsequenz, der notwendigen Existenz Gottes, auseinandersetzten.“

Ihre Arbeit eröffne interessante neue Möglichkeiten, die Stichhaltigkeit weiterer Gottesbeweise zu untersuchen und diese Gottesbeweise zu variieren, sagt Benzmüller. „Man kann also sagen, dass wir interessante neue Perspektiven für eine Computer-assistierte theoretische Philosophie beziehungsweise Metaphysik aufzeigen. Nicht mehr, aber auch nicht weniger.“

Christoph Benzmüller studierte an der Universität des Saarlandes Informatik und Computerwissenschaften, wo er auch 2007 habilitierte. Danach war er Professor an der privaten „International University in Germany“ in Bruchsal. Seit 2012 ist er Fellow an der Freien Universität Berlin. Er arbeitet auf dem Gebiet der Logik, der Künstlichen Intelligenz und Computerlinguistik.  Bruno Woltzenlogel Paleo forscht am Institut für Computersprachen an der Technischen Universität Wien. (pro)