Gödel's ontological argument

Gödel's ontological argument is a formal modal-logic proof for the existence of God developed by the logician Kurt Gödel in his private notebooks during the 1940s and shown to the philosopher Dana Scott in February 1970. The proof was first published in 1987 by Jordan Howard Sobel and again in 1995 in the third volume of Gödel's Collected Works, edited by Solomon Feferman and others.^{1, 2, 4} Gödel's argument stands in the tradition of the ontological proofs of Anselm of Canterbury, René Descartes, and especially Gottfried Wilhelm Leibniz, but differs from earlier versions in being expressed in the rigorous formalism of higher-order modal logic, with the entire derivation reduced to five axioms, three definitions, and a small number of theorems whose validity can be mechanically checked.^{1, 10}

The argument's reception has been shaped by two developments. First, Sobel demonstrated in 1987 that Gödel's axiom system entails modal collapse — the conclusion that every true proposition is necessarily true — a consequence widely treated as unacceptable for any system of metaphysical modality, since it eliminates contingency and thereby any meaningful distinction between necessary and contingent truths. Second, beginning in 2013, Christoph Benzmüller and Bruno Woltzenlogel Paleo formalized the proof in higher-order theorem provers including Coq, Isabelle, LEO-II, and Satallax, mechanically confirming both that Gödel's premises validly entail the existence of a God-like being and that they entail modal collapse, and detecting a previously unnoticed inconsistency in Gödel's original 1970 axiomatization that had been silently corrected in Scott's 1972 variant.^{3, 7, 8} The result is a family of related ontological arguments — Gödel's, Scott's, Anderson's, Hájek's, Fitting's — whose formal validity is no longer at issue, leaving the philosophical dispute concentrated on the truth and intelligibility of their axioms.

Historical development

Gödel's interest in the ontological argument originated in his lifelong study of Leibniz, whose work he regarded with particular admiration. The earliest drafts of an ontological proof in Gödel's Nachlass are dated to about 1941, and the manuscript material in Collected Works includes several distinct versions developed between 1940 and 1970.^{1, 13} The proof Gödel eventually circulated has its direct ancestor in Leibniz's 1676 manuscript Quod ens perfectissimum existit ("That a most perfect being exists"), in which Leibniz attempted to repair what he saw as a gap in Descartes's ontological argument by demonstrating that the concept of a perfect being is not self-contradictory. Leibniz argued that the divine perfections are "simple, positive, and absolute" qualities that cannot stand in logical conflict with one another, so the concept of a being possessing all of them is internally coherent and the conditional ontological argument can therefore be discharged.^{2, 12}

Gödel did not publicly discuss the proof during his lifetime. His colleague Oskar Morgenstern recorded in a diary entry from August 1970 that Gödel feared his work on the argument would be misunderstood — that "others might think that he actually believes in God, whereas he is only engaged in a logical investigation."^{1, 2} In February 1970, however, while Gödel believed himself to be near death, he allowed Dana Scott to copy out one of the derivations from his notebooks. Scott circulated the proof privately among logicians and produced his own slightly modified version, which became the form in which most subsequent scholars first encountered the argument.^{1, 10}

The proof remained unpublished for nearly two decades after Scott received it. Sobel was the first to print Gödel's text in his 1987 paper "Gödel's Ontological Proof," which appeared in a Festschrift for Richard Cartwright, and the proof received its definitive scholarly edition in 1995 when Robert Merrihew Adams's introductory note and the relevant manuscript material were published in Collected Works, Volume III.^{1, 2, 4} Adams's introduction, occupying pages 388 to 402 of that volume, provides the principal scholarly account of the proof's textual history and its relationship to Leibnizian metaphysics.²

The Leibnizian background

To understand what Gödel's proof was attempting to accomplish, it is necessary to see what Leibniz had already done with the ontological argument and what Leibniz left unfinished. Descartes, in the Fifth Meditation, had argued that existence is a perfection and therefore belongs to the essence of a perfect being in the way that having three angles equal to two right angles belongs to the essence of a triangle. Leibniz accepted the structural form of Descartes's argument but objected that Descartes had assumed without proof that the concept of a perfect being is even logically coherent. If the divine perfections are mutually incompatible — if, for instance, omniscience and omnipotence somehow contradict one another — then the concept of a being possessing all perfections is empty, and any conclusion derived from it is suspect.^{2, 12}

