Die Widerspruchsfreiheit der Grundannahmen von Gödel konnte dabei vom Computer belegt werden. Zudem konnten die Wissenschaftler zeigen: Die nicht triviale Beweisführung kann vom Computer größtenteils vollautomatisch erzeugt werden. Das hatten die beiden Wissenschaftler nicht erwartet. Jenseits des Einsatzes von Theorembeweisern in der Philosophie und Mathematik könnten solche Systeme in der Zukunft bei Dialogsystemen eingesetzt werden, so dass Computer menschliche Argumentationsmuster verstehen und sogar ergänzen können.

Der von Gödel verwendete „Logikformalismus“ – eine sogenannte höherstufige Modallogik, die Begriffe wie „notwendig“ und „möglich“ verwendet – galt bisher als zu komplex und schwierig, um ihn auf dem Computer abzubilden und dort zu automatisieren. Verfügbare Theorembeweiser basieren zumeist auf weitaus einfacheren Formalismen. Um dieses Problem zu umgehen wendeten die Wissenschaftler eine Methode an, der es ihnen ermöglichte Gödels höherstufige Modallogik mithilfe bereits existierender Theorembeweiser zu automatisieren. Dieser Trick beruht wiederum auf theoretischen Arbeiten von Benzmüller und Paulson von der britischen University of Cambridge. Für die klassische Logik höherer Stufe wurden in den letzten beiden Jahrzehnten mehrere Theorembeweiser entwickelt. Diese konnten nun in der Arbeit von Benzmüller und Woltzenlogel Paleo erfolgreich eingesetzt werden. Auch ein von Benzmüller entwickelter Theorembeweiser kam dabei zum Einsatz.

Kurt Gödels mathematisierter Gottesbeweis wurde nach dessen Tod veröffentlicht. Es gehört zur Klasse der sogenannten ontologischen Beweise, die eine lange Tradition in der Philosophie haben: Als Konstruktionen des reinen Denkens wurden und werden sie seither sehr kontrovers in der Fachwelt diskutiert. Ausgehend von abstrakten Begriffen, die von der Erfahrung abstrahieren, wird in einem ontologischen Gottesbeweis mithilfe einer logischen Argumentation die Existenz Gottes aus wenigen Grundannahmen (Axiomen) gefolgert. Umgekehrt kann man sagen, dass die Existenz Gottes auf die Stichhaltigkeit der Axiome und abstrakten Begriffe reduziert wird.

Bekannte Philosophen haben sich intensiv mit ontologischen Gottesbeweisen beschäftigt, unter anderem St. Anselm, Descartes, Leibniz und Kant. Bei solchen Beweisen sind zwei Fragen wichtig: (A) Sind die jeweiligen Grundannahmen gültig und sinnvoll gewählt? (B) Ist die logische Argumentationskette tatsächlich fehlerfrei? Die Beschäftigung mit Frage (A) ist Aufgabe der Philosophie und Theologie, und ontologische Gottesbeweise wurden in diesem Punkt oft und zurecht heftig kritisiert. Die Beschäftigung mit Frage (B) ist Aufgabe der mathematischen und philosophischen Logik. Insbesondere für Gödels Gottesbeweis gilt aber, dass der verwendete Logikformalismus und die Gödelsche Beweisführung nicht trivial sind. Die Analyse der logischen Aspekte erfolgte bisher ausschließlich – mühsam und fehleranfällig – mit Papier und Bleistift.

Die beiden Wissenschaftler wollen Gödels Beweis nun weiter untersuchen und dabei auch auf jüngere Arbeiten eingehen, die tiefere logische Aspekte an Gödels Arbeit kritisieren. Auch andere ontologische Gottesbeweise wollen sie in der Zukunft mit ihrer Methode auf ihre logische Stichhaltigkeit überprüfen. Logikformalismus und Grundannahmen können dabei dann als veränderbare Parameter aufgefasst werden. Mit diesen Parametern wollen die Wissenschaftler dann im Theorembeweiser experimentieren, um neue Einsichten zur logischen Struktur der Argumente zu gewinnen. In dieser Hinsicht ergeben sich nach der Überzeugung der Wissenschaftler interessante Perspektiven für eine computer-assistierte theoretische Philosophie und Metaphysik; die Wissenschaftler erwarten die Stichhaltigkeit von Schlussfolgerungen aus Grundannahmen effektiv und flexibel überprüfen zu können.

Die uralte Frage nach der Existenz Gottes bleibt natürlich unbeantwortet und ist abhängig von Sinnhaftigkeit und Realitätsbezug der gewählten Grundannahmen. Gödels Argumentationskette ist jedoch nachweisbar korrekt – so viel hat der Computer nach Ansicht der Wissenschaftler nun gezeigt.

Eine Übersetzung von Gödels Beweisskizze (in der Version des Gödel-Schülers Dana Scott) aus der formalen Logik in die natürliche Sprache:

• Annahme 1: Entweder eine Eigenschaft oder ihre Negation ist positiv.
• Annahme 2: Eine Eigenschaft, die notwendigerweise durch eine positive Eigenschaft impliziert wird, ist positiv.
• Theorem 1: Positive Eigenschaften kommen möglicherweise einer existenten Entität zu.
• Definition 1: Eine gottähnliche Entität besitzt alle positiven Eigenschaften.
• Annahme 3: Die Eigenschaft, gottähnlich zu sein, ist positiv.
• Schlussfolgerung: Möglicherweise existiert Gott.
• Annahme 4: Positive Eigenschaften sind notwendigerweise positiv.
• Definition 2: Eine Eigenschaft ist Essenz einer Entität, falls sie der Entität zukommt und notwendigerweise alle Eigenschaften der Entität impliziert.
• Theorem 2: Gottähnlich zu sein ist eine Essenz von jeder gottähnlichen Entität.
• Definition 3: Eine Entität existiert genau dann notwendigerweise, wenn all ihre Essenzen notwendigerweise in einer existenten Entität realisiert sind.
• Annahme 5: Notwendigerweise zu existieren ist eine positive Eigenschaft.
• Theorem 3: Gott existiert notwendigerweise.