Computer beweist die Existenz Gottes
Gödels Gottesbeweis
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 [1].Der KI-Wissenschaftler Prof. Dr. Raul Rojas hat mit Prof. Dr. Christoph Benzmüller [2] 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.
Theorembeweiser für die höherstufige Modallogik
Etwas langsamer. Was ist die Modallogik und wo liegt die Schwierigkeit, sie im Computer zu behandeln?
Christoph Benzmüller: Modallogiken sind Erweiterungen der klassischen Logik. Letztere führt prominente logische Verknüpfungen ein, dazu gehören: "nicht", "und", "oder", "es folgt", "äquivalent" und "für alle x gilt". Die klassische Logik unterstützt aber keinen adäquaten Umgang mit zentralen Begriffen hinsichtlich Zeit, Raum, Wissen, Glauben, und auch nicht mit Begriffen wie "notwendigerweise gilt" bzw. "möglicherweise gilt", wie hier erforderlich. Modallogiken erweitern deshalb die klassische Logik um entsprechende logische Operatoren; typischerweise werden diese notiert als "[]" und "<>". 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. Hier wird also eine universelle Aussage für alle Eigenschaften getroffen, und dazu stellt die Logik höherstufige Quantoren bereit. In der Formelsprache drückt Gödel dies wie folgt aus:
Gott-artig(x) <-> All P [ positiv(P) -> P(x) ]
Die Mechanisierung und Automatisierung von Logik auf dem Computer - man bezeichnet solche Computerprogramme auch als "Theorembeweiser" - hat seit der Jahrtausendwende sehr gute Fortschritte gemacht. Dies betrifft aber vor allem Theorembeweiser für ausdrucksarme, eingeschränkte Logiken, beispielsweise solche ohne Quantoren oder zumindest ohne höherstufige Quantoren. Höherstufige Logik, wie hier erforderlich, wird von theoretischen Informatikern aufgrund ihrer schlechten Komplexitätseigenschaften oft sogar als nicht handhabbar eingeordnet - teilweise zu Unrecht, wie unsere erfolgreiche Arbeit nun zeigt.
Was war eine besondere Herausforderung?
Christoph Benzmüller: Ein besonderes Problem für unsere Arbeit war, dass es für die höherstufige Modallogik bisher noch keine implementierten Theorembeweiser gab. Bei höherstufigen klassischen Logiken sieht es besser aus, mittlerweile gibt es hier zuverlässige und leistungsfähige Systeme; auch ich entwickle seit etwa 15 Jahren einen solchen Theorembeweiser.
Für Gödels Gottesbeweis wendeten wir einen Trick an, der es uns ermöglicht, höherstufige Modallogiken mithilfe letzterer Systeme zu mechanisieren und zu automatisieren. Dieser Trick beruht auf eigenen Arbeiten, die zum Teil mit Larry Paulson von der Universität Cambridge entstanden sind. Diese Arbeiten zeigen, wie man höherstufige Modallogik in die höherstufige klassische Logik einbetten kann, bzw. darin simulieren kann. Die klassische Logik höherer Stufe wird dabei als eine Art universelle Logik (mit Einschränkungen) verstanden und eingesetzt.
Neue Perspektiven für eine Computer-assistierte theoretische Philosophie bzw. Metaphysik
Müssen wir jetzt alle zur Kirche?
Christoph Benzmüller: 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. Zunächst steht also die übergeordnete Frage im Raum, welche Herangehensweise an das Thema jeder Einzelne für sich akzeptiert und welche er grundsätzlich ablehnt. Die Reduzierung der Frage auf begrifflich-logische Untersuchungen wird von nicht wenigen als eine inakzeptable Extremform angesehen. Diese Form der Auseinandersetzung ist es aber, die das Logikgenie Kurt Gödel gewählt hat.
Selbst wenn wir die grundsätzliche Herangehensweise von Gödel akzeptieren, so gibt es dennoch Aspekte, die wir kritisch hinterfragen müssen. Eine zentrale Frage ist natürlich, ob wir Gödels Grundannahmen (d.h. seine abstrakten Begriffsdefinitionen und seine Axiome) sowie deren konkrete Kodierungen in dem zugrunde gelegten Logikformalismus akzeptieren. Eine dazu orthogonale Frage ist, ob der Logikformalismus adäquat gewählt ist. Akzeptieren wir aber all diese Punkte (Herangehensweise, Logikformalismus und Grundannahmen), so sollte man sich wohl auch mit der Konsequenz, der notwendigen Existenz Gottes, auseinandersetzten.
Ich muss zugeben, dass ich all diese Punkte für mich selbst noch nicht erschöpfend beantwortet habe, und möglicherweise war dies auch bei Gödel der Fall. Wie dem auch sei, unsere aktuellen Arbeiten eröffnen interessante neue Möglichkeiten, den Logikformalismus und die Grundannahmen als veränderbare Parameter aufzufassen und dann mit diesen Parametern im Theorembeweiser zu experimentieren. Dadurch sollte es uns möglich sein, die Stichhaltigkeit weiterer Gottesbeweise zu untersuchen und diese Gottesbeweise zu variieren, um möglicherweise neue Einsichten zu gewinnen. Man kann also sagen, dass wir interessante neue Perspektiven für eine Computer-assistierte theoretische Philosophie bzw. Metaphysik aufzeigen. Nicht mehr, aber auch nicht weniger.
Müssen alle Philosophen jetzt "Computer lernen"?
Christoph Benzmüller: Natürlich nicht. Die Philosophie ist ein sehr weites Feld und ontologische Beweise nehmen darin nur einen kleinen Raum ein. Allerdings war ich nach eigenen Recherchen recht erstaunt über die offensichtliche Lebendigkeit der Diskussionen auf diesem Gebiet. Auch finden sich viele Veranstaltungen zu diesem Thema im Philosophie-Lehrangebot an Universitäten.
Hätte diese Forschung eine Anwendung in der nicht-philosophischen bzw. rein mathematischen Praxis?
Christoph Benzmüller: In der Mathematik gibt es bereits interessante Anwendungen. Aktuell möchte ich hier auf die formale Verifikation des Beweises zur 400 Jahre alten Kepplerschen Vermutung durch Thomas Hales verweisen. Zuvor hatten die Gutachter der mathematischen Fachzeitschrift Annals of Mathematics vergeblich versucht, diesen Beweis zu verstehen, letztendlich haben sie aufgegeben. Thomas Hales wollte dies nicht akzeptieren und hat seinen Beweis nun mithilfe von interaktiven und automatischen Theorembeweisern verifiziert. Ein lesenswerter Aufsatz zu diesem Thema ist: In Computers We Trust? [3].
Natürlich ergeben sich Einsatzmöglichkeiten auch in vielen anderen Disziplinen: Wer solche abstrakte Begriffe formalisieren und mechanisieren kann, wie für ontologische Beweise erforderlich, der muss auch vor komplexen Begriffen aus anderen Disziplinen nicht zurückschrecken.
Christoph Benzmüller: Dann sagen wir mit Leibniz: "Lass uns rechnen!" Ich danke für dieses Gespräch.
URL dieses Artikels:
https://www.heise.de/-3503718
Links in diesem Artikel:
[1] http://arxiv.org/abs/1308.4526
[2] http://christoph-benzmueller.de/
[3] http://www.simonsfoundation.org/quanta/20130222-in-computers-we-trust/
Copyright © 2013 Heise Medien