Christoph Benzmüller vom Fachbereich Mathematik und Informatik an der Freien Universität Berlin und sein Wiener Kollege Bruno Woltzenlogel Paleo von der Technischen Universität Wien gelang es, mithilfe eines Computerprogramms, eines sogenannten Theorembeweisers, die logische Korrektheit eines Gottesbeweises von Kurt Gödel aus dem Jahr 1941 mit höchster mathematischer Präzision zu bestätigen. Wir haben nachgefragt.
Herr Benzmüller, wie bitte beweist man einen Gottesbeweis?
Bei den ontologischen Gottesbeweisen – angefangen von Anselm von Canterbury über Descartes und Leibniz bis hin zu Gödel – will man von der konkreten Erfahrung abstrahieren. Man bedient sich einer A-priori-Herangehensweise. Das heißt, man lässt alle Erfahrungen in der realen Welt außen vor und versucht, nur mit abstrakten Definitionen einen Begriff von Gott zu skizzieren. Ein solcher Beweis besteht aus einer Reihe von Annahmen, Definitionen und Schlüssen. Wir haben mittels eines selbst entwickelten Programms, eines sogenannten Theorembeweisers, nachgewiesen, dass Gödels Argument logisch korrekt ist.
Also man kann jetzt jemandem, der nicht an Gott glaubt, Ihren Beweis unter die Nase halten und sagen: „Gott gibt es!“
Nein. Wir haben nur gezeigt, dass Gödels Beweis – zumindest in einer der zwei überlieferten Fassungen – logisch korrekt ist.
Wenn ein Gottesbeweis nicht die Existenz Gottes beweist, was ist daran dann so interessant?
Es geht um begriffliche Klarheit, um größtmögliche Reduktion. Ontologische Gottesbeweise versuchen, mit möglichst wenigen Grundannahmen zu dem Schluss zu kommen: „Notwendigerweise existiert Gott.“ Diese Annahmen kann man dann natürlich – wenn man die Argumentationskette für logisch fehlerfrei hält – kontrovers diskutieren. Zum Beispiel, indem ich sage: „Gödels erstes Axiom: ‚Entweder eine Eigenschaft oder ihre Negation ist positiv‘ finde ich absurd, weil es keine neutralen Eigenschaften vorsieht. Deswegen ist für mich der Gottesbeweis hinfällig.”
Als Sie Ihren Theorembeweiser entwickelt haben, war es da von Anfang an Ihre Absicht, Gottesbeweise zu überprüfen?
Nein, wir sind bei der Suche nach Anwendungsmöglichkeiten auf Gödels Gottesbeweis gestoßen. Wir haben überlegt: Können wir das? Können wir das nicht? Sehr große Axiommengen kann der Beweiser noch nicht verarbeiten. Wir wussten, Gödels Gottesbeweis ist eine schöne, kleine, kompakte Arbeit, die eine ambitionierte und relevante Modallogik verwendet.
Das heißt, der Gottesbeweis war ein einfacher Startpunkt, um auszuprobieren, was Ihr Theorembeweiser leisten kann?
Exakt! Man muss sich nur einmal die Art der Argumentführung in den philosophischen Aufsätzen über ontologische Gottesbeweise anschauen. Da steht dann: „Satz eins lautet ...“, „Definition A lautet ...“, „hieraus ergibt sich ...“. Genau diese Schritte lassen sich direkt mit den Kapazitäten bearbeiten, die Theorembeweiser wie der unsrige heute bereits haben. Es passt wie die Faust aufs Auge!
Wie lange hat Ihr Computer denn an der Bestätigung des Gottesbeweises gerechnet?
Das geht ganz schnell. Wenn ich mich richtig erinnere: Theorem eins, ein paar Millisekunden. Erste Schlussfolgerung, weitere Millisekunden. Theorem zwei waren dann wenige Sekunden und die Aussage am Ende wieder ein paar Millisekunden. Das musste man bislang mühsam mit Bleistift und Papier ausrechnen. Man könnte sich auch vorstellen, dass ein Philosoph, der sich mit solch einer Beweisführung beschäftigt, einfach die Schritte formal ins System eingibt, eine Taste drückt und dann einfach zehn oder vielleicht dreißig Sekunden auf die Antworten wartet.
Interview: Martin Kaluza
