Am Computer haben Forscher bewiesen, dass es Gott gibt – ohne Glauben, rein anhand logischer Argumente.

Mit diesen Worten wird ein Artikel aus Blick am Abend vom 9. September eingeleitet. Sollte diese Aussage stimmen, würde dies nicht weniger als eine Revolution unseres Weltverständnisses bedeuten. Das, was seit Jahrtausenden Gegensand von Glaube war, wäre nun bewiesen, und die Idee von Gottheiten würde aus der Domäne der Religion zu einem – zu dem – Fundament einer jeden Wissenschaft erhoben. Ein neues Zeitalter der Menschheit würde eingeläutet.

In doppelter Hinsicht lohnt es sich, einen kurzen skeptischen Blick auf diese Geschichte zu werfen. Zum einen schlicht, um in Erfahrung zu bringen, was genau wie bewiesen wurde. Zum anderen ist Blick am Abend bei wissenschaftlichen Themen nicht immer die zuverlässigste Quelle.

Der «Gottesbeweis»

Der Blick am Abend-Artikel bezieht sich auf eine vor Kurzem erschienen Studie mit dem Titel «Formalization, Mechanization and Automation of Godel’s Proof of God’s Existence». Der Text ist inklusive Literaturverzeichnis nur zwei Seiten lang, aber der Grad der Erkenntnis einer Arbeit muss nicht mit deren Textlänge zusammenhängen.

In der Arbeit wird der ontologische Gottesbeweis des Mathematikers Kurt Gödel untersucht, welchen die Autoren in folgender modallogischer Form zusammenfassen:

Die interessierende Arbeit hat aber nicht wirklich geprüft, ob diese Argumentationskette logisch korrekt ist, sondern, wie gut sich die Korrektheit mit Hilfe von Computern berechnen lässt. Das Ganze ist denn auch eine Art «proof of concept» für computergestützte Theoremprüfung, wie die Autoren erklären:

This work attests the maturity of contemporary interactive and automated deduction tools for classical higher-order logic and demonstrates the elegance and practical relevance of the embeddings-based approach. Most importantly, our work opens new perspectives for a computer-assisted theoretical philosophy.

Gleichzeitig halten die Autoren fest:

The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility, but the computer can assist in building and checking rigorously correct logical arguments.

Das bedeutet also: Mittels Computer wurde bloss die logische Kohärenz des Gödelschen Gottesbeweises demonstriert, aber nicht die inhaltliche Wahrheit der Axiome. Dass logische Konsistenz nicht mit faktischer Wahrheit einhergeht, ist eine banale Erkenntnis und Bestandteil z.B. jedes Einstiegstextes zu Logik:

Der logische Gottesbeweis von Gödel (oder auch von anderen) sagt letztlich also nichts über die Existenz von Gottheiten aus. Kurioserweise tut sich einer der Autoren der Studie, Christoph Benzmüller, schwer mit diesem Umstand. Auf die Frage, ob wir nun alle zur Kirche müssten, Antworter Benzmüller in einem Interview bei heise online:

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.

Natürlich, wenn wir die unbewiesenen Grundannahmen akzeptieren, müssen wir auch die Konklusion akzeptieren. Oder anders ausgedrückt: Wer an Gott glauben will, glaubt daran.

Fazit: Wenn Wissenschaft zum PR-Stunt verkommt

Die Schlagzeile rund um den am Computer bewiesenen Gott riecht stark nach einer bewusst inszenierten PR-Aktion. Die computergestützte Theoremprüfung, um welche es in der Mini-Studie eigentlich geht, mag eine durchaus sinnvolle Bereicherung für bestimmte Aspekte der formalen Logik darstellen. Dass gerade Gödels Gottesbeweis als Anschauungsbeispiel verwendet wird, scheint in erster Linie strategisches Kalkül der Autoren. Blick am Abend hätte wohl kaum einen ganzseitigen Bericht ohne den Aufhänger «Gott mit Computer bewiesen!» gedruckt. «Computergestützte deduktive Logik kann ein robustes Werkzeug sein!» klingt irgendwie weniger spektakulär.

Dafür, dass diese Studie eine bewusste PR-Aktion darstellt, spricht womöglich auch die mediale Karriere der Studie. Nebst Blick am Abend haben einige andere (Online-)Medien darüber berichtet, u.a. Spiegel Online, die Frankfurter Allgemeine Zeitung, die Wiener Zeitung, ORF.at.

Der Ursprung der Geschichte scheint indes bei heise online zu liegen: Am 26. August erschienen dort ein Artikel sowie das bereits zitierte Interview. Die Person, die das Interview geführt hat, ist ein gewisser Raul Rojas. Raul Rojas ist aber nicht bloss Autor bei Telepolis (einem Sub-Magazin von heise.de), sondern auch Professor für künstliche Intelligenz an der Freien Universität Berlin. Einer der Studienautoren, Christoph Benzmüller, ist auch an der Freien Universität Berlin tätig. Im Interview unterhalten sich also zwei Kollegen und machen Werbung für Benzmüllers Forschung.

Telepolis beschreibt sich selber folgendermassen:

Unter «kritisch reflektieren» fällt dann wohl auch «Freunden und Bekannten eine unkritische PR-Plattform geben».

Es ist nicht sonderlich erstaunlich, dass bestimmte Medien Wissenschaft verzerrt und unkritisch widergeben. Wenn aber auch Forscherinnen und Forscher selber Medienlogiken derart verinnerlichen, dass sie ihre Arbeit möglichst mediengerecht gestalten, um Aufmerksamkeit zu haschen, ist eine rote Linie überschritten. Es ist so schlicht nicht mehr klar, was das eigentliche Ziel der Forschung ist: Neue wissenschaftliche Erkenntnisse oder maximale mediale Resonanz?

—

Dank an Felix Roth für den Hinweis auf den Blick am Abend-Artikel.