Gödel's ontological proof is aformal argument by the mathematicianKurt Gödel (1906–1978) for theexistence of God. The argument is in a line of development that goes back toAnselm of Canterbury (1033–1109). St. Anselm'sontological argument, in its most succinct form, is as follows: "God, by definition, is that for which no greater can be conceived. God exists in the understanding. If God exists in the understanding, we could imagine Him to be greater by existing inreality. Therefore, God must exist." A more elaborate version was given byGottfried Leibniz (1646–1716); this is the version that Gödel studied and attempted to clarify with his ontological argument.

The argument usesmodal logic, which deals with statements about what isnecessarily true orpossibly true. From the axioms that a property can only be positive if not-having-it is not positive, and that properties implied by a positive property must all also be themselves positive, it concludes that (since positive propertiesdo not involve contradiction) for any positive property, there is possibly a being that instantiates it. It defines God as the being instantiating all positive properties. After defining what it means for a property to be "the essence" of something (the one property that necessarily implies all its other properties), it concludes that God's instantiation of all positive properties must be the essence of God. After defining a property of "necessary existence" and taking it as an axiom that it is positive, the argument concludes that, since God must have this property, God must exist necessarily.

Gödel left a fourteen-point outline of his philosophical beliefs in his papers.^[1] Points relevant to the ontological proof include:

4. There are other worlds and rational beings of a different and higher kind.

5. The world in which we live is not the only one in which we shall live or have lived.

13. There is a scientific (exact) philosophy and theology, which deals with concepts of the highest abstractness; and this is also most highly fruitful for science.

14. Religions are, for the most part, bad—but religion is not.

The first version of the ontological proof in Gödel's papers is dated "around 1941". Gödel is not known to have told anyone about his work on the proof until 1970, when he thought he was dying. In February, he allowedDana Scott to copy out a version of the proof, which circulated privately. In August 1970, Gödel toldOskar Morgenstern that he was "satisfied" with the proof, but Morgenstern recorded in his diary entry for 29 August 1970, that Gödel would not publish because he was afraid that others might think "that he actually believes in God, whereas he is only engaged in a logical investigation (that is, in showing that such a proof with classical assumptions (completeness, etc.) correspondingly axiomatized, is possible)."^[2] Gödel died January 14, 1978. Another version, slightly different from Scott's, was found in his papers. It was finally published, together with Scott's version, in 1987.^[3]

In letters to his mother, who was not a churchgoer and had raised Kurt and his brother asfreethinkers,^[4] Gödel argued at length for a belief in an afterlife.^[5] He did the same in an interview with a skepticalHao Wang, who said: "I expressed my doubts as G spoke [...] Gödel smiled as he replied to my questions, obviously aware that his answers were not convincing me."^[6] Wang reports that Gödel's wife, Adele, two days after Gödel's death, told Wang that "Gödel, although he did not go to church, was religious and read the Bible in bed every Sunday morning."^[7] In an unmailed answer to a questionnaire, Gödel described his religion as "baptized Lutheran (but not member of any religious congregation). My belief istheistic, notpantheistic, followingLeibniz rather thanSpinoza."^{[note 1]}

The proof^[8][10] usesmodal logic, which distinguishes betweennecessary truths andcontingent truths. In the most common semantics for modal logic, many "possible worlds" are considered. Atruth isnecessary if it is true in all possible worlds. By contrast, if a statement happens to be true in our world, but is false in another world, then it is acontingent truth. A statement that is true in some world (not necessarily our own) is called apossible truth.

Furthermore, the proof useshigher-order (modal) logic because the definition of God employs an explicit quantification over properties.^[11]

First, Gödel axiomatizes the notion of a "positive property":^{[note 2]} for each propertyφ, eitherφ or itsnegation ¬φ must be positive, but not both (axiom 2). If a positive propertyφ implies a propertyψ in each possible world, thenψ is positive, too (axiom 1).^{[note 3]} Gödel then argues that each positive property is "possibly exemplified", i.e. applies at least to some object in some world (theorem 1). Defining an object to be Godlike if it has all positive properties (definition 1),^{[note 4]} and requiring that property to be positive itself (axiom 3),^{[note 5]} Gödel shows that insome possible world a Godlike object exists (theorem 2), called "God" in the following.^{[note 6]} Gödel proceeds to prove that a Godlike object exists inevery possible world.