Leibniz's solution was to argue that a perfection is a "simple, positive, and absolute" quality — a quality that contains no negation and cannot be analyzed into more basic constituents. Two such qualities cannot contradict one another, Leibniz reasoned, because contradiction requires that one quality affirm what another denies, and a quality that contains no negation has nothing to deny. Therefore the perfections are mutually compatible, the concept of a perfect being is consistent, and the ontological argument can proceed from a verified antecedent rather than an assumed one.^{2, 12}

Robert Adams, in his 1994 book Leibniz: Determinist, Theist, Idealist, has shown that Leibniz's reasoning rests on assumptions about logical analysis that became untenable in the wake of Frege and Russell. The notion that all genuine properties decompose into "simple, positive, and absolute" constituents is itself a substantive metaphysical thesis, and the inference from the absence of negation to the absence of contradiction is not formally valid in modern logic.¹² What Gödel's proof provides is a way to extract Leibniz's strategy from these untenable assumptions and re-express it in a framework — higher-order modal logic — where the relevant claims can be stated precisely and their consequences mechanically checked. The "positive properties" of Gödel's axioms occupy the structural role of Leibniz's perfections, but the framework is no longer that of seventeenth-century logic.^{1, 2}

The formal argument

Gödel's proof is presented in higher-order modal logic, in which one can quantify not only over individuals but also over properties. The single primitive notion is that of a positive property, expressed by a predicate P applied to properties. The proof's axioms, definitions, and theorems can be stated as follows, in the formulation that appears in Collected Works:^{1, 10}

Definition 1. x is God-like if and only if x possesses every positive property as an essential property.

Definition 2. A property φ is an essence of x if and only if x has φ and every property x has follows necessarily from φ.

Definition 3. x necessarily exists if and only if every essence of x is necessarily exemplified.

Axiom 1. If a property is positive and entails another property, then that other property is also positive.

Axiom 2. A property is positive if and only if its negation is not positive.

Axiom 3. The property of being God-like is positive.

Axiom 4. If a property is positive, it is necessarily positive.

Axiom 5. Necessary existence is a positive property.

Theorem 1. If a property is positive, then it is possible that something has it.

Theorem 2. It is possible that a God-like being exists.

Theorem 3. If something is God-like, then being God-like is its essence.

Theorem 4 (Conclusion). Necessarily, a God-like being exists.

The derivation moves through three structural steps. From Axioms 1 and 2 it follows (Theorem 1) that no positive property is necessarily uninstantiated, since if a positive property were necessarily uninstantiated it would entail every property (including its own negation), and by Axiom 1 the negation of any positive property would itself be positive, contradicting Axiom 2. From Axiom 3 and Theorem 1 it follows (Theorem 2) that the property of being God-like is possibly instantiated. From Definitions 1 and 2 together with Axioms 3 and 4 it follows (Theorem 3) that being God-like is the essence of any being that has it. From Definition 3, Axiom 5, Theorem 2, and Theorem 3, together with the S5 modal principle that possibly necessary entails necessary, the conclusion (Theorem 4) follows: it is necessarily the case that a God-like being exists.^{1, 7, 10}

The formal validity of this derivation in S5 modal logic with the appropriate higher-order machinery has been mechanically verified using automated theorem provers, including LEO-II, Satallax, the Coq proof assistant, and Isabelle.^{7, 8} Whatever objections may be raised against the proof, they cannot be objections to the inferential moves — those are sound. The dispute is entirely about the axioms.

The notion of positive properties

