The Gödelian proof is a formal mathematical demonstration of God's existence developed by Kurt Gödel between 1941 and 1970, employing modal logic and axiomatic set theory. The argument claims that if we accept certain axioms about positive properties—that they form an ultrafilter closed under entailment and necessity—then we can formally derive that there exists a being possessing all positive properties necessarily. Gödel defines God as the being having all positive properties, proves such a being is possible, then demonstrates through modal logic that if God's existence is possible, it is necessary. The proof's inferential structure moves from axioms about the logical behavior of positive properties through intermediate theorems about essence and necessary existence to conclude that there necessarily exists exactly one being with all positive properties.
Gödel first sketched the proof in notebooks from 1941, refining it through the 1940s, though he never published it during his lifetime, fearing it would be misunderstood as a personal religious confession rather than a logical exercise. The proof was first made public through Dana Scott's 1970 seminar notes and Gödel's conversations with Oskar Morgenstern recorded in the latter's diary. Key expositors include C. Anthony Anderson in "Some Emendations of Gödel's Ontological Proof" (1990), Jordan Howard Sobel in "Logic and Theism" (2004), and Alexander Pruss in "A Gödelian Ontological Argument Improved" (2009). Recent work by Christoph Benzmüller and Bruno Woltzenlogel Paleo has verified the proof's formal validity using automated theorem provers, confirming in "Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers" (2014) that the derivation is logically sound given the axioms.
The strongest objections target the axioms rather than the formal derivation. Sobel demonstrated in "Gödel's Ontological Proof" (1987) that Gödel's axioms entail modal collapse—every true proposition becomes necessarily true—which most philosophers find unacceptable. Critics also challenge the coherence of "positive property," arguing it remains undefined beyond its formal behavior, and question whether existence should count as positive. Anderson responds by weakening the axioms to avoid modal collapse while preserving the proof's conclusion. Pruss defends a notion of positive properties as pure perfections lacking intrinsic limitations. Robert Maydole in "The Ontological Argument" (2012) argues the modal collapse objection assumes S5 modal logic unnecessarily. Benzmüller and Paleo's formal verification sidesteps interpretive issues, showing that whatever positive properties are, if they behave according to Gödel's axioms, the conclusion follows necessarily.
Unlike Anselm's conceptual argument from the idea of "that than which nothing greater can be conceived," Gödel's proof operates through pure formal logic without phenomenological analysis. Where Descartes argues from clear and distinct perception of God's essence and Leibniz focuses on proving the possibility of a perfect being through compossibility of perfections, Gödel axiomatizes the notion of positive properties directly. The Gödelian approach differs from Plantinga's possible worlds formulation by working within higher-order modal logic rather than first-order possible worlds semantics, and unlike Hartshorne's modal argument, makes no appeal to intuitions about worship or religious adequacy.