Gottesbeweis auf dem MacBook

Der Computer ist in alle Lebensbereiche vorgedrungen, um unser irdisches Dasein zu erleichtern und wir können heute jedes erdenkliche Problem mit Hilfe eines Computers effektiver und leichter lösen. Es scheint die Zeit gekommen, um auch die großen Fragen unserer Existenz an die Maschine outzusourcen, denn sie kennt die besseren Antworten.

Christoph Benzmüller von der Freien Universität Berlin und sein Kollege Bruno Woltzenlogel-Paleo von der Technischen Universität Wien haben dem Computer Kurt Gödels ontologischen Gottesbeweis beigebracht, eine Logik-Operation, die für Computer bis dahin als viel zu schwierig angesehen wurde. Der Macbook von Christoph Benzmüller stellte darauf hin einwandfrei fest, dass Gott nicht nur möglicherweise, sondern sogar zwangsläufig existieren muss. Die von Benzmüller und Paleo veröffentlichte Arbeit findest du auf arXiv.org.

Während sich seit der Antike Philosophen Gedanken über die Natur unseres Universums und die Existenz von göttlichen Wesen gemacht haben, dringt nun auch der Computer in diesen ihm bisher verwehrten Bereich vor: die Theologie. Die Zuständigkeit für die letzten Fragen der Menschheit geht von unserem Schöpfer auf fein säuberlich ausgeführte Logik-Operationen über. Auch wenn es heute noch surreal scheint, dass Computer sich Gedanken über die Existenz einer göttlichen Identität machen, ist die Frage, ob dies in der Zukunft möglich ist, unausweichlich geworden. Noch ist der Computer im Bereich der Philosophie nur eine Rechenmaschine, ein komplexer Taschenrechner. Doch Christoph Benzmüller sieht einer Zukunft entgegen, in der ein Computer auch die komplexesten Logikgebilde lösen kann. Ob er dann Gott nicht nur mathematisch beweisen kann, sondern auch das philosophische Denken übernehmen wird, bleibt wohl vorerst noch der Science-Fiction überlassen.

Bereits Douglas Adams demonstrierte in seinem weltberühmten Roman ,Per Anhalter durch die Galaxis', dass der Beweis Gottes fatale Folgen für den Glauben haben kann. So ist es nicht verwunderlich, dass die Argumentation Gott könne mit Hilfe von Rechenoperationen bewiesen werden, auch auf starken Widerstand stieß. Kurt Gödels Herangehensweise widerstrebte Theisten, denn sie glauben an die Unbeweisbarkeit des Göttlichen oder unterstellen Gödel, dass seine Grundannahmen fehlerhaft sind. Nicht umsonst verheimlichte Gödel seinen bereits 1941 aufgestellten ontologischen Gottesbeweis.

Der Mathematiker Kurt Gödel gilt als einer der bedeutendsten Logiker des 20 Jahrhunderts, beschäftigte sich mit Prädikatenlogik und leistete einen Beitrag zu Einsteins Relativitätstheorie. Sein zwei Seiten fassendes Manuskript mit dem Gottesbeweis wurde erst 1970, nach seinem Tod, durch Dana Scott, einen seiner Studenten, an die Öffentlichkeit getragen. Benzmüller und Paleo zeigten jetzt mit dem Computer, dass die in Gödels Manuskript durchgeführte Beweisführung sich als wahr herausstellte. Wir haben uns mit Christoph Benzmüller, einem Vordenker auf dem Gebiet der Automatisierung von ausdrucksstarken Logiken, über die Beweisbarkeit von Gott mit Hilfe der Mathematik und des Computers unterhalten.

Mit deinem Kollegen Bruno Woltzenlogel-Paleo hast du die Existenz Gottes mit einem Macbook bewiesen, was muss ich mir darunter vorstellen?
Ausgehend von den Grundannahmen in Kurt Gödel's ontologischem Argument haben wir das Theorem „Notwendigerweise existiert Gott“ mit dem Computer beweisen können. In der Mathematik kennen wir Theoreme wie „Wurzel von 2 ist irrational" und das beweisen wir dann mit dem vorausgesetzten Wissen über die Zahlen. Hier ist das ähnlich. Der Computer beweist die Aussage: „Notwendigerweise existiert Gott" und dafür verwendet er die von Gödel vorgeschlagenen Definitionen und Axiome.

Kann ich also einfach irgendwelche Grundannahmen erfinden. Gott also fünf beliebige mathematische Eigenschaften zuteilen und so relativ einfach seine Existenz beweisen?
Gödel hat nicht irgendwelche Annahmen herangezogen, sondern er bezieht sich auf eine lange Tradition. Ontologische Gottesbeweise gab es bereits bei Anselm von Canterbury, Descartes, und Leibniz. Auch auf die Kritik von Kant geht Gödel in seiner Arbeit ein. Gödels Arbeit steht also nicht im leeren Raum. Der Realitätsbezug von Gödels Grundannahmen ist dennoch nicht leicht ersichtlich. Aber auch in der Mathematik ist der Realitätsbezug nicht immer klar erkennbar, oder ist dir schon mal eine reelle Zahl begegnet?