The pivot of Gödel's proof is the predicate "positive" applied to properties. Gödel offered no explicit definition of positivity in his manuscript notes; he treated it as a primitive notion with two sketched glosses. In one note, Gödel wrote that positive may be understood "in the moral aesthetic sense (independently of the accidental structure of the world)" or as "pure attribution" — that is, as containing no defect, limitation, or privation.^{1, 2} Both glosses point in the same direction: a positive property is one whose possession enhances rather than limits the being that possesses it, and which can be ascribed without implying any negation or imperfection.

This characterization echoes Leibniz's notion of a perfection as a "simple, positive, and absolute" quality, but Gödel's framework is more flexible: it does not require positive properties to be simple or unanalyzable, only that they satisfy the closure conditions imposed by the axioms.^{2, 12} Axioms 1 and 2 together impose a structure on positivity that resembles an ultrafilter on the lattice of properties: positive properties are closed under entailment (Axiom 1) and exactly one of any property and its negation is positive (Axiom 2). These axioms are mathematically well-behaved, but they leave open the substantive question of which properties are positive — and on this question Gödel's notes provide little guidance beyond Axioms 3 and 5, which assert the positivity of being God-like and of necessary existence respectively.

Graham Oppy, in the Stanford Encyclopedia of Philosophy entry on ontological arguments, has emphasized that the persuasiveness of Gödel's proof depends entirely on whether one accepts that the properties typically associated with God — omnipotence, omniscience, perfect goodness — are in fact positive in the technical sense the axioms require. A non-theist who denies the coherence of these properties will simply deny that they satisfy the conditions for positivity, and the proof will fail to compel.¹⁰ Alexander Pruss has identified at least five distinct ways of explicating positivity that have been proposed in the literature — comparison-based, excellence-based, anti-negativity, Leibnizian, and "no limitations" accounts — each of which would yield a slightly different proof, and none of which has commanded general assent.¹⁰

Essence and necessary existence

Definitions 2 and 3 introduce the technical notions on which Theorems 3 and 4 depend. A property φ is the essence of a being x if x has φ and if every property x has follows necessarily from φ. This is a strong notion: an essence is not merely a defining feature but a property from which all of x's other properties can be derived. Gödel's Definition 2 differs from the more familiar Aristotelian notion of essence — which picks out the fundamental kind to which a being belongs — and is closer to the Leibnizian notion of a complete individual concept, in which every property of an individual is contained.^{1, 2, 12}

Necessary existence, in Definition 3, is then defined as a property of beings whose essences are necessarily exemplified. This is a higher-order construction: a being necessarily exists not merely if it exists in every possible world, but if every property that is its essence is instantiated in every possible world. Gödel's choice of this definition is motivated by the structural needs of the proof. Axiom 5 declares necessary existence to be a positive property, which (combined with Definition 1) means that any God-like being possesses necessary existence as one of its essential properties; the proof then uses Definition 3 to conclude that the essence of such a being is necessarily exemplified, and therefore that the being necessarily exists.^{1, 10}

The interaction between these definitions and the modal logic of S5 is what generates the proof's striking conclusion. In S5, what is possibly necessary is necessary; combined with Theorem 2 (the possible existence of a God-like being) and the chain of definitions linking God-likeness to necessary existence, this yields Theorem 4. The proof's elegance lies in how compactly it packages the modal inference, but this same compactness is what creates the modal collapse problem analyzed in the next section.

Sobel's modal collapse objection

In his 1987 paper "Gödel's Ontological Proof," Jordan Howard Sobel demonstrated that Gödel's axiom system entails not only the existence of a God-like being but also the much stronger and far more troubling thesis that every true proposition is necessarily true. This result, known as modal collapse, can be stated formally as the schema p → □p: if p is true, then p is necessarily true.^{3, 4}

Sobel's derivation of modal collapse exploits the interaction of Definition 2 (essence) and Axiom 5 (necessary existence is positive). If a God-like being has every positive property as an essential property, and if essence requires that every property the being has follows necessarily from its essence, then for any contingent property q that the God-like being happens to possess, it follows that q is necessarily entailed by being God-like — and since the God-like being necessarily exists, q obtains necessarily as well. Generalizing, every property that holds in the actual world holds in every possible world, and the distinction between contingent and necessary truths collapses.^{3, 4, 15}

