Pluto hat geschrieben:Wow!

Informatiker ließen einen Computer Gödels berühmten ontologischen Gottesbeweis nachrechnen!
[...]
wie denkt ihr darüber?
Möglich, oder nicht? — Oder gar fehlerhaft programmiert, oder einfach nur Pseudowissenschaft?
Um Pseudowissenschaft handelt es sich bei dieser Bestätigung von Gödels modallogischem Gottesbeweis ganz gewiss nicht, - es sei denn, man zählt Logik, KI-Forschung und Mathematik neuerdings unter die Pseudowissenschaften.
Fehlerhaft programmiert könnte nur der automatische Theorembeweiser sein, der eingesetzt wurde. Aber das ist sehr unwahrscheinlich.
Im Nachlass des österreichischen Logikers und Mathematikers Kurt Gödel fand man einen in formallogischer Sprache formulierten Gottesbeweis, der sich an den ontologischen Gottesbeweis Anselms von Canterburys anlehnt und der in mehreren Ableitungsschritten zu der Conclusio führt, dass
mit Notwendigkeit etwas in allen möglichen Welten existieren muss, dass alle positiven Eigenschaften in sich vereint, wobei - zu existieren - eine dieser positiven Eigenschaften ist (
nicht zu existieren, wird also als
negative Eigenschaft bestimmt).
Gott als etwas zu definieren, dass alle positiven Eigenschaften in sich vereint, entspricht Canterburys Definition Gottes als
dasjenige, über das hinaus nichts Vollkommeneres gedacht werden kann.
Gödel hat diesen Beweis geheimgehalten, weil er befürchtete, dass der Beweis missverstanden wird. Erwähnenswert ist noch, dass Kurt Gödel nach einhelliger Fachmeinung, der brillanteste Logiker des 20. Jahrhunderts war.
Kurt Gödel formulierte diesen Beweis in der Sprache eines bestimmten logischen Kalküls, welches man
Modallogik nennt und in der Modallogik in dem spezielleren System
S5, einem besonders ausdrucksmächtigen System. In der Modallogik ist es möglich Aussagen zu formulieren, die die Operatoren: "Es ist
möglich, dass ..." und "Es ist
notwendig, dass ..." enthalten.
Die beiden Logiker und Mathematiker Christoph Benzmüller und Bruno Woltzenlogel Paleo haben nun folgendes getan:
Zunächst haben sie Gödels in S5 formulierten Beweis in das etwas schwächere modallogische System KB übersetzt. Allein das ist schon eine erstaunliche Leistung. Dieser Vereinfachungsschritt war nötig, weil automatische Theorembeweiser mit dem modallogischen System S5 überfordert sind. Die Ausrucksmächtigkeit von S5 wird nämlich erkauft durch eine viel schwierigere Überprüfbarkeit. Das System KB ist weniger ausdrucksmächtig, dadurch aber leichter auf logische Inkonsistenzen und Widersprüche zu überprüfen.
Danach haben sie Gödels Beweis mit einem automatischen Theorembeweiser überprüft. Theorembeweiser sind Computerprogramme, die z.B. mathematische Theoreme daraufhin überprüfen, ob sie korrekt und widerspruchsfrei sind. Solche Theorembeweiser sind keine dummen Computerprogramme: es sind intelligente Programme, denn sie müssen Widersprüche in sehr komplexen Theoremen
aufspüren können, was eine Art
Intuition erfordert, genau in die Richtung zu suchen, wo sich Widersprüche ergeben können.
Die Überprüfung von Gödels Beweis ergab, dass sowohl die Axiome und Definitionen des Beweises, als auch seine logischen Ableitungen alle korrekt sind. Die Schlussfolgerung von Gödels logischen Gottesbeweis ist also korrekt:
Es existiert mit Notwendigkeit etwas in allen möglichen Welten, das alle positiven Eigenschaften in sich vereint. Gödel nennt das "Gott".
Ob man diesem Beweis etwas abgewinnen kann, hängt davon ab, ob man die Axiome und Definitionen Gödels teilt und darüber hinaus auch noch, ob man die axiomatischen Voraussetzungen des modallogischen Systems K akzeptiert. Sowohl die Axiome und Definitionen Gödels, als auch die Voraussetzungen des logischen Kalküls haben übrigens durchaus hohe Plausibilität.
http://page.mi.fu-berlin.de/cbenzmueller/papers/R54.pdf