Gödel's ontological argument, step by step

Update 2015: I wrote a new series on ontological arguments.

By request, I am going to explain Gödel's ontological argument step by step, for your reference. Here's how it will work. I am following the symbolic logic proof shown on the Wikipedia article.* In the first section, I will explain everything in English. In the second section, I will write out the proof symbolically, expanding out steps as much as I feel necessary.

Please skip to the section of your preferred level of precision.

*Please note that there are several different variations of Gödel's ontological argument with different sets of axioms and different steps. C. G. Small has another explanation, using a different variation of Gödel's argument.

Section 1: English

All capital letters represent any given property. All small letters represent objects. I use the word "negative" to merely mean non-positive.

• Entailment: V "entails" W if and only if in all possible worlds, all objects with property V also have property W. Note that if in all possible worlds, there is not a single object with property V, then V automatically entails W.
  
  
• Axiom 1: If Z entails Y, and if Z is positive, then Y is also positive.
  
  
• Axiom 2: For all properties Z, either Z is positive or not-Z is positive, but not both.
  
  
• Theorem 1: If a property Q is positive, then in some possible world there exists an object with property Q.
• Proof by contradiction:
• Suppose that Q is positive, and that there is not any possible world where there exists an object with property Q.
• Then in all possible worlds, there are no objects with property Q.
• Therefore Q entails any given property. Q entails R and Q entails not-R.
• Therefore R and not-R are both positive. This contradicts Axiom 2.
  
  
• God-like: An object is "god-like" if and only if the object has every property which is positive. Note that a god-like object cannot have any negative properties. If a god-like object had negative property V, then it would fail to have the positive property not-V.
  
  
• Axiom 3: The property of being god-like is a positive property.
  
  
• Theorem 2: In some possible world, there exists an object which is god-like.
• Since god-like is a positive property, Theorem 1 states that in some possible world there exists an object with the god-like property.
  
  
• Essence: Property V is an "essence" of x if and only if the following conditions hold:
• The object x has the property V.
• If x has any property U, then V entails U.
  
  
• Axiom 4: If a property is positive, then it is positive in all possible worlds.
  
  
• Theorem 3: If an object x is god-like, then the god-like property is the essence of x.
  
• Suppose x has any property Q. x cannot have any negative properties, so Q must be positive.
  
• Therefore, in all possible worlds, Q is a positive property.
• Therefore, in all possible worlds, any god-like object must have property Q.
  
• Therefore the god-like property entails Q.
  
  
• Necessary existence: Object x is "necessarily existing" if and only if the following condition holds: For any property V, if V is an essence of x, then in all possible worlds there exists an object with property V.
  
  
• Axiom 5: Necessary existence is a positive property.
  
  
• Theorem 4: In all possible worlds, there exists a god-like object.
• We know that in some possible world, there exists a god-like object.
• Since necessary existence is a positive property in all possible worlds, that god-like object must be necessarily existing.
• That object has the god-like property as its essence.
  
• By the definition of necessary existence, there must, in all possible worlds, exist an object which has the god-like property.
  
  
• Corrolary 1: If there are two god-like objects, then they cannot have any properties which are different.
• Proof by contradiction:
• Suppose we have two god-like objects, and some property Q which applies to one object, but not the other.
• Since god-like objects cannot have negative properties, Q must be positive.
• Similarly, not-Q must be positive. This contradicts Axiom 2.

Section 2: Symbolic Logic

P represents the property of being "positive". G represents the property of being "god-like". NE represents the property of necessary existence. All other capital letters represent any given property. All small letters represent objects. The letters "ess" represent "is the essence of".

[Update April 2015: I finally converted all these equations to LaTeX. Hope that makes it more readable! Javascript must be enabled.]

• Axiom 1: $\{P(Z) \wedge \square\forall x[Z(x) \Rightarrow Y(x)]\} \Rightarrow P(Y)$
  
  
• Axiom 2: $P(\lnot Z) \Leftrightarrow \lnot P(Z)$
  
  
• Theorem 1: $P(Q) \Rightarrow \Diamond \exists x[Q(x)]$
  
• Proof (by contradiction):
• Suppose $P(Q) \wedge \lnot \Diamond \exists x[Q(x)]$
• $\square\forall x[\lnot Q(x)]$
• $\square\forall x[Q(x) \Rightarrow \lnot R(x)]$
• $P(\lnot R)$ (By Axiom 1)
• $\lnot P(R)$ (By Axiom 2)
  