The philosophical cost of modal collapse is severe. If every truth is necessarily true, there are no contingent facts: the entire history of the universe down to the smallest detail unfolds with the same logical necessity as the truths of arithmetic. Free will, on standard libertarian conceptions, becomes impossible, since libertarian freedom requires that an agent could have done otherwise — and if every truth is necessarily true, no agent could have done otherwise about anything. The doctrine of divine creation also becomes problematic, since on classical theism God's act of creating this world rather than some other is supposed to be free, and modal collapse forecloses any such freedom.^{3, 4, 15}

The 2014 computer-verified analysis by Benzmüller and Woltzenlogel Paleo, presented at the European Conference on Artificial Intelligence (ECAI 2014), independently confirmed Sobel's modal collapse result by deriving it mechanically from Gödel's axioms using the higher-order theorem prover LEO-II. Their formalization established that the axioms are consistent (so the conclusion does follow from them rather than from a hidden contradiction) but that they entail modal collapse as a theorem.^{7, 8} Sobel's argument has been subjected to detailed scrutiny by Srećko Kovač and others, and while alternative derivations of modal collapse have been proposed, the core result — that Gödel's axiom system as he wrote it entails modal collapse — is now firmly established.¹⁵

Sobel's derivation of modal collapse from Gödel's axioms^{3, 15}

Anderson's emendation and the Hájek alternatives

The standard response to Sobel's modal collapse result has been to modify Gödel's axioms in ways that block the collapse derivation while preserving the conclusion that a God-like being necessarily exists. The most influential such modification is due to C. Anthony Anderson, in his 1990 paper "Some Emendations of Gödel's Ontological Proof," published in the journal Faith and Philosophy.⁵

Anderson identified Definition 1 — which states that a God-like being possesses every positive property as an essential property — as the locus of the modal collapse problem. By requiring that every positive property be possessed essentially, Definition 1 forces every property of the God-like being to follow from its essence in a way that propagates through the modal logic to yield collapse. Anderson's revised definition states instead that a being is God-like if and only if it has as an essential property all and only the positive properties; in other words, the God-like being's essential properties are exactly the positive properties, no more and no less. This revision blocks the inference from Sobel's step 4 to step 5 in the table above, because the property "being such that p" for an arbitrary contingent p need not be among the God-like being's essential properties.^{5, 14}

Anderson's 1990 system has been extensively analyzed. Computer-verified work by Benzmüller, Leon Weber, and Woltzenlogel Paleo, published in Logica Universalis in 2017, formally examined the controversy between Anderson and Petr Hájek over whether Anderson's emendation is the most economical fix. Their mechanized analysis confirmed that Anderson's system blocks modal collapse and still entails the necessary existence of a God-like being, but also revealed subtle interactions between the modified definition and the remaining axioms that constrain how the system can be further extended.¹⁴ Anderson and Michael Gettings, in a 1996 follow-up paper, raised concerns about the philosophical motivation for the revised definition and explored whether it could be justified independently of the desire to avoid modal collapse.¹¹

Petr Hájek, in his 2002 paper "A New Small Emendation of Gödel's Ontological Proof," published in Studia Logica, proposed a different and more conservative modification. Hájek's strategy is to weaken Axiom 4 (the claim that positive properties are necessarily positive) rather than to revise Definition 1, on the grounds that Axiom 4 is doing the heavy lifting in propagating modal collapse and is also the axiom for which Gödel offered the least independent justification.⁹ Hájek showed that with Axiom 4 weakened in a specific way, the existence of a God-like being can still be derived but the modal collapse inference is blocked. The choice between Anderson's and Hájek's emendations remains an open question in the literature, with each having its defenders.^{9, 14}

Computer verification by Benzmüller and Woltzenlogel Paleo

The application of higher-order automated theorem provers to Gödel's ontological proof, beginning in 2013, transformed the scholarly study of the argument. Christoph Benzmüller and Bruno Woltzenlogel Paleo's project — first announced in the 2013 arXiv paper "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence" and presented in expanded form at ECAI 2014 — encoded the proof in higher-order modal logic and ran it through multiple proof assistants and theorem provers.^{7, 8}