Ne noch nicht, aber Gott auch nicht.
Eben, genau! Wichtig bei Gödels Beweis ist also die kritische Auseinandersetzung mit den Grundannahmen. Sehr provokant formuliert ist in der Mathematik die Grundlagensituation aber sogar noch unklarer. Die Konsistenz der Arithmetik ist beispielsweise nicht gesichert. Die Widerspruchsfreiheit von Gödels Grundannahmen konnten unsere Theorembeweiser hingegen nachweisen.

Christoph Benzmüller zeigt uns die Operation auf seinem Laptop | Foto: Max Thesseling

Werden also bei Gödels Gottesbeweis die richtigen Grundannahmen getroffen?
Zunächst sollten wir darüber reden, ob ein ontologischer Gottesbeweis eine grundsätzlich geeignete Herangehensweise darstellt, um die Frage zur „Existenz Gottes“ zu klären. Viele Religionen würden dazu sagen: Nein, hier muss man Glauben in den Mittelpunkt stellen. Diese Haltung ist durchaus nachvollziehbar. Wenn man sich aber mit dem Geist, dem reinen rationalen Denken bemühen möchte, dann ist das Vorgehen durchaus plausibel und analog zu dem was man in der Mathematik tut. Gödel reduziert die Aussage über die notwendige Existenz Gottes auf Axiome und Definitionen. Und diese Grundannahmen muss man dann kritisch hinterfragen. Das ist Aufgabe der Philosophie und Theologie.

Welche Eigenschaften hat Gott also aus Sicht von Gödel?
Ein gottartiges Wesen wird als ein Wesen definiert, dem alle positiven Eigenschaften zukommen. Das ist ja jetzt nicht so auffallend widersprüchlich formuliert. Oder wie würdest du das sehen?

Für mich wirkt das total vage.
Genau, da sind wir ja schon bei der Idee. Gödel sagt, ich formuliere den Begriff mit möglichst wenig konkreter Erfahrung, mit möglichst wenig aus der realen Welt. Die Frage nach Gott wird somit auf ein abstraktes Gedankenexperiment reduziert.

Mit einem klassisch religiösen Verständnis von Gott hat das dann aber relativ wenig zu tun?
Das Endresultat scheint diesem aber auch nicht zu widersprechen, auch wenn es auf einer völlig anderen Herangehensweise beruht. Bei Religionen steht eben typischerweise der Glaube im Mittelpunkt.

Welchen Nutzen ziehe ich als nicht-Theologe und nicht-Mathematiker aus dieser Erkenntnis?
Du kannst unseren Beitrag als eine Anregung zur Beschäftigung mit dem Thema ansehen. Nehmen wir mal für einen Augenblick an, dass du Interesse hast, die Frage nach der Existenz Gott selbst mit einem reinen rationalen Denken zu hinterfragen. Dann ist meine Frage an dich: Was gefällt dir an Gödels Gottesbeweis nicht und warum? Wie würdest du Gott definieren? Kannst Du dann die Existenz beweisen oder gar widerlegen?

Ich hab immer gedacht so etwas wäre unmöglich. Ist nicht die Haupteigenschaft von Gott, dass man ihn eben nicht beweisen kann?
Damit kritisierst Du die grundsätzliche Herangehensweise ontologischer Gottesbeweise. Du lehnst diese Form der abstrakten, rationalen Auseinandersetzung mit dem Thema also von vornherein ab. Der Beweis von Gödel ist für dich dann nicht relevant, und Du kannst und musst ihn auch nicht verstehen.

Ist das typische Kritik von Religionen?
Ja, das ist eine ernstzunehmende Kritik.

Und ist die auch berechtigt?
Ja. Ich bin als Wissenschaftler allerdings gerne bereit mich rational mit Dingen auseinander zu setzen. Mir erscheinen ontologische Gottesbeweise nicht grundsätzlich absurd oder ausgeschlossen. Aber ich habe selbst meine Probleme mit einzelnen Axiomen von Gödel und ich bin noch nicht davon überzeugt, dass diese ein rundes Bild abgeben. Der Realitätsbezug ist für mich also nicht geklärt.

Bei welchem Axiom kann dich persönlich Gödel nicht überzeugen?
Ein debattierbares Axiom besagt beispielsweise, dass eine Eigenschaft oder ihre Negation positiv ist. Kritiken an einzelnen Annahmen und Aspekten in Gödels Beweis wurden übrigens von mehreren Philosophen geäußert. Das Interessante ist, dass unsere Technik es uns nun erlaubt, auch viele dieser Kritiken im Computer auf ihre Stichhaltigkeit zu untersuchen. Das tun wir gerade.

Gödels Gottesbeweis, der sich durch eure Arbeit zwar bewahrheitet hat, ist also kein Grund wieder regelmäßig in die Kirche zu gehen?
Wenn es durch unsere Arbeit gelungen ist, die ein oder andere zur Auseinandersetzung mit dem Thema angeregt zu haben, dann ist das eine tolle Sache. Egal von welcher Seite. Es handelt sich hier um eine philosophisch und theologisch interessante Fragestellung, und diese ist von großer Bedeutung für jeden Einzelnen und für die Gesellschaft.