• $\square\forall x[Q(x) \Rightarrow R(x)]$
• $P(R)$ (By Axiom 1)
• $\lnot P(R) \wedge P(R)$ (Contradiction)
  
  
• Definition of G: $G(x) \Leftrightarrow \forall V[P(V) \Rightarrow V(x)]$
  
  
• Axiom 3: $P(G)$
  
  
• Theorem 2: $\Diamond \exists x[G(x)]$
• Proof: Combine Axiom 3 and Theorem 1
  
  
• Definition of ess: $V~ess~x \Leftrightarrow V(x) \wedge \forall U\{U(x) \Rightarrow \square\forall y[V(y) \Rightarrow U(y)]\}$
  
  
• Axiom 4: $P(Z) \Rightarrow \square P(Z)$
  
  
• Theorem 3: $G(x) \Rightarrow G~ess~x$
• Proof: Suppose $G(x) \wedge Q(x)$
  
• $P(\lnot Q) \Rightarrow \lnot Q(x)$ (By definition of G)
• $Q(x) \Rightarrow \lnot P(\lnot Q)$
• $\lnot P(\lnot Q)$
• $P(Q)$ (By Axiom 2)
• $\square P(Q)$ (By Axiom 4)
• Suppose (for contradiction) that $\lnot \square\forall y[G(y) \Rightarrow Q(y)]$
• $\Diamond \exists y[G(y) \wedge \lnot Q(y)]$
• $\Diamond \exists y[[P(Q) \Rightarrow Q(y)] \wedge \lnot Q(y)]$ (By definition of G)
• $\Diamond \exists y[\lnot P(Q)]$
• $\Diamond \lnot P(Q)$
• $\lnot \square P(Q)$
• $\square P(Q) \wedge \lnot \square P(Q)$ (contradiction)
• $\forall Q\{ Q(x) \Rightarrow \square\forall y[G(y) \Rightarrow Q(y)] \}$
• $G~ess~x$ (By definition of ess)
  
  
• Definition of NE: $NE(x) \Leftrightarrow \forall V[V~ess~x \Rightarrow \square \exists y V(y)]$
  
  
• Axiom 5: $P(NE)$
  
  
• Theorem 4: $\square \exists x G(x)$
• Proof:
• $\Diamond \exists y[G(y)]$ (Theorem 2)
• $\square P(NE)$ (By Axiom 4)
  
• $\Diamond \exists y[G(y) \wedge NE(y)]$ (By definition of G)
• $\Diamond \exists y[G(y) \wedge ( G~ess~y \Rightarrow \square \exists x G(x) )]$ (By definition of NE)
• $\Diamond \exists y[G~ess~y \wedge ( G~ess~y \Rightarrow \square \exists x G(x) )]$ (By Theorem 3)
• $\Diamond \exists y[\square \exists x G(x) ]$
• $\Diamond \square \exists x G(x)$
• Lemma: $\Diamond \square S \Rightarrow \square S$ for any statement S
• $\Diamond \lnot S \Rightarrow \square\Diamond \lnot S$ (an axiom of modal logic)
• $\lnot \square\Diamond \lnot S \Rightarrow \lnot \Diamond \lnot S$
• $\Diamond \square S \Rightarrow \square S$
• $\square \exists x G(x)$
  
  
• Corrolary 1: $G(x) \wedge G(y) \Rightarrow \forall Q[Q(x) \Leftrightarrow Q(y)]$
  
• Proof (by contradiction):
• Suppose $G(x) \wedge G(y) \wedge \exists Q[ Q(x) \wedge \lnot Q(y) ]$
• $P(\lnot Q) \Rightarrow \lnot Q(x)$ (By definition of G)
• $\lnot P(\lnot Q)$
• $P(Q)$ (By Axiom 2)
  
• $P(Q) \Rightarrow Q(y)$ (By definition of G)
• $\lnot P(Q)$
• $\lnot P(Q) \wedge P(Q)$ (Contradiction)

Questions, corrections welcome.

I realize that in the comments, it's hard to use symbols which don't appear on a keyboard. The following symbols will be understood:
~ or $\lnot$ is "not"
[] or $\square$ is "in all possible worlds" or "it is necessary that"
<> or $\Diamond$ is "in some possible world" or "it is possible that"
=> or $\Rightarrow$ is "if ..., then..."
<=> or $\Leftrightarrow$ is "if and only if"
^ or $\wedge$ is "and"
v or $\vee$ is "or"
E or $\exists$ is "there exists"
A or $\forall$ is "for every" or "for all"