The technical setup involved several layers. Higher-order modal logic was embedded in the simply-typed lambda calculus underlying the Coq and Isabelle proof assistants, allowing modal formulas to be represented and manipulated as ordinary higher-order expressions. The theorem provers LEO-II and Satallax were then applied to derive each of Gödel's theorems from his axioms automatically. The model-finder Nitpick was used to verify the consistency of the axiom set by searching for finite models in which all axioms hold simultaneously. A step-by-step natural-deduction formalization in Coq provided a human-readable verification, and a more automated formalization in Isabelle used the Sledgehammer and Metis tactics to derive the theorems with minimal human intervention.^{7, 8}

Three results emerged from this work. First, the conclusion of Gödel's proof (Theorem 4: necessarily, a God-like being exists) was mechanically derived from the axioms in every system tested. Second, modal collapse was independently rederived, confirming Sobel's 1987 result with full formal rigor. Third, LEO-II detected that Gödel's original 1970 axiomatization is inconsistent in modal logics with reflexive accessibility relations, an inconsistency that had been silently corrected by Dana Scott in the variant Scott copied from Gödel's notebooks. The Scott variant, which is what most commentators had been working with since 1970, is consistent (Nitpick finds models for it) and yields Theorem 4 without contradiction; Gödel's original notation, when reconstructed precisely, does not.^{7, 8}

The discovery of the Gödel-versus-Scott discrepancy is an instance of computer-aided philosophy uncovering a technical fact about a famous historical argument that had escaped human readers for over forty years. It also demonstrated that the modal collapse problem is not an artifact of any particular reconstruction but follows from any of the consistent versions of the proof in their original form.^{7, 8, 14}

Higher-order theorem provers used in Benzmüller-Paleo verification^{7, 8}

Fitting's reformulation in intensional type theory

Melvin Fitting's 2002 monograph Types, Tableaus, and Gödel's God, published in the Trends in Logic series, presents what is perhaps the most thorough single treatment of Gödel's proof from the perspective of formal logic. Fitting embeds the proof in a higher-order modal type theory derived from the Montague-Gallin tradition of intensional logic, using semantic tableaux as the proof procedure rather than natural deduction or sequent calculus.⁶

One of Fitting's central contributions is to show that the modal collapse problem depends critically on whether properties are understood intensionally or extensionally. On an extensional reading, properties are identified with the sets of individuals that have them, and two properties that pick out the same individuals across possible worlds are the same property. On an intensional reading, properties are finer-grained: they include something like a mode of presentation that distinguishes properties even when they apply to the same individuals. Fitting argues that under a properly intensional treatment, the property abstraction step that powers Sobel's modal collapse derivation is no longer freely available, because the construction of the property "being such that p" requires extensional collapse.⁶

Fitting's analysis suggests that the modal collapse objection, while formally correct against the system Gödel actually wrote down, may not generalize to all reasonable formalizations of the underlying argument. If positive properties are intensional entities, the abstraction operation that takes an arbitrary true proposition p and converts it into a property "being such that p" is restricted, and the chain of reasoning that yields modal collapse breaks at the abstraction step rather than at any of the explicit axioms.⁶ Whether this defense is ultimately successful depends on whether one accepts the intensional treatment of properties as philosophically motivated or as an ad hoc fix to avoid an unwanted conclusion — a question Fitting himself treats as open.

The question of positive properties

Even if every modal-collapse worry can be resolved by Anderson's, Hájek's, or Fitting's modifications, the philosophical force of Gödel's proof still depends entirely on whether one accepts that the property of being God-like is positive (Axiom 3) and that necessary existence is positive (Axiom 5). These two axioms are not theorems of higher-order modal logic; they are substantive metaphysical claims, and the proof's persuasive power can be no greater than their joint plausibility.¹⁰