To this end, he definesessences: ifx is an object in some world, then a propertyφ is said to be an essence ofx ifφ(x) is true in that world and ifφ necessarily entails all other properties thatx has in that world (definition 2). Requiring positive properties being positive in every possible world (axiom 4), Gödel can show that Godlikeness is an essence of a Godlike object (theorem 3). Now,x is said toexist necessarily if, for every essenceφ ofx, there is an elementy with propertyφ in every possible world (definition 3). Axiom 5 requires necessary existence to be a positive property.

Hence, it must follow from Godlikeness. Moreover, Godlikeness is an essence of God, since it entails all positive properties, and any non-positive property is the negation of some positive property, so God cannot have any non-positive properties. Since necessary existence is also a positive property (axiom 5), it must be a property of every Godlike object, as every Godlike object has all the positive properties (definition 1). Since any Godlike object is necessarily existent, it follows that any Godlike object in one world is a Godlike object in all worlds, by the definition of necessary existence. Given the existence of a Godlike object in one world, proven above, we may conclude that there is a Godlike object in every possible world, as required (theorem 4). Besides axiom 1-5 and definition 1–3, a few other axioms from modal logic^{[clarification needed]} were tacitly used in the proof.

From these hypotheses, it is also possible to prove that there is only one God in each world by Leibniz's law, theidentity of indiscernibles: two or more objects are identical (the same) if they have all their properties in common, and so, there would only be one object in each world that possesses property G. Gödel did not attempt to do so however, as he purposely limited his proof to the issue of existence, rather than uniqueness.

The following is the original argument in symbolic notation, then an explanation of each individual symbol used, and then a translation into English of the full argument.

Common notation in symbolic logic:

• ${\displaystyle \phi (x)}$: "Object${\displaystyle x}$ has property${\displaystyle \phi }$" (notation forfirst-order predicates)
• ${\displaystyle \Rightarrow }$: "implies" (material implication)
• ${\displaystyle \mathrm{\forall }x}$: "For every${\displaystyle x}$", or "for all${\displaystyle x}$" (universal quantifier)
• ${\displaystyle \mathrm{\exists }x}$: "There exists an${\displaystyle x}$", or "for some${\displaystyle x}$" (existential quantifier)
• ${\displaystyle \mathrm{\neg }\phi }$: "Thenegation of${\displaystyle \phi }$" (i.e., not${\displaystyle \phi }$)

Modal operators (used inmodal logic):

• ${\displaystyle ◊}$: "It is possible that...", or, "in at least onepossible world, it is true that..." (modal operator for possibility)
• ${\displaystyle ◻}$: "It is necessary that...", or, "in all possible worlds, it is true that..." (modal operator for necessity)

Primitive predicate in this argument:

• ${\displaystyle P(\phi )}$: "Property${\displaystyle \phi }$ is positive" (since it applies to properties, "being positive" is asecond-order property)

Derived predicates (defined in terms of other predicates within the argument):

• ${\displaystyle G(x)}$: "${\displaystyle x}$ is God-like". (Definition 1)
• ${\displaystyle \phi \text{ ess }x}$: "${\displaystyle \phi }$ is an essential property of${\displaystyle x}$" (Definition 2)
• ${\displaystyle E(x)}$: "Object${\displaystyle x}$ exists necessarily" (Definition 3)

Possible-worlds readings of modal terms have been added in parentheses, i.e., "in all possible worlds" for "necessarily" and "in at least one possible world" for "possibly". For completeness, "in the actual world" should be added to all sentences that were saidwithout "necessarily" or "possibly", but this has been skipped since it might make the text difficult to read.

