Gödel's Ontological Argument

The following version of the argument is taken from Wikipedia.

Axiom 1. $(P(\phi )\wedge \square \forall x(\phi (x)\Rightarrow \psi (x)))\Rightarrow P(\psi )$.

Axiom 2. $P(\neg \phi )\iff \neg P(\phi )$.

Theorem 1. $P(\phi )\Rightarrow ◊\exists x\phi (x)$.

Definition 1. $G(x)\iff \forall \phi (P(\phi ))\Rightarrow \phi (x))$.

Axiom 3. $P(G)$.

Theorem 2. $◊\exists xG(x)$.

Definition 2. $\phi \mathrm{ess}x\iff \phi (x)\wedge \forall \psi (\psi (x)\Rightarrow \square \forall y(\phi (y)\Rightarrow \psi (y)))$.

Axiom 4. $P(\phi )\Rightarrow \square P(\phi )$.

Theorem 3. $G(x)\Rightarrow G\mathrm{ess}x$.

Definition 3. $E(x)\iff \forall \phi (\phi \mathrm{ess}x\Rightarrow \square \exists y\phi (y))$.

Axiom 5. $P(E)$.

Theorem 4. $\square \exists xG(x)$.

We could give purely formal proofs of the theorems. However, we decide to take an informal approach.

Proof of Theorem 1

Suppose $P(\phi )$ and $\square \forall x\neg \phi (x)$. Therefore, $\square \forall x(\phi (x)\Rightarrow \neg \phi (x))$. By Axiom 1, $P(\neg \phi )$. By Axiom 2, $\neg P(\phi )$, a contradiction.

Proof of Theorem 2

By Axiom 3, $P(G)$. By Theorem 1, $◊\exists xG(x)$.

Proof of Theorem 3

Let $x$ be an arbitrary object and suppose $G(x)$. Then for all $\phi$, $P(\phi )\Rightarrow \phi (x)$. Let $\psi$ be an arbitrary property and suppose $\psi (x)$. Let $w$ be an arbitrary world, $y$ an arbitrary object in $w$, and suppose $G(y)$. If $P(\psi )$, then by Axiom 4, $\square P(\psi )$, so by Definition 1, $\psi (y)$, hence $G\mathrm{ess}x$. If $\neg P(\psi )$, then by Axiom 2, $P(\neg \psi )$. By Definition 1, $\neg \psi (x)$, contradicting $\psi (x)$. Therefore, $G\mathrm{ess}x$.

Proof of Theorem 4

By Theorem 2, $◊\exists xG(x)$. By Axiom 5, $P(E)$, so Axiom 4 implies $\square P(E)$. Let $w$ be a world such that $\exists xG(x)$ is true at $w$. Then $G(a)$ is true at $w$ for some object $a$ in $w$. We have $P(E)$ is true at $w$, so by Definition 1, $E(a)$ is true at $w$. By Definition 3 and Theorem 3, $\square \exists xG(x)$ is true at $w$, so $◊\square \exists xG(x)$. By the S5 Axiom, $\square \exists xG(x)$.

Kurt Gödel Ontological Argument God