Kurt Gödel hat den Beweis ja eigentlich bereits 1941 erbracht. Warum hast du das jetzt mit dem Computer wiederholt?
Was uns angetrieben hat, war die Frage, ob unsere Computertechnik, dass sogenannte interaktive und automatische Theorembeweisen, schon weit genug entwickelt ist, um sich mit solch schwierigen Beweisen beschäftigen zu können. Dies ist der Fall, wie wir gezeigt haben. Das Schöne ist, dass wir jetzt sehr einfach die Grundannahmen in Gödels Beweis als veränderbare Parameter ansehen können und entsprechende Varianten des Beweises mit dem Computer durchspielen können. In der theoretischen Philosophie musste man das bisher mühsam mit Papier und Bleistift tun.

Ich kann also jetzt meine eigenen Annahmen treffen, wie Gott zu sein hat und das dann in dein Model eingeben und der Computer rechnet aus, ob er unter diesen Voraussetzung existiert?
Exakt. Unsere Arbeit eröffnet aber noch weitere Perspektiven. In der theoretischen Philosophie gibt es eine große Bandbreite an Logiken. Viele davon galten bisher aber als nicht-automatisierbar. Automatische Theorembeweiser entwickelte man bisher in erster Linie für einfachere Logiken, zum Beispiel für die Prädikatenlogik erster Stufe und die Aussagenlogik—Studienanfänger in der Mathematik oder Informatik kennen das. Für fortgeschrittene, ausdrucksstarke philosophische Logiken, solche die Allaussagen über Prädikate zulassen und in denen es um mögliche Welten geht, gab es bisher keine Theorembeweiser. Wir haben gezeigt, dass dies auch hier durchaus möglich ist. Mit unserem Beitrag sind wir also der leibnizschen Vision einer Computer-assistierten theoretischen Philosophie etwas näher gekommen. Wir möchten dieser eine Art Logikassistenten zur Verfügung stellen, der dabei hilft präzise zu arbeiten. Ungefähr so wie der Taschenrechner hilft eine fehlerfreie Steuererklärung zu erstellen. Wenn du deine Steuererklärung machst, dann kriegst du das doch sicher auch nicht ohne Taschenrechner fehlerfrei hin?

Ne, dabei lass ich mir komplett vom Computer helfen. Der sagt mir dann wo ich da was eintragen muss. Und das gibt es jetzt auch für Philosophen?
Wir möchten ein Werkzeug bereitstellen, das theoretischen Philosophen das formale, logische Arbeiten erleichtern kann. Das Überprüfen der logischen Korrektheit von Gödels Gottesbeweis ist hier als Anwendungsbeispiel zu sehen. Andere Fragen sind dadurch aber nicht berührt und bleiben dem Menschen vorbehalten. Hierzu zählt auch die Klärung des Realitätsbezugs von Gödels Grundannahmen.

Können Computer auch solche Aufgaben in Zukunft übernehmen? Oder wird ihnen das immer verwehrt bleiben?
Hier bin ich sehr skeptisch.

Foto: Max Thesseling

Also beweist der Computer Gott gar nicht?
Der Computer zeigt lediglich, dass die Aussage „Notwendigerweise existiert Gott“ aus den Grundannahmen von Gödel in einer bestimmten Logik gefolgert werden kann. Er sichert aber nicht die „Gültigkeit“ der Annahmen in der realen Welt. Es lohnt sich der Vergleich mit der Mathematik. Wenn der Computer beweist „es gibt keine größte Primzahl", würden viele das wohl einfach so akzeptieren. Ohne aber zu definieren, was eine Primzahl ist, und ohne weitere Annahmen zu treffen, kann man auch hier nichts beweisen. Bei Gödels Gottesbeweis ist das Spiel analog. Jetzt steht aber eine gewichtigere Aussage im Raum, und das hat zu heftigen Reaktionen geführt.

Klar, weil sich bei Religion die Menschen gleich persönlich angegriffen fühlen. Warst du selbst auch religiös motiviert?
Ich bin in einem religiösen Umfeld groß geworden, aber ich bin klarer Wissenschaftler. Religiosität war keine Motivation für unsere Arbeit. Was uns interessiert hat, ist die Logik. Mich interessiert aber auch die fundamentale Frage, wie weit kommen Computer in der Zukunft. Wo wird das enden mit der Entwicklung intelligenter Systeme. Im Schachspielen ist es bereits akzeptiert, dass kein Mensch mehr gegen die stärksten Computerprogramme gewinnt. Auch der Erfolg des Watson-Systems von IBM vor zwei Jahren gegen die besten Menschen im Jeopardy-Quiz hat mich beeindruckt. In viele weitere Domänen dringt der Computer gerade vor, und das hier kann man als eine weitere neue Domäne ansehen: das Mechanisieren und Automatisieren sehr ausdrucksstarker Logiken in der theoretischen Philosophie.