• Axiom 1: If${\displaystyle \phi }$ is a positive property, and if it is necessarily true (true in all possible worlds) that every object with property${\displaystyle \phi }$ also has property${\displaystyle \psi }$, then${\displaystyle \psi }$ is also a positive property.
• Axiom 2: The negation of a property${\displaystyle \phi }$ is positive if, and only if,${\displaystyle \phi }$ is not positive.
• Theorem 1: If a property${\displaystyle \phi }$ is positive, then it is possible that there exists an object${\displaystyle x}$ that has this property (in at least one possible world, there exists an object${\displaystyle x}$ that has this property).
• Definition 1: An object${\displaystyle x}$ is God-like if, and only if,${\displaystyle x}$ has all positive properties.
• Axiom 3: The property of being God-like is itself a positive property.
• Theorem 2: It is possible that there exists a God-like object${\displaystyle x}$ (in at least one possible world, there exists a God-like object${\displaystyle x}$).
• Definition 2: A property${\displaystyle \phi }$ is an essential property of an object${\displaystyle x}$ if,${\displaystyle x}$ has property${\displaystyle \phi }$, and every property${\displaystyle \psi }$ of${\displaystyle x}$ necessarily (in all possible worlds) and generally (for all objects) follows from${\displaystyle \phi }$.
• Axiom 4: If a property${\displaystyle \phi }$ is positive, then it is necessarily positive (positive in all possible worlds).
• Theorem 3: If${\displaystyle x}$ is God-like, then being God-like is an essential property of${\displaystyle x}$.
• Definition 3: An object${\displaystyle x}$ "exists necessarily" if each of its essential properties${\displaystyle \phi }$ applies, in each possible world, to some object${\displaystyle y}$.
• Axiom 5: "Necessary existence" is a positive property.
• Theorem 4: It is necessarily true (true in all possible worlds) that a God-like object exists.

Most criticism of Gödel's proof is aimed at its axioms: as with any proof in any logical system, if the axioms the proof depends on are doubted, then the conclusions can be doubted. It is particularly applicable to Gödel's proof – because it rests on five axioms, some of which are considered questionable. A proof does not necessitate that the conclusion be correct, but rather that by accepting the axioms, the conclusion follows logically.

Many philosophers have called the axioms into question. The first layer of criticism is simply that there are no arguments presented that give reasons why the axioms are true. A second layer is that these particular axioms lead to unwelcome conclusions. This line of thought was argued byJordan Howard Sobel,^[12] showing that if the axioms are accepted, they lead to a "modal collapse" where every statement that is true is necessarily true, i.e. the sets of necessary, of contingent, and of possible truths all coincide (provided there areaccessible worlds at all).^{[note 7]} According toRobert Koons,^[9]: 9 Sobel suggested in a 2005 conference paper^{[citation needed]} that Gödel might have welcomed modal collapse.^[13]

There are suggested amendments to the proof, presented byC. Anthony Anderson,^[14] but argued to be refutable by Anderson and Michael Gettings.^[15] Sobel's proof of modal collapse has been questioned by Koons,^{[9][note 8]} but a counter-defence by Sobel has been given.^{[citation needed]}

Gödel's proof has also been questioned byGraham Oppy,^[16] asking whether many other almost-gods would also be "proven" through Gödel's axioms. This counter-argument has been questioned by Gettings,^[17] who agrees that the axioms might be questioned, but disagrees that Oppy's particular counter-example can be shown from Gödel's axioms.

Religious scholarFr. Robert J. Spitzer accepted Gödel's proof, calling it "an improvement over the Anselmian Ontological Argument (which does not work)."^[18]

There are, however, many more criticisms, most of them focusing on the question of whether these axioms must be rejected to avoid odd conclusions. The broader criticism is that even if the axioms cannot be shown to be false, that does not mean that they are true. Hilbert's famousremark about interchangeability of the primitives' names applies to those in Gödel's ontological axioms ("positive", "god-like", "essence") as well as to those in Hilbert's geometry axioms ("point", "line", "plane"). According toAndré Fuhrmann (2005) it remains to show that the dazzling notion prescribed by traditions and often believed to be essentially mysterious satisfies Gödel's axioms. This is not a mathematical, but a theological task.^{[19]: 364–366} It is this task which decides which religion's god has been proven to exist.

Christoph Benzmüller and Bruno Woltzenlogel-Paleo formalized Gödel's proof to a level that is suitable forautomated theorem proving or at least computational verification viaproof assistants.^[20] The effort made headlines in German newspapers. According to the authors of this effort, they were inspired byMelvin Fitting's book.^[21]

