Beweis ist bewiesen

Kurt Gödels Gottesbeweis ist richtig

1941 entwickelte Kurt Gödel eine hochkomplexe Formel, um Gott zu beweisen. Der Freund von Albert Einstein lag richtig. Zu dem Schluss sind nun zwei Computerwissenschaftler gekommen.

Kurt Gödel (rechts) mit Albert Einstein im «Institute for Advanced Study» in Princeton (NJ, USA)

Jetzt sind die letzten Zweifel ausgeräumt: Gott existiert tatsächlich. Zu diesem Schluss kommt der «Spiegel». Die Rechnung stammt von Computerwissenschaftler Christoph Benzmüller von der Freien Universität Berlin, zusammen mit Bruno Woltzenlogel Paleo von der technischen Universität Wien. Die Formelfolge entwickelte der österreichische Mathematiker Kurt Gödel anno 1941 auf ein paar losen Blättern Papier. An den Formeln feilte er in den nächsten Jahrzehnten.

«Keine Minute brauchte der Computer, um Gödels Beweis für gültig zu befinden», bilanziert der «Spiegel». Somit könne die Existenz Gottes fortan als gesichertes logisches Theorem gelten.

300 Zeilen lang

Kurt Gödel, einer der bedeutendsten Logiker des 20. Jahrhunderts, hielt seinen Gottesbeweis mehrere Jahrzehnte geheim. Gödel war vor den Nationalsozialisten aus Wien in die Universitätsstadt Princeton geflohen, wo er regelmässig mit Albert Einstein durch Parks spazierte. Unter Wissenschaftlern geniesst Gödel ein mit Einstein vergleichbares Ansehen.

Sein Schweigen brach er erst ein paar Jahre vor seinem Tod. Sein Beweis besteht aus komplexen Formeln, in der Modallogik zweiter Stufe. Als erstes bewies er, dass Gott möglicherweise existiere, später, dass er definitiv existiert. Der Beweis ist knapp 300 Zeilen lang.

Höherstufige Logik

Benzmüller laut der Zeitschrift «Pro»: «Besonders kompliziert wird es bei der klassischen Logik und insbesondere bei der Modallogik, wenn höherstufige Quantoren ins Spiel kommen. Ein Beispiel für einen höherstufigen Quantor findet sich in Gödels Definition von «Gott-artig». In natürlicher Sprache ausgedrückt besagt diese: «Ein Wesen ist 'Gott-artig', falls es alle positiven Eigenschaften aufweist.» Die Automatisierung von Logik auf dem Computer habe jedoch in den vergangenen Jahren derartig Fortschritte gemacht, dass auch höherstufige Logik verarbeitet werden könne, die normalerweise von theoretischen Informatikern aufgrund ihrer Komplexität oft sogar als nicht handhabbar eingeordnet werde.

Zum Thema:
Den kennenlernen, mit dem Kurt Gödel rechnete