View source for Gödel's ontological proof

'''Gödel's ontological proof''' is a formal argument by the mathematician [[Kurt Gödel]] (1906–1978) for the [[existence of God]]. The argument is in a line of development that goes back to [[Anselm of Canterbury]] (1033–1109).  St. Anselm's [[ontological 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 in [[reality]]. Therefore, God must exist." A more elaborate version was given by [[Gottfried Leibniz]] (1646–1716); this is the version that Gödel studied and attempted to clarify with his ontological argument.

Gödel left a fourteen-point outline of his philosophical beliefs in his papers.<ref>In: Wang, Hao. ''A Logical Journey: From Gödel to Philosophy.'' A Bradford Book, 1997. Print. p.316.</ref> 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.

== History ==
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 allowed [[Dana Scott]] to copy out a version of the proof, which circulated privately. In August 1970, Gödel told [[Oskar 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)."<ref>Quoted in Gödel 1995, p. 388. The German original is quoted in Dawson 1997, p. 307. The nested parentheses are in Morgenstern's original diary entry, as quoted by Dawson.</ref> 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.<ref>The publication history of the proof in this paragraph is from Gödel 1995, p. 388</ref>

Morgenstern's diary is an important and usually reliable source for Gödel's later years, but the implication of the August 1970 diary entry—that Gödel did not believe in God—is not consistent with the other evidence. In letters to his mother, who was not a churchgoer and had raised Kurt and his brother as [[freethinker]]s,<ref>Dawson 1997, pp. 6.</ref> Gödel argued at length for a belief in an afterlife.<ref>Dawson 1997, pp. 210–212.</ref> He did the same in an interview with a skeptical [[Hao Wang (academic)|Hao 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."<ref>Wang 1996, p. 317. The ellipsis is Wikipedia's.</ref> 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."<ref>Wang 1996, p. 51.</ref> In an unmailed answer to a questionnaire, Gödel described his religion as "baptized Lutheran (but not member of any religious congregation). My belief is ''[[Theism|theistic]]'', not [[Pantheism|pantheistic]], following [[Gottfried Wilhelm Leibniz|Leibniz]] rather than [[Spinoza]]."<ref group=note>Gödel's answer to a special questionnaire sent him by the sociologist Burke Grandjean. This answer is quoted directly in Wang 1987, p. 18, and indirectly in Wang 1996, p. 112. It's also quoted directly in Dawson 1997, p. 6,
who cites Wang 1987.

The Grandjean questionnaire is perhaps the most extended autobiographical item in Gödel's papers. Gödel filled it out in pencil and wrote a cover letter, but he never returned it. "Theistic" is italicized in both Wang 1987 and Wang 1996. It is possible that this italicization is Wang's and not Gödel's.

The quote follows Wang 1987, with two corrections taken from Wang 1996. Wang 1987 reads "Baptist Lutheran" where Wang 1996 has "baptized Lutheran". "Baptist Lutheran" makes no sense, especially in context, and was presumably a typo or mistranscription. Wang 1987 has "rel. cong.", which in Wang 1996 is expanded to "religious congregation".</ref>

==Outline==

The proof uses [[modal logic]], which distinguishes between [[logical truth|''necessary'' truths]] and [[Contingency (philosophy)|''contingent'' truths]]. In the most common semantics for modal logic, many "[[Modal logic#Semantics|possible worlds]]" are considered. A [[truth]] is ''necessary'' if it is true in all possible worlds. By contrast, a truth is ''contingent'' if it just happens to be the case. For instance, "more than half of this planet is covered by water" is a contingent truth, that relies upon which planet "this planet" is. If a statement happens to be true in our world, but is false in another world, then it is a contingent truth. A statement that is true in some world (not necessarily our own) is called a ''[[logically possible|possible]]'' truth.

Furthermore, the proof uses [[higher-order logic|higher-order]] (modal) logic because the definition of God employs an explicit quantification over properties.<ref>Fitting, 2002, p. 139</ref>

First, Gödel axiomatizes the notion of a "positive property":<ref group=note>This assumes that it is possible to single out ''positive'' properties from among all properties. Gödel comments that "Positive means positive in the [[moral]] [[aesthetics|aesthetic]] sense (independently of the accidental structure of the world)... It may also mean pure ''attribution'' as opposed to ''privation'' (or containing privation)." (Gödel 1995), see also manuscript in (Gawlick 2012).</ref> for each property ''φ'', either ''φ'' or its [[negation]] ¬''φ'' 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).<ref group=note>As a profane example, if the property of being green is positive, that of not being red is, too (by axiom 1), hence that of being red is negative (by axiom 2).</ref> 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), and requiring that property to be positive itself (axiom 3),<ref group=note> If one considers the [[partial order]] <math> \preceq </math> defined by <math> \varphi \preceq \psi </math> iff <math> \square \forall y (\varphi(y) \to \psi(y)) </math>, then Axioms 1-3 can be summarized by saying that positive properties form an [[ultrafilter]] on this ordering. Definition 1 and Axiom 4 are needed to establish the ''Godlike'' property as principal element of the ultrafilter. </ref> Gödel shows that in ''some'' possible world a Godlike object exists (theorem 2), called "God" in the following.<ref group=note>By removing all modal operators from axioms, definitions, proofs, and theorems, a modified version of theorem 2 is obtained saying "∃''x'' ''G''(''x'')", i.e. "There exists an object which has all positive, but no negative properties". Nothing more than axioms 1-3, definition 1, and theorems 1-2 needs to be considered for this result.</ref> Gödel proceeds to prove that a Godlike object exists in ''every'' possible world.

To this end, he defines ''essences'': if ''x'' is an object in some world, then a property ''φ'' is said to be an essence of ''x'' if ''φ''(''x'') is true in that world and if ''φ'' necessarily entails all other properties that ''x'' 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 to ''exist necessarily'' if, for every essence ''φ'' of ''x'', there is an element ''y'' 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{{clarify|reason=They should be stated.|date=August 2016}} 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, the [[identity 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.

===Symbolic notation===

<math>
\begin{array}{rl}

\text{Ax. 1.} & \left(P(\varphi) \;\wedge\; \Box \; \forall x (\varphi(x) \Rightarrow \psi(x))\right) \;\Rightarrow\; P(\psi) \\

\text{Ax. 2.} & P(\neg \varphi) \;\Leftrightarrow\; \neg P(\varphi) \\

\text{Th. 1.} & P(\varphi) \;\Rightarrow\; \Diamond \; \exists x \; \varphi(x) \\

\text{Df. 1.} & G(x) \;\Leftrightarrow\; \forall \varphi (P(\varphi) \Rightarrow \varphi(x)) \\

\text{Ax. 3.} & P(G) \\

\text{Th. 2.} & \Diamond \; \exists x \; G(x) \\

\text{Df. 2.} & \varphi \text{ ess } x \;\Leftrightarrow\; \varphi(x) \wedge \forall \psi \left(\psi(x) \Rightarrow \Box \; \forall y (\varphi(y) \Rightarrow \psi(y))\right) \\

\text{Ax. 4.} & P(\varphi) \;\Rightarrow\; \Box \; P(\varphi) \\

\text{Th. 3.} & G(x) \;\Rightarrow\; G \text{ ess } x \\
		
\text{Df. 3.} & E(x) \;\Leftrightarrow\; \forall \varphi (\varphi \text{ ess } x \Rightarrow \Box \; \exists y \; \varphi(y)) \\
			
\text{Ax. 5.} & P(E) \\
			
\text{Th. 4.} & \Box \; \exists x \; G(x)
  
\end{array}
</math>

==Criticism==

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. This is particularly applicable to Gödel's proof – because it rests on five axioms, some of which are 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 by [[Jordan Howard Sobel]],<ref>{{cite book | author=Jordan Howard Sobel | authorlink=Jordan Howard Sobel | contribution=Gödel's ontological proof | pages=241–261 | isbn=978-0262200639 | editor=Judith Jarvis Thomson | editorlink=Judith Jarvis Thomson | title=On Being and Saying: Essays for Richard Cartwright | location=Cambridge/MA & London, England | publisher=MIT Press | date=Nov 1987 | url-access=registration | url=https://archive.org/details/onbeingsayingess00judi }}</ref> 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 are [[accessibility relation|accessible]] worlds at all).<ref group=note>Formally, <math>p \Rightarrow \Box p</math> for all ''p'' implies <math>\Diamond p \Rightarrow p</math> for all ''p'' by [[indirect proof]], and <math>\Box p \Rightarrow \Diamond p</math> holds for all ''p'' whenever there are accessible worlds.</ref> According to [[Robert Koons]],<ref name="Koons.2005"/>{{rp|9}} Sobel suggested that Gödel might have welcomed modal collapse.<ref>{{cite book | isbn=0-19-507255-3 | url=https://monoskop.org/images/a/aa/Kurt_G%C3%B6del_Collected_Works_Volume_III_1995.pdf | author=Kurt Gödel |editor1 = Solomon Feferman | editor2= John W. Dawson jr. | editor3= Warren Goldfarb | editor4 = Charles parsons | editor5 = Robert M. Solovay | title=Unpublished Essays and Lectures | location=Oxford | publisher=Oxford University Press | series=Collected Works | volume=III | edition=1st | date=Mar 1995 | <!---chapter=Appendix B---> contribution=Texts Relating to the Ontological Proof | pages=429–437}} Here: p.435; probably, Sobel referred to Gödel's note: ''"If <math>\varphi(x) \Rightarrow \Box \varphi(x)</math> is assumed [as following from the essence of <math>x</math>], ... but that is the inferior way. Rather, <math>\varphi(x) \Rightarrow \Box \varphi(x)</math> should follow first from the existence of God."'' The note might indicate that Gödel was aware of his axioms implying modal collapse.</ref>

There are suggested amendments to the proof, presented by [[C. Anthony Anderson]],<ref>{{cite journal | url=https://appearedtoblogly.files.wordpress.com/2011/05/anderson-anthony-c-22some-emendations-of-gc3b6dels-ontological-proof22.pdf | author=Curtis Anthony Anderson | authorlink=Curtis Anthony Anderson | title=Some Emendations of Gödel's Ontological Proof | journal=[[Faith and Philosophy]] | volume=7 | number=3 | pages=291&mdash;303 | date=Jul 1990 | doi=10.5840/faithphil19907325}}</ref> but argued to be refutable by Anderson and Michael Gettings.<ref>{{cite book | contributionurl=https://projecteuclid.org/euclid.lnl/1235417020 | author=Curtis Anthony Anderson and Michael Gettings | contribution=Gödel's ontological proof revisited | editor=Petr Hájek | title=Proc. Gödel '96: Logical Foundations of Mathematics, Computer Science and Physics &mdash; Kurt Gödel's Legacy | publisher=Springer | series=Lecture Notes in Logic | volume=6 | pages=167&mdash;172 | date=Aug 1996 }}</ref> Sobel's proof of modal collapse has been questioned by Koons,<ref name="Koons.2005">{{cite report | url=http://www.robkoons.net/media/69b0dd04a9d2fc6dffff80b4ffffd524.pdf | author=Robert C. Koons | authorlink=Robert Koons |title=Sobel on Gödel's Ontological Proof | institution=University of Texas at Austin | type=Unpublished Paper | date=Jul 2005 }}</ref><ref group=note>Since Sobel's proof of modal collapse uses [[lambda abstraction]], but Gödel's proof does not, Koons suggests to forbid this property-construction operation as the "most conservative" measure, before "rejecting or emending ... axioms (as Anderson does)".</ref> but a counter-defence by Sobel has been given.{{citation needed|date=May 2016}}

Gödel's proof has also been questioned by [[Graham Oppy]],<ref>{{cite journal | url=https://www.researchgate.net/publication/31121878_Godelian_ontological_arguments | author=Graham Oppy | authorlink=Graham Oppy | title=Godelian ontological arguments | journal=Analysis | volume=54 | number=4 | pages=226&mdash;230 | date=Oct 1996 | doi = 10.1093/analys/56.4.226 }} &mdash; [https://www.researchgate.net/profile/Graham_Oppy/publication/31121878_Godelian_ontological_arguments/links/0f3175343e378809ad000000.pdf?origin=publication_detail Longer version (2005)]</ref> asking whether lots of other almost-gods would also be "proven" by Gödel's axioms. This counter-argument has been questioned by Gettings,<ref>{{cite journal | author = Gettings Michael | year = 1999 | title = Gödel's ontological argument: a reply to Oppy | url = | journal = Analysis | volume = 59 | issue = 264| pages = 309–313 | doi=10.1111/1467-8284.00184}}</ref> 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 scholar [[Robert Spitzer (priest)|Fr. Robert J. Spitzer]] accepted Gödel's proof, calling it "an improvement over the Anselmian Ontological Argument (which does not work)."<ref>{{Cite news|url=https://www.magiscenter.com/proof-from-godel-theorem-shows-god-exists-through-super-axiom/|title=Godel's Theorem and the Existence of God|date=2017-04-26|work=Magis Center|access-date=2018-05-23|language=en-US}}</ref>

There are, however, many more criticisms, most focusing on the philosophically interesting 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 famous [[Synthetic geometry#Logical synthesis|remark]] 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 to [[André 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 merely a theological task.<ref>{{cite book | contributionurl=https://dl.dropboxusercontent.com/u/19453127/Homepage/downloads/GoedelExistenzNotwendigkeit.pdf | author=André Fuhrmann | chapter=Existenz und Notwendigkeit &mdash; Kurt Gödels axiomatische Theologie |trans-chapter=Existence and Necessity &mdash; Kurt Gödel's Axiomatic Theology | language=German | pages=349&mdash;374 | editor=W. Spohn | title=Logik in der Philosophie |trans-title=Logic in Philosophy | location=Heidelberg | publisher=Synchron | year=2005 }}</ref>{{rp|364–366}} It is this task which decides which religion's god has been proven to exist.

==Computer-verified versions==

Christoph Benzmüller and Bruno Woltzenlogel-Paleo formalized Gödel's proof to a level that is suitable for [[automated theorem proving]] or at least computer verification via [[proof assistant]]s.<ref>https://github.com/FormalTheology/GoedelGod</ref> The effort made headlines in German newspapers. According to the authors of this effort, they were inspired by [[Melvin Fitting]]'s book.<ref>{{cite news|last=Knight|first=David|title=Scientists Use Computer to Mathematically Prove Gödel's God Theorem|url=http://www.spiegel.de/international/germany/scientists-use-computer-to-mathematically-prove-goedel-god-theorem-a-928668.html|accessdate=28 October 2013|newspaper=Der Spiegel|date=23 October 2013}}</ref>

In 2014, they computer-verified Gödel's proof (in the [[#Symbolic notation|above]] version).<ref name="Benzmuller.Woltzenlogel.2014">{{cite book | contributionurl=http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf | author=Christoph Benzmüller and Bruno Woltzenlogel-Paleo | contribution=Automating Gödel's Ontological Proof of God's Existence with Higher-Order Automated Theorem Provers | editor= | title=Proc. [[European Conference on Artificial Intelligence]] | publisher=IOS Press | series=Frontiers in Artificial Intelligence and Applications | volume=263 | pages=93&mdash;98 | month= | year=2014 }}</ref>{{rp|97}}<ref group=note>Lines "T3" in Fig.2, and item 3 in section 4 ("Main findings"). Their theorem "T3" corresponds to "Th.4" shown [[#Symbolic notation|above]].</ref>
They also proved that this version's axioms are consistent,<ref group=note>Line "CO" in Fig.2, and item 1 in section 4 (p.97).</ref>
but imply modal collapse,<ref group=note>Line "MC" in Fig.2, and item 6 in section 4 (p.97).</ref> thus confirming Sobel's 1987 argument.

In the same paper, they suspected Gödel's original version of the axioms{{#tag:ref|The version shown [[#Symbolic notation|here]] is by Dana Scott.<ref>{{cite book | isbn=978-0511497988 | author=D. Scott | contribution=Appendix B: Notes in Dana Scott's Hand [1972] | pages=145&ndash;146 | editor=J.H. Sobel | title=Logic and Theism: Arguments for and Against Beliefs in God | location=Cambridge | publisher=Cambridge University Press | year=2004 }}</ref> It differs from Gödel's original by omitting the first conjunct, <math>\varphi(x)</math>, in Df.2. |group=note|name="Godel vs Scott"}} to be inconsistent, as they failed to prove their consistency.<ref group=note>Lines "CO'" in Fig.2, and item 5 in section 4 (p.97).</ref>
In 2016, they gave a computer proof that this version implies <math>\Diamond\Box\bot</math>, i.e. is inconsistent in every modal logic with a reflexive or symmetric [[accessibility relation]].<ref name="Benzmuller.Woltzenlogel.2016">{{cite book | contributionurl=http://www.ijcai.org/Proceedings/16/Papers/137.pdf | author=Christoph Benzmüller and Bruno Woltzenlogel-Paleo | contribution=The Inconsistency in Gödel's Ontological Argument: &mdash; A Success Story for AI in Metaphysics | editor=Subbarao Kambhampati | title=Proc. 25th [[International Joint Conference on Artificial Intelligence]] | publisher=AAAI Press | pages=936&mdash;942 | date=Jul 2016 }}</ref>{{rp|940 lf}}
Moreover, they gave an argument that this version is inconsistent in every logic at all,<ref group=note>Item 8 in section 4.1 "Informal argument" (p.940).</ref> but failed to duplicate it by automated provers.<ref group=note>See the detailled discussion in section 4 "Intuitive Inconsistency Argument" (p.939-941).</ref> In the same paper they suggested that modal collapse is not necessarily a flaw.{{dubious|date=June 2019}}

== In literature ==
A humorous variant of Gödel's ontological proof is mentioned in Quentin Canterel's novel ''The Jolly Coroner''.<ref>{{cite book <!--- isbn=9781911079132 --- commented-out: data obtained from http://books.digicafe.info/doc/how-to-xml-mobi-epub2-the-jolly-coroner-321734.html, but could'nt be confirmed by https://en.wikipedia.org/wiki/Special:BookSources/9781911079132 ---> <!--- isbn=978-1-909122-82-6 -- commented out: data obtained from http://www.barnesandnoble.com/w/the-jolly-coroner-quentin-canterel/1122771737?ean=9781909122826, but isbn is wrong according to https://www.amazon.com/s?search-alias=stripbooks&field-isbn=9781909122826 ---> | author=Quentin Canterel | title=The Jolly Coroner: A Picaresque Novel | location= | publisher=Acorn Independent Press | year=2015 }}</ref>{{page needed|date=March 2017}}
The proof is also mentioned in the TV series ''[[Hand of God (TV series)|Hand of God]]''.{{Specify|reason=Which episode?|date=March 2017}}

==See also==
* [[Existence of God]]
* [[Philosophy of religion]]
* [[Theism]]
* [[Ontological argument]]

==Notes==
{{reflist|group=note}}

==References==
{{Reflist}}

==Further reading==
* Bjørdal, Frode. "Understanding Gödel's Ontological Argument", in T. Childers (ed.), ''The Logica Yearbook 1998'', Prague 1999, 214-217.
* 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.
* {{cite book |author=[[John W. Dawson, Jr]]|title=Logical Dilemmas: The Life and Work of Kurt Godel |publisher=AK Peters, Ltd |location=Wellesley, Mass |year=1997 |pages= |isbn=1-56881-025-3 |oclc= |doi=}}
* [[Melvin Fitting]], "Types, Tableaus, and Godel's God" Publisher: Dordrecht Kluwer Academic, 2002, {{ISBN|1-4020-0604-7}}, {{ISBN|978-1-4020-0604-3}}
* {{cite book | isbn=0-19-507255-3 | url=https://monoskop.org/images/a/aa/Kurt_G%C3%B6del_Collected_Works_Volume_III_1995.pdf | author=Kurt Gödel |editor1 = Solomon Feferman | editor2= John W. Dawson jr. | editor3= Warren Goldfarb | editor4 = Charles parsons | editor5 = Robert M. Solovay | title=Unpublished Essays and Lectures | location=Oxford | publisher=Oxford University Press | series=Collected Works | volume=III | edition=1st | date=Mar 1995 }} &mdash; See Chapter "Ontological Proof", pp.&nbsp;403–404, and Appendix B "Texts Relating to the Ontological Proof", pp.&nbsp;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.&nbsp;361–377, September 1998
* {{cite web |url=http://www.stats.uwaterloo.ca/~cgsmall/Godel.final.revision.PDF |title=Reflections on Gödel's Ontological Argument |first=Christopher  |last=Small |location=[[University of Waterloo]]}}
* {{cite book |author=[[Hao Wang (academic)|Wang, Hao]] |title=Reflections on Kurt Gödel |publisher=MIT Press |location=Cambridge, Mass |year=1987 |pages= |isbn=0-262-23127-1 |oclc= |doi=}}
* {{cite book |author=Wang, Hao |title=A Logical Journey: from Gödel to Philosophy |publisher=MIT Press |location=Cambridge, Mass |year=1996 |pages= |isbn=0-262-23189-1 |oclc= |doi=}}

==External links==
*{{cite SEP |url-id=ontological-arguments |title=Ontological arguments |last=Oppy |first=Graham}}
* [https://www.ontology.co/biblio/ontological-proof-contemporary-biblio.htm Annotated bibliography of studies on Gödel's Ontological Argument]
* Thomas Gawlick, ''[http://www.idmp.uni-hannover.de/fileadmin/institut/IDMP-Studium-Mathematik/downloads/Gawlick/Predigt_Gawlick_Gottesbeweise.pdf Was sind und was sollen mathematische Gottesbeweise?]'', Jan. 2012 &mdash; shows Gödel's original proof manuscript on p.&nbsp;2-3
*[https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/ConMathThe122512-1iea8ps.pdf A Divine Consistency Proof for Mathematics]  &mdash; A submitted work by [[Harvey Friedman]] showing that if God exists (in the sense of Gödel), then Mathematics, as formalized by the usual [[Zermelo–Fraenkel set theory|ZFC axioms]], is consistent. 

{{DEFAULTSORT:Godels Ontological Proof}}
[[Category:Arguments for the existence of God]]
[[Category:Modal logic]]
[[Category:Religious philosophy]]
[[Category:Works by Kurt Gödel|Ontological proof]]