Gödel's God, Machine-Checked: The Ontological Proof from Leibniz to Lean

An out-of-judgement GPU World field report: the contest premise taken seriously, a Bayesian model, the full Lagos story, and what a frozen frontier reveals about trust, attention and accountability.

One GPU Per Person: Notes from a World That Didn't Happen

An out-of-judgement GPU World field report: the contest premise taken seriously, a Bayesian model, the full Lagos story, and what a frozen frontier reveals about trust, attention and accountability.

Part of the Philosophy section — a companion to Kant's Questions in the Age of AI and A Short History of Philosophy. The Lean formalization discussed here: github.com/drewarrowood/godel-ontological.

In 1970, convinced he was dying, Kurt Gödel allowed a trusted friend to copy out a proof he had carried around since the 1940s. He had hesitated for three decades for a characteristic reason: he feared people would think that he actually believed in God. The proof was ontological — a modern, modal reconstruction of the argument for God's existence from Anselm of Canterbury and Leibniz, boiled down to five axioms and a short chain of theorems. Gödel, the greatest logician of the century, had turned the oldest argument in natural theology into something that looks like mathematics: definitions, axioms, lemmas, a conclusion of the form necessarily, there exists a God-like being (□ ∃x GodLike(x)).

The notes circulated, Dana Scott repaired them, Christ Benzmüller and Bruno Woltzenlogel Paleo mechanized them in Isabelle/HOL — automated theorem provers found that Gödel's unrepaired axioms were outright inconsistent, and verified Scott's variant. And now there is a small, honest Lean 4 formalization that rebuilds the whole chain from scratch: github.com/drewarrowood/godel-ontological. Five axioms in, one boxed existence claim out, lake build green, zero sorry. It is a lovely artifact — and reading it is a lesson in what proofs, machines, and philosophy can and cannot do for each other.

I want to walk the chain, because the chain is the argument, and then ask the question the repo itself asks in its honesty clause: what exactly has been proved?

The lineage in one line each

• Anselm (1078): God is "that than which nothing greater can be conceived." Existing in reality is greater than existing merely in the understanding — so the greatest conceivable being must exist.
• Descartes (1641): Existence is a perfection. I cannot conceive of God as existing-but-might-not, any more than a mountain without a valley.
• Leibniz (c. 1700): The gap is possibility. If the most perfect being is possible, then — perfections being unlimited — it exists necessarily. He never finished the possibility proof.
• Gödel (c. 1941): Modalize it. Positivity instead of perfection, S5 possible worlds instead of understanding-versus-reality, and Leibniz's missing step falls out as a theorem.

Each link added precision and, with it, fragility. That is worth keeping in mind for everything that follows.

The axioms, the definitions, the chain

The Scott set works with a meta-predicate Positive on properties, read rigidly across worlds: a property is positive iff its negation is not positive (A1); whatever a positive property necessarily entails is positive (A2); being God-like is positive (A3); positive properties are necessarily positive (A4 — in the Lean encoding this comes for free because positivity is not world-indexed); and necessary existence is positive (A5). Three definitions do the rest: God-like means having every positive property (D1), an essence of x is a property x has that necessarily entails everything x has (D2), and necessary existence means every essence is necessarily exemplified (D3).

From these, five steps:

• T1. Any positive property is possibly exemplified. (Otherwise it is nowhere exemplified, hence entails the impossible, hence its negation collapses positivity itself — contradiction.)
• C. Possibly, a God-like being exists. (God-likeness is positive by A3, possible by T1.)
• T2. God-likeness is the essence of any God-like being. (If a God-like being has ψ, then ψ is positive — otherwise its negation would be, and the God-like being would instantiate it too. So God-likeness entails everything the being has, necessarily.)
• Reflection. If a God-like being exists at any world, it exists at every world. (It has necessary existence by A5; its essence — God-likeness — is therefore necessarily exemplified.)
• T3. Necessarily, there exists a God-like being: □ ∃x GodLike(x). (C gives a possible instance; reflection promotes it to necessity.)

The whole derivation, abbreviated, looks like this in Lean:

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

Note what is not in that type: no ambient axiom declarations, no hidden lemmas. The axioms sit in the theorem's type as hypotheses. The repo is explicit about this — it calls it the honesty clause, and it is the single most philosophical thing about the code.

What the machine proved — and what it did not