Axiom 3 — that being God-like is positive — is the more philosophically loaded of the two. The God-like being is defined as one possessing all positive properties as essential properties; whether this definition is itself coherent depends on whether the totality of positive properties is internally consistent. A non-theist might argue, following Leibnizian lines, that omnipotence and omniscience and perfect goodness are not jointly compatible — that, for instance, the property of being able to bring about evil and the property of being unable to do anything wrong are both candidates for positivity but are mutually exclusive. If the positive properties are not jointly compossible, the property of being God-like is not positive (because it implies a contradiction), and Axiom 3 fails.¹⁰

Axiom 5 — that necessary existence is positive — faces a different objection. Critics in the tradition of Kant's "existence is not a real predicate" worry that necessary existence is not the kind of property that can meaningfully be attributed to a being at all, let alone one that can enhance the being's metaphysical standing. Defenders respond, with Norman Malcolm and Charles Hartshorne, that even if mere existence is not a predicate, necessary existence is genuinely a property — there is a real difference between a being that happens to exist contingently and one that could not have failed to exist — and that this property is naturally regarded as a perfection.^{2, 10}

Graham Oppy has argued that absent some independent, non-question-begging criterion for which properties count as positive, the proof cannot persuade anyone who does not already accept its conclusion. The non-theist will simply deny Axiom 3, and there is no neutral standpoint from which to adjudicate the dispute. Theist and atheist agree on the formal validity of the proof; they disagree on whether one of its key axioms is true; and the proof itself does nothing to settle this disagreement.¹⁰

Contemporary assessment

The contemporary scholarly situation regarding Gödel's ontological argument can be summarized in three observations. First, the formal validity of the proof — and of its main variants — is no longer contested. Higher-order theorem provers have mechanically verified that the conclusion follows from the axioms, and no logician working in the area regards the inferential structure as defective.^{7, 8} Second, the modal collapse objection developed by Sobel in 1987 establishes that Gödel's axioms in their original form entail an unacceptably strong conclusion, but the emendations of Anderson, Hájek, Fitting, and others have produced consistent variants that block modal collapse while preserving the central conclusion that a God-like being necessarily exists.^{3, 5, 9, 14} Third, the philosophical disputes that remain concern the substantive content of the axioms — particularly the meaning and applicability of "positive property" — and these disputes are not resolvable by formal methods alone.¹⁰

The status of Gödel's proof within the broader project of natural theology is comparable to the status of Plantinga's modal ontological argument: both are formally valid in S5 modal logic, both reduce the entire weight of the theistic conclusion to a single contestable premise, and both leave open the question of whether the disputed premise can be defended on grounds independent of the conclusion it is meant to establish. Where the two arguments differ is in their formal apparatus and in the precise location of the disputed premise — for Plantinga, it is the possibility of maximal greatness; for Gödel, it is the positivity of being God-like — but the structural parallel is exact.¹⁰

The historical significance of Gödel's contribution lies less in the proof's persuasive force than in its demonstration that ontological arguments can be given fully formal expression. Anselm's original argument and even Leibniz's more sophisticated version operated at a level of informality that allowed competing interpretations and made it difficult to determine where, exactly, an objection should attach. Gödel's proof closed off this avenue: with the axioms and definitions stated precisely and the inferential rules fixed, every objection must specify whether it targets a particular axiom, a particular definition, or a particular inferential move. The result is that the dialectic surrounding Gödel's proof is unusually focused — much of the recent literature has the character of a technical investigation rather than a traditional philosophical debate — and the questions that remain are correspondingly sharp.^{1, 2, 10}

Whether this sharpness counts as an advance depends on one's expectations for natural theology. To those who hoped that formalization would reveal the proof's conclusion to be either obviously true or obviously false, the result is disappointing: the proof is valid, but its key axioms remain as contested as ever. To those who saw the value of formalization as clarifying rather than settling the dispute, the result is exactly what one should have expected: Gödel's proof has made the ontological argument as precise as it can be made, and the precision has not changed the underlying philosophical question, which is whether the concept of an absolutely perfect being is coherent. Gödel himself, who believed himself to be doing logic rather than theology, would likely have been satisfied with this outcome.^{1, 2}