In 2014, they computationally verified Gödel's proof (in theabove version).^{[22]: 97 [note 9]} They also proved that this version's axioms are consistent,^{[note 10]} but imply modal collapse,^{[note 11]} thus confirming Sobel's 1987 argument. In the same paper, they suspected Gödel's original version of the axioms^{[note 12]} to be inconsistent, as they failed to prove their consistency.^{[note 13]}

In 2016, they gave an automated proof that the original version implies${\displaystyle ◊◻\mathrm{\perp }}$, i.e., is inconsistent in every modal logic with a reflexive or symmetricaccessibility relation.^{[24]: 940 lf} Moreover, they gave an argument that this version is inconsistent in every logic at all,^{[note 14]} but failed to duplicate it by automated provers.^{[note 15]} However, they were able to verify Melvin Fitting's reformulation of the argument and guarantee its consistency.^[25]

In 2025, Benzmüller andDana Scott provided the proofs withIsabelle for Scott's variant of Gödel’s modal ontological argument.^[26]

• Philosophy of religion

• Frode Alfson Bjørdal, "Understanding Gödel's Ontological Argument", in T. Childers (ed.),The Logica Yearbook 1998, Prague 1999, 214–217.
• Frode Alfson Bjørdal, "All Properties are Divine, or God Exists", in Logic and Logical Philosophy, Vol. 27 No. 3, 2018, pp. 329–350.
• Bromand, Joachim. "Gödels ontologischer Beweis und andere modallogische Gottesbeweise", in J. Bromand und G. Kreis (Hg.),Gottesbeweise von Anselm bis Gödel, Berlin 2011, 381–491.
• John W. Dawson Jr (1997).Logical Dilemmas: The Life and Work of Kurt Godel. Wellesley, Mass: AK Peters, Ltd.ISBN 1-56881-025-3.
• Melvin Fitting, "Types, Tableaus, and Godel's God" Publisher: Dordrecht Kluwer Academic, 2002,ISBN 1-4020-0604-7,ISBN 978-1-4020-0604-3
• Kurt Gödel (Mar 1995). Solomon Feferman; John W. Dawson jr.; Warren Goldfarb; Charles parsons; Robert M. Solovay (eds.).Unpublished Essays and Lectures(PDF). Collected Works. Vol. III (1st ed.). Oxford: Oxford University Press.ISBN 0-19-507255-3. — See Chapter "Ontological Proof", pp. 403–404, and Appendix B "Texts Relating to the Ontological Proof", pp. 429–437.
• Goldman, Randolph R. "Gödel's Ontological Argument", PhD Diss., University of California, Berkeley 2000.
• Hazen, A. P. "On Gödel's Ontological Proof", Australasian Journal of Philosophy, Vol. 76, No 3, pp. 361–377, September 1998
• Small, Christopher."Reflections on Gödel's Ontological Argument"(PDF).University of Waterloo. Archived fromthe original(PDF) on 2009-12-22. Retrieved2010-08-31.
• Wang, Hao (1987).Reflections on Kurt Gödel. Cambridge, Mass: MIT Press.ISBN 0-262-23127-1.
• Wang, Hao (1996).A Logical Journey: from Gödel to Philosophy. Cambridge, Mass: MIT Press.ISBN 0-262-23189-1.

• Oppy, Graham."Ontological arguments". InZalta, Edward N. (ed.).Stanford Encyclopedia of Philosophy.
• Annotated bibliography of studies on Gödel's Ontological Argument
• Thomas Gawlick,Was sind und was sollen mathematische Gottesbeweise?, Jan. 2012 — shows Gödel's original proof manuscript on p. 2-3
• A Divine Consistency Proof for Mathematics — A submitted work byHarvey Friedman showing that if God exists (in the sense of Gödel), then Mathematics, as formalized by the usualZFC axioms, is consistent.

• Arguments for the existence of God
• Modal logic
• Works by Kurt Gödel

• CS1 German-language sources (de)
• Articles with short description
• Short description is different from Wikidata
• Wikipedia articles needing clarification from August 2016
• All articles with unsourced statements
• Articles with unsourced statements from December 2020
• Articles with unsourced statements from May 2016