Gödels Gott, maschinengeprüft: Der ontologische Beweis von Leibniz bis Lean

Teil der Sektion Philosophie — ergänzend zu Kants Fragen im Zeitalter der KI und Eine kurze Geschichte der Philosophie. Die hier diskutierte Lean-Formalisierung: github.com/drewarrowood/godel-ontological.

1970, in der Überzeugung zu sterben, ließ Kurt Gödel einem vertrauten Freund einen Beweis abschreiben, den er seit den 1940er Jahren mit sich herumtrug. Er hatte drei Jahrzehnte gezögert — aus einem bezeichnenden Grund: Er fürchtete, die Leute würden glauben, dass er tatsächlich an Gott glaube. Der Beweis war ontologisch — eine moderne, modale Rekonstruktion des Gottesbeweises von Anselm von Canterbury und Leibniz, verdichtet zu fünf Axiomen und einer kurzen Kette von Theoremen. Gödel, der größte Logiker des Jahrhunderts, hatte das älteste Argument der natürlichen Theologie in etwas verwandelt, das wie Mathematik aussieht: Definitionen, Axiome, Lemmata, eine Konklusion der Form notwendig existiert ein gottgleiche Wesen (□ ∃x GodLike(x)).

Die Notizen kursierten, Dana Scott reparierte sie, Christ Benzmüller und Bruno Woltzenlogel Paleo mechanisierten sie in Isabelle/HOL — automatische Theorembeweiser fanden heraus, dass Gödels unreparierte Axiome schlicht inkonsistent waren, und verifizierten Scotts Variante. Und inzwischen gibt es eine kleine, ehrliche Lean-4-Formalisierung, die die ganze Kette von Grund auf neu aufbaut: github.com/drewarrowood/godel-ontological. Fünf Axiome hinein, eine geboxte Existenzaussage hinaus, lake build grün, null sorry. Es ist ein herrliches Artefakt — und seine Lektüre ist eine Lektion darüber, was Beweise, Maschinen und Philosophie füreinander tun können und was nicht.

Ich möchte die Kette entlanggehen, denn die Kette ist das Argument — und dann die Frage stellen, die das Repo in seiner Ehrlichkeitsklausel selbst stellt: Was genau ist hier bewiesen worden?

Die Herkunftslinie, je ein Satz

• Anselm (1078): Gott ist „das, über das hinaus Größeres nicht gedacht werden kann". Wirklich zu existieren ist größer, als nur im Verstand zu existieren — also muss das größte Denkbare existieren.
• Descartes (1641): Existenz ist eine Vollkommenheit. Ich kann Gott nicht als existierend-aber-vernichtbar denken, ebenso wenig wie einen Berg ohne Tal.
• Leibniz (um 1700): Die Lücke ist die Möglichkeit. Wenn das vollkommenste Wesen möglich ist, dann — da Vollkommenheiten unbeschränkt sind — existiert es notwendig. Den Möglichkeitsteil des Beweises hat er nie fertiggestellt.
• Gödel (um 1941): Modalisiere es. Positive Eigenschaft statt Vollkommenheit, S5-Mögliche-Welten statt Verstand-gegen-Wirklichkeit — und Leibniz' fehlender Schritt fällt als Theorem heraus.

Jedes Glied hat Präzision hinzugefügt und, damit, Zerbrechlichkeit. Das sollte man bei allem Folgenden im Kopf behalten.

Die Axiome, die Definitionen, die Kette

Das Scott-Set arbeitet mit einem Metaprädikat Positive über Eigenschaften, starr über Welten gelesen: Eine Eigenschaft ist positiv gdw. ihre Negation nicht positiv ist (A1); was eine positive Eigenschaft notwendig impliziert, ist positiv (A2); gottgleich zu sein ist positiv (A3); positive Eigenschaften sind notwendig positiv (A4 — in der Lean-Kodierung fällt das gratis an, weil Positivität nicht weltenindiziert ist); und notwendige Existenz ist positiv (A5). Drei Definitionen erledigen den Rest: Gottgleich heißt, jede positive Eigenschaft zu besitzen (D1); ein Wesen (Essence) von x ist eine Eigenschaft, die x hat und die notwendig alles impliziert, was x hat (D2); und notwendige Existenz heißt, dass jedes Wesen notwendig instanziiert ist (D3).

Daraus fünf Schritte:

• T1. Jede positive Eigenschaft ist möglicherweise instanziiert. (Andernfalls ist sie nirgends instanziiert, also impliziert sie das Unmögliche, und die Negation kollabiert die Positivität selbst — Widerspruch.)
• C. Möglicherweise existiert ein gottgleiches Wesen. (Gottgleichheit ist positiv nach A3, möglich nach T1.)
• T2. Gottgleichheit ist das Wesen jedes gottgleichen Wesens. (Wenn ein gottgleiches Wesen ψ hat, dann ist ψ positiv — sonst wäre die Negation von ψ positiv, und das gottgleiche Wesen würde sie ebenfalls instanziieren. Also impliziert Gottgleichheit alles, was das Wesen hat, notwendig.)
• Reflexion. Existiert ein gottgleiches Wesen in irgendeiner Welt, existiert es in jeder. (Es hat notwendige Existenz nach A5; sein Wesen — Gottgleichheit — ist daher notwendig instanziiert.)
• T3. Notwendig existiert ein gottgleiches Wesen: □ ∃x GodLike(x). (C liefert eine mögliche Instanz; die Reflexion hebt sie zur Notwendigkeit.)

Die gesamte Herleitung sieht in Lean, gekürzt, so aus:

theorem T3_necessarily_God
    (hA1 : A1 Positive) (hA2 : A2 Positive)
    (hA3 : A3 Positive) (hA5 : A5 Positive) :
    □ (fun w => ∃ x, GodLike Positive w x) := ...

Beachte, was nicht in diesem Typ steht: keine ambienten axiom-Deklarationen, keine versteckten Lemmata. Die Axiome stehen als Hypothesen im Typ des Theorems. Das Repo sagt das explizit — es nennt es die Ehrlichkeitsklausel, und sie ist das Philosophischste am ganzen Code.

Was die Maschine bewiesen hat — und was nicht

Lean verifiziert eine Implikation: A1 ∧ A2 ∧ A3 ∧ A5 ⊢ □∃x GodLike(x), unter dieser Kodierung der Modalität. Das ist alles, was sie verifiziert. Ob die Axiome wahr sind — ob „Positivität" ein kohärenter Begriff ist, ob sich das Gute so dichotom über Eigenschaften legt, wie A1 es verlangt, ob notwendige Existenz eine positive Eigenschaft ist und kein geschmuggelte Konklusion — ist keine Frage mit einem Typ. Der Beweisassistent prüft Gültigkeit; die Soundness ist unser Problem.

Das verdient Nachdenken, denn es kehrt die übliche Sorge über Maschinen in der Philosophie um. Die Maschine räumt die Debatte nicht weg; sie leitet sie dorthin zurück, wo sie immer schon stattfand: zu den Prämissen. Gödels eigene Notizen, durch einen Theorembeweiser von Benzmüller und Woltzenlogel Paleo geschickt, erwiesen sich als inkonsistent — die Maschine fand den Fehler in den Axiomen, nicht in der Logik. Scotts A5 (notwendige Existenz ist positiv) ist genau die Reparatur, die die Konsistenz wiederherstellt. Die Formalisierung ist in diesem Sinne das schärfste Instrument, das je auf dieses Argument gerichtet wurde: Sie sagt uns nicht, was wir glauben sollen; sie sagt uns exakt, wozu wir uns verpflichten würden.

Der Preis des Beweises

Und die Verpflichtungen sind gewichtig. Sobel zeigte 1987, dass Scotts Axiome nicht bloß □∃x GodLike(x) beweisen — sie beweisen den modalen Kollaps: φ → □φ, für jede Aussage φ. Alles Wahre ist notwendig wahr. Es gibt keine andere Möglichkeit, wie die Welt hätte sein können. Das Repo leitet dies in seiner dünnen Kodierung erneut her und zieht die naheliegende Konsequenz: Kontingenz ist unmöglich, und mit ihr jede Willensfreiheits-Lektüre von „hätte anders handeln können". Man bekommt den notwendigen Gott und bezahlt mit jeder kontingenten Tatsache im Universum.

Die Auswege der Literatur sind ebenfalls kartiert. Andersons Reparatur von 1990 (halbiert A1, definiert gottgleich als notwendiges Haben genau der positiven Eigenschaften) hält T3 und blockiert zugleich den Kollaps — das Repo prüft das nach. Und die Frame-Analyse ist ernüchternd für jeden, der dachte, „S5" leiste bescheidene Arbeit: Der kritische Schritt von Möglichkeit zu Notwendigkeit braucht die Symmetrie der Relation (Gegenmodell B zeigt eine S4-Kette, in der die Axiome gelten und Gott nur in der Senke existiert — ◇∃G wahr, □∃G falsch), und die globale Behauptung, Gott existiere in jeder Welt, braucht einen universellen Frame, in dem jede Welt jede andere sieht (Gegenmodell A: zwei isolierte S5-Cluster, Gott in einem). Das Theorem ist in der Kodierung wahr, weil die Kodierung großzügig ist. Jede tragende Wand ist jetzt beschriftet — und genau das ist der Sinn einer guten Formalisierung.

