Kurt Gödel left a formal ontological argument in his 1970 notes: five axioms, three definitions, three theorems. But the axioms and definitions of that original version are inconsistent — a fact nobody noticed until 2013. Here is the argument line by line, what went wrong, and four influential repairs and reformulations.
Imagine possible worlds together with a relation saying which are accessible from which. At a world w, □p means p holds at every world accessible from w; ◇p means at least one. Different conditions on that relation give different modal logics — which is what the “frame” column below records.
Anything a thing can be — tall, kind, prime. The system quantifies over properties in its higher-order domain, and positivity is a predicate of properties, so keep the two levels apart.
The primitive notion. Gödel suggested readings — “positive in the moral–aesthetic sense”, or pure attribution without privation — but never formally defined it. The argument only lays down axioms governing P.
Every truth is a necessary truth: nothing could have been otherwise, and contingency vanishes. Not an axiom — a consequence of Scott's system, and the objection each later variant is built to escape.
The Lean theorems behind these rows are machine-checked. The “axioms used” and “frame” columns describe what the current Lean derivation consumes — they do not show those assumptions are minimal, and where the literature proves something sharper the row says so. Sources: the Lean files.
| System | Year | Status | Axioms used for key result | Frame (this proof) | Modal collapse | Uniqueness |
|---|
Lean checks conditional mathematics: given the definitions and assumptions encoded here, the stated conclusions follow. It also certifies explicit countermodels and contradictions. Every theorem in this development is a conditional, and #print axioms reports only Lean's own three foundational axioms — Gödel's never appear, because they are hypotheses, not postulates.
Three things Lean does not settle, and which are human work: whether an encoding is historically faithful to its author; whether the hypotheses a particular proof uses are logically minimal; and whether a theorem absent from the development is actually unprovable. Conflating these is the easiest way to get this subject wrong — and an earlier version of this page did, in both directions. Two errors it contained are now corrected below and flagged where they occurred.
So an axiom can stand in three genuinely different relations to a theorem, and the table above reports only the first:
Used by this proof — it is a hypothesis of the statement, enforced by the type. Derivable — it follows from the others, so keeping it is redundant; Anderson's A4 and A5 are the only ones here shown to be. Independent — there is a model of everything else in which it fails. No axiom of Scott's or Fitting's system is claimed independent on this page; showing that needs countermodels, and they have not been built.