Godel's ontological proof

Godels ontological proof is a formal argument by the mathematician Kurt Godel for the existence of God. The argument is in a line of development that goes back to Anselm of Canterbury. St. Anselms 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 ; this is the version that Godel studied and attempted to clarify with his ontological argument.
Godel left a fourteen-point outline of his philosophical beliefs in his papers. 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.

1. History
The first version of the ontological proof in Godels papers is dated "around 1941". Godel 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, Godel told Oskar Morgenstern that he was "satisfied" with the proof, but Morgenstern recorded in his diary entry for 29 August 1970, that Godel 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)." Godel died January 14, 1978. Another version, slightly different from Scotts, was found in his papers. It was finally published, together with Scotts version, in 1987.
Morgensterns diary is an important and usually reliable source for Godels later years, but the implication of the August 1970 diary entry - that Godel 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 freethinkers, Godel argued at length for a belief in an afterlife. He did the same in an interview with a skeptical Hao Wang, who said: "I expressed my doubts as G spoke Godel smiled as he replied to my questions, obviously aware that his answers were not convincing me." Wang reports that Godels wife, Adele, two days after Godels death, told Wang that "Godel, although he did not go to church, was religious and read the Bible in bed every Sunday morning." In an unmailed answer to a questionnaire, Godel described his religion as "baptized Lutheran but not member of any religious congregation. My belief is theistic, not pantheistic, following Leibniz rather than Spinoza."

2. Outline
The proof uses modal logic, which distinguishes between necessary truths and contingent truths. In the most common semantics for modal logic, many "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 possible truth.
Furthermore, the proof uses higher-order modal logic because the definition of God employs an explicit quantification over properties.
First, Godel axiomatizes the notion of a "positive property": 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. Godel 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, Godel shows that in some possible world a Godlike object exists theorem 2, called "God" in the following. Godel 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, Godel 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 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 Leibnizs 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. Godel did not attempt to do so however, as he purposely limited his proof to the issue of existence, rather than uniqueness.

2.1. Outline Symbolic notation
Ax. 1. P φ ∧ ◻ ∀ x φ x ⇒ ψ x) ⇒ P ψ Ax. 2. P ¬ φ ⇔ ¬ P φ Th. 1. P φ ⇒ ◊ ∃ x φ x Df. 1. G x ⇔ ∀ φ P φ ⇒ φ x) Ax. 3. P G Th. 2. ◊ ∃ x G x Df. 2. φ ess x ⇔ φ x ∧ ∀ ψ x ⇒ ◻ ∀ y φ y ⇒ ψ y) Ax. 4. P φ ⇒ ◻ P φ Th. 3. G x ⇒ G ess x Df. 3. E x ⇔ ∀ φ ess x ⇒ ◻ ∃ y φ y) Ax. 5. P E Th. 4. ◻ ∃ x G x {\displaystyle {\begin{array}{rl}{\text{Ax. 1.}}\leftP\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.}}Gx\;\Leftrightarrow \;\forall \varphi P\varphi\Rightarrow \varphi x)\\{\text{Ax. 3.}}PG\\{\text{Th. 2.}}\Diamond \;\exists x\;Gx\\{\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.}}Gx\;\Rightarrow \;G{\text{ ess }}x\\{\text{Df. 3.}}Ex\;\Leftrightarrow \;\forall \\varphi {\text{ ess }}x\Rightarrow \Box \;\exists y\;\varphi y)\\{\text{Ax. 5.}}PE\\{\text{Th. 4.}}\Box \;\exists x\;Gx\end{array}}}

3. Criticism
Most criticism of Godels 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 Godels 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, 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 accessible worlds at all. According to Robert Koons, Sobel suggested that Godel might have welcomed modal collapse.
There are suggested amendments to the proof, presented by C. Anthony Anderson, but argued to be refutable by Anderson and Michael Gettings. Sobels proof of modal collapse has been questioned by Koons, but a counter-defence by Sobel has been given.
Godels proof has also been questioned by Graham Oppy, asking whether lots of other almost-gods would also be "proven" by Godels axioms. This counter-argument has been questioned by Gettings, who agrees that the axioms might be questioned, but disagrees that Oppys particular counter-example can be shown from Godels axioms.
Religious scholar Fr. Robert J. Spitzer accepted Godels proof, calling it "an improvement over the Anselmian Ontological Argument which does not work."
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. Hilberts famous remark about interchangeability of the primitives names applies to those in Godels ontological axioms as well as to those in Hilberts geometry axioms. According to Andre Fuhrmann 2005 it remains to show that the dazzling notion prescribed by traditions and often believed to be essentially mysterious satisfies Godels axioms. This is not a mathematical, but merely a theological task. It is this task which decides which religions god has been proven to exist.

4. Computer-verified versions
Christoph Benzmuller and Bruno Woltzenlogel-Paleo formalized Godels proof to a level that is suitable for automated theorem proving or at least computer verification via proof assistants. The effort made headlines in German newspapers. According to the authors of this effort, they were inspired by Melvin Fittings book.
In 2014, they computer-verified Godels proof in the above version. They also proved that this versions axioms are consistent, but imply modal collapse, thus confirming Sobels 1987 argument.
In the same paper, they suspected Godels original version of the axioms to be inconsistent, as they failed to prove their consistency. In 2016, they gave a computer proof that this version implies ◊ ◻ ⊥ {\displaystyle \Diamond \Box \bot }, i.e. is inconsistent in every modal logic with a reflexive or symmetric accessibility relation. Moreover, they gave an argument that this version is inconsistent in every logic at all, but failed to duplicate it by automated provers. In the same paper they suggested that modal collapse is not necessarily a flaw.

5. In literature
A humorous variant of Godels ontological proof is mentioned in Quentin Canterels novel The Jolly Coroner. The proof is also mentioned in the TV series Hand of God.