Lean verifies an implication: A1 ∧ A2 ∧ A3 ∧ A5 ⊢ □∃x GodLike(x), under this encoding of modality. That is all it verifies. Whether the axioms are true — whether "positivity" is a coherent notion, whether goodness carves properties up dichotomously the way A1 demands, whether necessary existence is a positive property rather than a smuggled conclusion — is not a question with a type. The proof assistant checks validity; soundness is our problem.

This is worth savoring, because it inverts the usual anxiety about machines in philosophy. The machine does not bulldoze the debate; it reroutes it to the only place it ever really lived: the premises. Gödel's own notes, run through a theorem prover by Benzmüller and Woltzenlogel Paleo, turned out inconsistent — the machine found the flaw in the axioms, not in the logic. Scott's A5 (necessary existence is positive) is precisely the repair that restores consistency. The formalization is, in this sense, the sharpest instrument anyone has ever pointed at this argument: it does not tell us what to believe, it tells us exactly what we would be committing to.

The price of the proof

And the commitments are steep. Sobel observed in 1987 that Scott's axioms do not merely prove □∃x GodLike(x) — they prove modal collapse: φ → □φ, for every proposition φ. Anything true is necessarily true. There are no other ways the world could have been. The repo re-derives this in its thin encoding and draws the obvious consequence: contingency is impossible, and with it any free-will reading of "could have done otherwise." You get necessary God, and you pay with every contingent fact in the universe.

The literature's escape hatches are mapped too. Anderson's 1990 repair (halve A1, redefine God-like as necessarily having exactly the positive properties) keeps T3 while blocking the collapse — the repo checks this. And the frame analysis is sobering for anyone who thought "S5" was doing modest work: the critical step from possibility to necessity needs symmetry of accessibility (countermodel B shows an S4 chain where the axioms hold and God exists at the sink world only — ◇∃G is true, □∃G false), and the global claim that God exists at every world needs a universal frame where every world sees every other (countermodel A: two isolated S5 clusters, God in one). The theorem is true in the encoding because the encoding is generous. Every load-bearing wall is now labeled, which is exactly what a good formalization is for.

Kant's revenge

Now bring in the man who ruined this party 240 years early. Kant's attack on the ontological argument, in the first Critique, comes down to one sentence: existence is not a real predicate. A hundred real thalers contain not a grain more than a hundred possible thalers; adding existence to a concept does not enrich it, because existential claims are not analytic — you cannot define something into being. Whatever is conceived is conceived as possible; to also claim it as necessary is to have smuggled in a synthesis that no definition supplies.

Look at A5 again: necessary existence is a positive property. Look at D3: a being with the positive property of necessary existence has every essence necessarily exemplified. The entire machinery of T2 and reflection exists to convert a definition into existence. Kant would not have been surprised that it takes five axioms and a proof assistant to pull off the smuggle cleanly; he would simply point out that the smuggle is now very well documented. The repo's honesty clause — Lean verifies an implication; the axioms are assumptions — is the first Critique in forty lines of code. It connects straight to the first of Kant's questions: what can I know? You can know exactly what follows from what you have assumed. Whether you may assume it is not a theorem.

And there is a Kantian postscript in the collapse result. In the kingdom of ends, rational beings legislate; legislation presupposes that things could be otherwise — that there is something to legislate about. A world where φ → □φ has no room for a will, divine or human. Gödel's proof buys necessity at the price of the very space in which autonomy, duty, and hope operate. The argument that was meant to secure the highest being secures, along the way, the death of everything Kant thought made us one.

What a proof assistant is for

I keep formalizations like this one next to my Kant for the same reason I keep a compiler next to my prose. Not because the machine settles the question — it never does — but because it stops the argument from drifting. After four weeks in this repo you cannot say "Gödel proved God's existence" with a straight face, and you cannot say "the ontological argument is wordplay" either. You can say something better: here are five assumptions; here is the exact chain from them to □∃x GodLike(x); here is where it breaks in weaker logics; here is what it costs; and here is the step Kant said was illegitimate, located to the line. Precision about premises is not the end of philosophy. It is the discipline that makes the remaining disagreements honest.

The machine checked every step. Which steps to grant is still yours.

If you want to go deeper: the repo's NOTES.md is a model research notebook; Benzmüller and Woltzenlogel Paleo's papers are the standard mechanization references; Sobel's Logic and Theism is the classic critique; Fitting's Types, Tableaus, and Gödel's God is the full logical treatment. For how duties of proof and audit show up elsewhere in my work, see the Lean formalization notes in Research.