Mittwoch, 28. August 2013
Computerverifikations des Gödelschen Gottesbeweises
klauslange,01:09h
Kurt Gödel hat der Nachwelt in seinem Nachlass einen ontologischen Gottesbeweis hinterlassen.
Er benutzt dabei die höherstufige Modallogik und es war bislang nicht möglich, alle seine Schliessungen korrekt nachzuvollziehen.
Dies ist nun mit Computerhilfe eindeutig gelungen und damit konnte die Korrektheit von Gödels ontologischer Gottesbeweis endgültig bestätigt werden.
Dazu gibt es einen sehr ausführliches Interview mit einem der Forscher, der diese Verifikation geleistet hat, auf Telepolis, die ja alles andere als religionsfreundlich sind.
Daraus:
Nehmen wir die beiden ersten Gödelschen Axiome. Das erste Axiom sagt, dass eine Eigenschaft positiv ist oder ihre Negation, niemals aber beides. Das zweite Axiom sagt, dass Eigenschaften, die notwendigerweise aus einer positiven Eigenschaften folgen, ebenfalls positiv sein müssen. Das ist auch schon alles, was Gödel über positive Eigenschaften in seinem ontologischen Beweis voraussetzt. Beide Axiome drückt er dann in der formalen Sprache der Logik aus.
Die Rahmenbedingungen für logische Formalisierungen stimmten bei Gödel. Seine Arbeit entstand nämlich zu einer Zeit, in der die formale Logik einen hohen Reifegrad erlangt hatte, nicht zuletzt durch Gödels bahnbrechende eigene Beiträge. Insbesondere mit der so genannten "Modallogik" stand ein gut entwickelter Logikformalismus zu Verfügung, der einen adäquaten und gut untersuchten Umgang mit den Begriffen "notwendig" und "möglich" unterstützte. Gödel beschreibt den von ihm gewählten Logikformalismus aber leider nicht mit letzter Konsequenz.
In diesem Punkt konnten unseren aktuellen Arbeiten interessante Einsichten liefern. Wir haben festgestellt, dass eine sehr schwache Modallogik, die so genannte Logik KB, die auf vergleichsweise wenigen Grundannahmen beruht, bereits eine erfolgreiche Beweisführung ermöglicht. Viele Arbeiten über Gödels Gottesbeweis erwähnen hier aber die stärkere Logik S5, und diese wurde in diesem Zusammenhang auch kritisiert. Wir wissen nun also, dass diese Kritik wohl gegenstandslos ist...
Modallogiken sind Erweiterungen der klassischen Logik. Letztere führt prominente logische Verknüpfungen ein, dazu gehören: "nicht", "und", "oder", "es folgt", "äquivalent" und "für alle x gilt". Die klassische Logik unterstützt aber keinen adäquaten Umgang mit zentralen Begriffen hinsichtlich Zeit, Raum, Wissen, Glauben, und auch nicht mit Begriffen wie "notwendigerweise gilt" bzw. "möglicherweise gilt", wie hier erforderlich. Modallogiken erweitern deshalb die klassische Logik um entsprechende logische Operatoren; typischerweise werden diese notiert als "[]" und "<>". 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. Hier wird also eine universelle Aussage für alle Eigenschaften getroffen, und dazu stellt die Logik höherstufige Quantoren bereit. In der Formelsprache drückt Gödel dies wie folgt aus:
Gott-artig(x) <-> All P [ positiv(P) -> P(x) ]
Die Mechanisierung und Automatisierung von Logik auf dem Computer - man bezeichnet solche Computerprogramme auch als "Theorembeweiser" - hat seit der Jahrtausendwende sehr gute Fortschritte gemacht. Dies betrifft aber vor allem Theorembeweiser für ausdrucksarme, eingeschränkte Logiken, beispielsweise solche ohne Quantoren oder zumindest ohne höherstufige Quantoren. Höherstufige Logik, wie hier erforderlich, wird von theoretischen Informatikern aufgrund ihrer schlechten Komplexitätseigenschaften oft sogar als nicht handhabbar eingeordnet - teilweise zu Unrecht, wie unsere erfolgreiche Arbeit nun zeigt.
Was war eine besondere Herausforderung?
Christoph Benzmüller: Ein besonderes Problem für unsere Arbeit war, dass es für die höherstufige Modallogik bisher noch keine implementierten Theorembeweiser gab. Bei höherstufigen klassischen Logiken sieht es besser aus, mittlerweile gibt es hier zuverlässige und leistungsfähige Systeme; auch ich entwickle seit etwa 15 Jahren einen solchen Theorembeweiser.
Für Gödels Gottesbeweis wendeten wir einen Trick an, der es uns ermöglicht, höherstufige Modallogiken mithilfe letzterer Systeme zu mechanisieren und zu automatisieren. Dieser Trick beruht auf eigenen Arbeiten, die zum Teil mit Larry Paulson von der Universität Cambridge entstanden sind. Diese Arbeiten zeigen, wie man höherstufige Modallogik in die höherstufige klassische Logik einbetten kann, bzw. darin simulieren kann. Die klassische Logik höherer Stufe wird dabei als eine Art universelle Logik (mit Einschränkungen) verstanden und eingesetzt.
Siehe insbesondere Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Er benutzt dabei die höherstufige Modallogik und es war bislang nicht möglich, alle seine Schliessungen korrekt nachzuvollziehen.
Dies ist nun mit Computerhilfe eindeutig gelungen und damit konnte die Korrektheit von Gödels ontologischer Gottesbeweis endgültig bestätigt werden.
Dazu gibt es einen sehr ausführliches Interview mit einem der Forscher, der diese Verifikation geleistet hat, auf Telepolis, die ja alles andere als religionsfreundlich sind.
Daraus:
Nehmen wir die beiden ersten Gödelschen Axiome. Das erste Axiom sagt, dass eine Eigenschaft positiv ist oder ihre Negation, niemals aber beides. Das zweite Axiom sagt, dass Eigenschaften, die notwendigerweise aus einer positiven Eigenschaften folgen, ebenfalls positiv sein müssen. Das ist auch schon alles, was Gödel über positive Eigenschaften in seinem ontologischen Beweis voraussetzt. Beide Axiome drückt er dann in der formalen Sprache der Logik aus.
Die Rahmenbedingungen für logische Formalisierungen stimmten bei Gödel. Seine Arbeit entstand nämlich zu einer Zeit, in der die formale Logik einen hohen Reifegrad erlangt hatte, nicht zuletzt durch Gödels bahnbrechende eigene Beiträge. Insbesondere mit der so genannten "Modallogik" stand ein gut entwickelter Logikformalismus zu Verfügung, der einen adäquaten und gut untersuchten Umgang mit den Begriffen "notwendig" und "möglich" unterstützte. Gödel beschreibt den von ihm gewählten Logikformalismus aber leider nicht mit letzter Konsequenz.
In diesem Punkt konnten unseren aktuellen Arbeiten interessante Einsichten liefern. Wir haben festgestellt, dass eine sehr schwache Modallogik, die so genannte Logik KB, die auf vergleichsweise wenigen Grundannahmen beruht, bereits eine erfolgreiche Beweisführung ermöglicht. Viele Arbeiten über Gödels Gottesbeweis erwähnen hier aber die stärkere Logik S5, und diese wurde in diesem Zusammenhang auch kritisiert. Wir wissen nun also, dass diese Kritik wohl gegenstandslos ist...
Modallogiken sind Erweiterungen der klassischen Logik. Letztere führt prominente logische Verknüpfungen ein, dazu gehören: "nicht", "und", "oder", "es folgt", "äquivalent" und "für alle x gilt". Die klassische Logik unterstützt aber keinen adäquaten Umgang mit zentralen Begriffen hinsichtlich Zeit, Raum, Wissen, Glauben, und auch nicht mit Begriffen wie "notwendigerweise gilt" bzw. "möglicherweise gilt", wie hier erforderlich. Modallogiken erweitern deshalb die klassische Logik um entsprechende logische Operatoren; typischerweise werden diese notiert als "[]" und "<>". 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. Hier wird also eine universelle Aussage für alle Eigenschaften getroffen, und dazu stellt die Logik höherstufige Quantoren bereit. In der Formelsprache drückt Gödel dies wie folgt aus:
Gott-artig(x) <-> All P [ positiv(P) -> P(x) ]
Die Mechanisierung und Automatisierung von Logik auf dem Computer - man bezeichnet solche Computerprogramme auch als "Theorembeweiser" - hat seit der Jahrtausendwende sehr gute Fortschritte gemacht. Dies betrifft aber vor allem Theorembeweiser für ausdrucksarme, eingeschränkte Logiken, beispielsweise solche ohne Quantoren oder zumindest ohne höherstufige Quantoren. Höherstufige Logik, wie hier erforderlich, wird von theoretischen Informatikern aufgrund ihrer schlechten Komplexitätseigenschaften oft sogar als nicht handhabbar eingeordnet - teilweise zu Unrecht, wie unsere erfolgreiche Arbeit nun zeigt.
Was war eine besondere Herausforderung?
Christoph Benzmüller: Ein besonderes Problem für unsere Arbeit war, dass es für die höherstufige Modallogik bisher noch keine implementierten Theorembeweiser gab. Bei höherstufigen klassischen Logiken sieht es besser aus, mittlerweile gibt es hier zuverlässige und leistungsfähige Systeme; auch ich entwickle seit etwa 15 Jahren einen solchen Theorembeweiser.
Für Gödels Gottesbeweis wendeten wir einen Trick an, der es uns ermöglicht, höherstufige Modallogiken mithilfe letzterer Systeme zu mechanisieren und zu automatisieren. Dieser Trick beruht auf eigenen Arbeiten, die zum Teil mit Larry Paulson von der Universität Cambridge entstanden sind. Diese Arbeiten zeigen, wie man höherstufige Modallogik in die höherstufige klassische Logik einbetten kann, bzw. darin simulieren kann. Die klassische Logik höherer Stufe wird dabei als eine Art universelle Logik (mit Einschränkungen) verstanden und eingesetzt.
Siehe insbesondere Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
... comment
