Computerprogramm bestätigt Gödels Gottesbeweis
KI-Foscher haben einen maschinengestützten Theorembeweis entwickelt und damit, wie sie sagen, eine Grundlage für eine computer-assistierte Metaphysik gelegt
- Florian Rötzer
Wissenschaftlern der Freien Universität Berlin und der TU Wien ist es gelungen, Kurt Gödels berühmten Gottesbeweis mit einem Computerprogramm zu überprüfen. Die KI-Forscher Christoph Benzmüller und Bruno Woltzenlogel Paleo haben dazu die Technik des maschinengestützten Theorembeweises eingesetzt, die bislang vor allem für mathematische Fragestellungen verwendet wurde. Bei einem ontologischen Gottesbeweis, mit dem sich etwa Spinoza, Descartes, Leibniz oder Kant auseinandergesetzt haben, wird versucht, die Existenz Gottes aus dem Denken logisch abzuleiten.
Gödels ontologischer Gottesbeweis wurde im Nachlass des bekannten Mathematikers und Logikers gefunden und ist bislang nur von Philosophen logisch untersucht worden. Die KI-Professoren haben eine Variante des Beweises formalisiert und nachgewiesen, dass die Grundannahmen konsistent und die Argumentationskette korrekt ist. Die Beweisführung konnte fast vollautomatisch mit dem Computer erzeugt werden. Gödel lehnte sich an Leibniz an und geht von wenigen Grundannahmen wie Definitionen für "Gott-artig", "Essenz", und "notwendige Existenz" und Axiomen aus.
Die Argumentationsführung setzt aber eine höherstufige Modallogik voraus, für die es noch keine maschinengestützten Theorembeweise gab. Im Telepolis-Gespräch mit dem KI-Forscher Raul Rojas erklärt Christoph Benzmüller: "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 sich höherstufige Modallogik in die höherstufige klassische Logik einbetten lässt beziehungsweise darin simuliert werden kann. Die klassische Logik höherer Stufe wird dabei als eine Art universelle Logik (mit Einschränkungen) verstanden und eingesetzt."
Auch wenn formal die logische Argumentationskette korrekt ist und damit die Existenz Gottes nach den Axiomen und Grundannahmen von Gödel bewiesen wurde, ließen sich diese ebenso wie der Logikformalismus hinterfragen. Für Benzmüller eröffnet der entwickelte Ansatz die Möglichkeit, 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 beziehungsweise. Metaphysik aufzeigen. Nicht mehr, aber auch nicht weniger. "
Das Gespräch mit Prof. Dr. Christoph Benzmüller auf Telepolis:
(fr)
