Kurt Gödel’s Gottesbeweis auf dem Computer

Dem Philosophen Gottfried Wilhelm Leibniz schwebte die Idee vor, philosophische Argumente --- einschließlich Argumente für oder gegen die Existenz Gottes --- in einer formalen Logiksprache zu notieren und die Korrektheit dieser Argumente dann mithilfe von Rechenmaschinen mechanisch zu überprüfen. Mit dieser Vision war Leibniz seiner Zeit weit voraus und wichtige Voraussetzungen fehlten ihm noch. Erst mit der Erfindung des Computers, der Entwicklung ausdrucksstarker Logiksprachen und der Programmierung leistungsfähiger Logikmaschinen (sogenannter Theorembeweiser) wurde seine Idee nun realisierbar.

Im Vortrag  werden wir die Leibniz'sche Vision am Beispiel eines Gottesbeweises beleuchten. Insbesondere werden wir den ontologischen Gottesbeweis des berühmten Mathematikers Kurt Gödel skizzieren und dessen Korrektheit dann mit einer Logikmaschine analysieren. Sogar bisher unbekannte Aspekte zu Gödel's Gottesbeweis konnte der Computer automatisch aufdecken.

Vortrag um 17 Uhr im Hörsaal der Takustr. 9