Kants Rache

Nun der Mann, der dieser Party 240 Jahre zuvorkam. Kants Angriff auf den ontologischen Beweis, in der ersten Kritik, läuft auf einen Satz hinaus: Existenz ist kein reales Prädikat. Hundert echte Taler enthalten kein Körnchen mehr als hundert mögliche Taler; Existenz zu einem Begriff hinzuzufügen, bereichert ihn nicht, denn Existenzaussagen sind nicht analytisch — man kann etwas nicht ins Sein definieren. Was auch immer gedacht wird, wird als möglich gedacht; es auch als notwendig zu behaupten, heißt, eine Synthese zu schmuggeln, die keine Definition liefert.

Sieh A5 noch einmal an: Notwendige Existenz ist eine positive Eigenschaft. Sieh D3 an: Ein Wesen mit der positiven Eigenschaft notwendiger Existenz hat jedes seiner Wesen (Essences) notwendig instanziiert. Die gesamte Maschinerie aus T2 und Reflexion existiert, um eine Definition in Existenz zu verwandeln. Kant wäre nicht überrascht gewesen, dass es fünf Axiome und einen Beweisassistenten braucht, um den Schmuggel sauber über die Bühne zu bringen; er hätte nur darauf hingewiesen, dass der Schmuggel nun sehr gut dokumentiert ist. Die Ehrlichkeitsklausel des Repos — Lean verifiziert eine Implikation; die Axiome sind Annahmen — ist die erste Kritik in vierzig Zeilen Code. Sie führt geradewegs zur ersten der Kantschen Fragen: Was kann ich wissen? Du kannst exakt wissen, was aus dem folgt, was du angenommen hast. Ob du es annehmen darfst, ist kein Theorem.

Und es gibt ein Kantisches Nachspiel im Kollapsresultat. Im Reich der Zwecke legislieren vernünftige Wesen; Gesetzgebung setzt voraus, dass die Dinge auch anders sein könnten — dass es etwas gibt, worüber man Gesetze gibt. Eine Welt, in der φ → □φ gilt, hat keinen Raum für einen Willen, göttlich oder menschlich. Gödels Beweis kauft Notwendigkeit zum Preis des Raums, in dem Autonomie, Pflicht und Hoffnung operieren. Das Argument, das das höchste Wesen sichern sollte, sichert nebenbei den Tod von allem, was Kant uns zu Menschen machte.

Wozu ein Beweisassistent gut ist

Ich halte Formalisierungen wie diese neben meinem Kant, aus demselben Grund, aus dem ich einen Compiler neben meine Prosa stelle. Nicht weil die Maschine die Frage entscheidet — tut sie nie —, sondern weil sie das Argument am Driften hindert. Nach vier Wochen in diesem Repo kannst du mit geradem Gesicht nicht mehr sagen „Gödel hat Gottes Existenz bewiesen", und du kannst auch nicht sagen „der ontologische Beweis ist Wortspiel". Du kannst etwas Besseres sagen: Hier sind fünf Annahmen; hier ist die exakte Kette von ihnen zu □∃x GodLike(x); hier bricht sie in schwächeren Logiken; hier ist ihr Preis; und hier ist der Schritt, den Kant für illegitim erklärte — located bis auf die Zeile. Präzision über Prämissen ist nicht das Ende der Philosophie. Sie ist die Disziplin, die die verbleibenden Meinungsverschiedenheiten ehrlich macht.

Die Maschine hat jeden Schritt geprüft. Welche Schritte du gelten lässt, bleibt dein.

Wenn du tiefer einsteigen willst: Die NOTES.md des Repos ist ein vorbildliches Forschungsnotebook; die Arbeiten von Benzmüller und Woltzenlogel Paleo sind die Standardreferenzen zur Mechanisierung; Sobels Logic and Theism ist die klassische Kritik; Fittings Types, Tableaus, and Gödel's God die vollständige logische Behandlung. Wie Beweis- und Audit-Pflichten anderswo in meiner Arbeit auftauchen, zeigen die Lean-Formalisierungsnotizen unter Research.