In his paper Jokes and their Relation to the Cognitive Unconscious: Marvin Minsky argued that a sense of humor would be an essential component of a rational agent. His argument went a bit like this: an AI would use need to use logic to deduce consequences from their data about the world. However, any sufficiently large database of facts would inevitably contain inconsistencies, and a blind application of ex falso quodlibet would lead to disaster.
The bus timetable, which you believe to be correct, says the bus arrives at 3:35, but it has actually arrived at 3:37. This is a contradiction, and so by ex falso, you think it's a good idea to give me all your money!
Clearly, the correct response to such an argument is to laugh at it and move on. Whence the sense of humor, according to Minksy.
When I first read Anselm's ontological argument for the existence of God, I had the correct Minskyan reaction — I laughed at it and moved on. However, one of the curiosities of mathematical logic is that Kurt Gödel did not laugh at it. He found all of the gaps in Anselm's reasoning, and then — and here we see what being one of the greatest logicians of all time gets you — he proceeded to repair all the holes in the proof.
That is: Gödel has given a proof of the existence of God. So let's look at the proof!
We begin by axiomatizing a predicate
\[ \Good : (i \to \prop) \to \prop \]
To do this, we first give the following auxilliary definitions.
-
$\Godlike : i \to \prop$
$\Godlike(x) = \forall \phi:i \to \prop.\; \Good(\phi) \Rightarrow \phi(x)$ -
$\EssenceOf : i \to (i \to \prop) \to \prop$
$\EssenceOf(x, \phi) = \phi(x) \wedge \forall \psi:i \to \prop.\; \psi(x) \Rightarrow \Box(\forall x.\; \phi(x) \Rightarrow \psi(x))$ -
$\Essential : i \to \prop$
$\Essential(x) = \forall \phi:i \to \prop.\; \EssenceOf(x,\phi) \Rightarrow \Box(\exists y.\phi(y))$
So something is godlike if it has all good properties. Something $x$'s essence is a property $\phi$, if $x$ has property $\phi$, and furthermore every property $x$ has is implied by $\phi$. Something $x$ is essential, if something with its essence necessarily exists. (This sounds like medieval theology already, doesn't it?)
Now, we can give the axioms describing the $\Good$ predicate.
- $\forall \phi:i \to \prop.\; \Good(\lambda x.\lnot \phi(x)) \iff \lnot \Good(\phi)$
- $\forall \phi, \psi:i \to \prop.\; (\forall x:i.\; (\phi(x) \Rightarrow \psi(x))) \Rightarrow \Good(\phi) \Rightarrow \Good(\psi)$
- $\Good(\Godlike)$
- $\Good(\phi) \Rightarrow \Box(\Good(\phi))$
- $\Good(\Essential)$
The first axiom says that every property is exactly good or not good (bad). The second says that if a property is a logical consequence of a good property, it is also a good property. The third says that being godlike is good. The third property says that every good property is necessarily good. Finally, being essential (as opposed to accidental) is good. I feel like I could argue with any of these axioms (except maybe 2), but honestly I'm more interested in the proof itself.
Below, I give Goedel's result, rearranged a bit and put into a natural deduction style. Loosely speaking, I'm using the natural deduction format from Davies and Pfenning's A Judgmental Reconstruction of Modal Logic. In my proof, I use the phrase “We have necessarily $P$” to mean that $P$ goes into the valid context, and I use “Necessarily:” with an indented block following it to indicate that I'm proving a box'd proposition. The rule is that within the scope of a “Necessarily:”, I can only use “necessarily $P$” results from outside of it.
This style is occasionally inconvenient when proving lemmas, so I'll also use the “necessitation rule” from traditional modal logic, which says that if you have a closed proof of $P$, you can conclude $\Box(P)$. (This rule is implied by the Davies and Pfenning rules, but it's handy in informal proofs.)
Now, their proof system is basically for S4, and the ontological argument uses S5. So I'll also make use (as an axiom) of the fact that $\Diamond(\Box(P))$ implies $\Box(P)$ — that is, that possibly necessary things are actually necessary. This saves having to mention world variables in the proof.
Overall, the proof system needed for the proof is a fully impredicative second-order classical S5 — a constructivist may find this a harder lift than the existence of God! (Can God create a consistent axiomatic system so powerful She cannot believe it?) Jokes aside, it's an interesting proof nonetheless.
We begin by showing that any Godlike entity only has necessarily good properties.
Lemma 1. (God is good) $\forall x:i.\; \Godlike(x) \Rightarrow \forall \phi:i \to \prop.\; \phi(x) \Rightarrow \Box(\Good(\phi))$
Proof.
- Assume $x$ and $\Godlike(x)$, $\phi$ and $\phi(x)$.
- For a contradiction, suppose $\lnot \Good(\phi)$.
- Then by axiom 1, $\Good(\lambda x.\lnot \phi(x))$.
- Unfolding $\Godlike$ and instantiating with $\lambda x.\;\lnot \phi(x), \Good(\lambda x.\lnot \phi(x)) \Rightarrow \lnot \phi(x)$.
- We know $\Good(\lambda x.\lnot \phi(x))$.
- Hence $\lnot \phi(x)$
- This contradicts $\phi(x)$.
- Therefore $\Good(\phi)$.
- By Axiom 4, $\Box(\Good(\phi))$.
Then, we show that all of a Godlike entity's properties are entailed by being Godlike. I was initially tempted to dub this the “I am that I am” lemma, but decided that “God has no hair” was funnier. The name comes from the theorem in physics that “black holes have no hair” — they are completely characterized by their mass, charge and angular momentum. Similarly, here being Godlike completely characterizes Godlike entities.
If you accept Leibniz's principle, this implies monotheism, as well. Hindus and Buddhists will disagree, because they often deny that things are characterized by their properties. (For differing reasons, Jean-Paul Sartre might say the same, too, as would Per Martin-Löf!)
Lemma 2. (God has no hair): $\forall x:i.\; \Godlike(x) \Rightarrow \EssenceOf(x, \Godlike)$
Proof.
- Assume $x$ and $\Godlike(x)$.
- By definition, $\EssenceOf(x, \Godlike)$ = $\Godlike(x) \wedge \forall \psi:i \to \prop.\; \psi(x) \Rightarrow \Box(\forall x.\; \Godlike(x) \Rightarrow \psi(x))$
-
- $\Godlike(x)$ holds by assumption.
- Assume $\psi:i \to \prop$ and $\psi(x)$.
- By Lemma (God is good), $\Box(\Good(\psi))$.
- So necessarily $\Good(\psi)$.
- Necessarily:
- Assume $x$ and $\Godlike(x)$.
- By definition of $\Godlike$, $\Good(\psi) \Rightarrow \psi(x)$.
- But necessarily $\Good(\psi)$.
- Hence $\psi(x)$
- Therefore $\forall x.\; \Godlike(x) \Rightarrow \psi(x)$
- Assume $x$ and $\Godlike(x)$.
- Therefore $\Box(\forall x.\; \Godlike(x) \Rightarrow \psi(x))$
- Therefore $\forall \psi:i \to \prop.\; \psi(x) \Rightarrow \Box(\forall x.\; \Godlike(x) \Rightarrow \psi(x))$
- Therefore $\EssenceOf(x, \Godlike)$
Next, we show that if a Godlike object could exist, then a Godlike entity necessarily exists.
Lemma 3. (Necessary Existence): $(\exists x:i.\; \Godlike(x)) \Rightarrow \Box(\exists y:i.\; \Godlike(y))$
Proof.
- Assume there is an $x$ such that $\Godlike(x)$.
- By axiom 5, $\Good(\Essential)$.
- By the definition of $\Godlike$, we have $\Essential(x)$.
- Unfolding $\Essential$, we get $\forall \phi:i \to \prop. \EssenceOf(x,\phi) \Rightarrow \Box(\exists y.\phi(y))$
- By Lemma (God has no hair), We know $\EssenceOf(x, \Godlike)$.
- Hence $\Box(\exists y:i.\; \Godlike(y))$
We can now show that the above implication is itself necessary. We could have stuck all of the above theorems inside a “Necessarily:” block, but that would have been an annoying amount of indentation. So I used the necessitation principle, which is admissible in Davies/Pfenning.
Lemma 4. (Necessary Necessary Existence): $\Box(\exists x:i.\; \Godlike(x)) \Rightarrow \Box(\exists y:i.\; \Godlike(y))$
Proof. By inlining the proofs of all the earlier lemmas, we can give a closed proof of the necessary existence lemma (i.e., using nothing but the axioms and definitions).
So by necessitation, we get $\Box(\exists x:i.\; \Godlike(x)) \Rightarrow \Box(\exists y:i.\; \Godlike(y))$.
Now, we‘ll show that it's possible that God exists. I would have called it the “no atheists in foxholes” lemma, except that the US military atheists’ association maintains a list of atheists in foxholes.
Lemma 5. (God is possible): $\Diamond (\exists x.\Godlike(x))$
Proof.
- For a contradiction, suppose $\Box(\forall y:i.\lnot \Godlike(y))$.
- Assume $y$ and $\Godlike(y)$.
- Instantiating the contradiction hypothesis, $\lnot \Godlike(y)$.
- Therefore $\forall y:i.\; \Godlike(y) \Rightarrow \lnot \Godlike(y)$.
- By Axiom 2, $\Good(\lambda y.\lnot \Godlike(y))$
- By Axiom 1, $\lnot \Good(\Godlike)$.
- By Axiom 3, $\Good(\Godlike)$.
- This is a contradiction.
- Assume $y$ and $\Godlike(y)$.
- Therefore $\lnot \Box(\forall y.\lnot \Godlike(y))$.
- By quantifier twiddling, $\lnot \Box(\lnot \exists y.\Godlike(y))$
- By clasical definition of possibility $\Diamond (\exists y.\Godlike(y))$
Now we can finish off Gödel's argument!
Theorem 1. (God necessarily exists): $\Box(\exists y:i.\; \Godlike(y))$
Proof.
- By Lemma (Necessary Necessary Existence), $\Box[(\exists x:i.\; \Godlike(x)) \Rightarrow \Box(\exists y:i.\; \Godlike(y))]$
- Necessarily $(\exists x:i.\; \Godlike(x)) \Rightarrow \Box(\exists y:i.\; \Godlike(y))$.
- By Lemma (God is Possible), $\Diamond ((\exists x:i.\; \Godlike(x)))$.
- Stipulating $\exists x:i.\; \Godlike(x)$:
- By using the implication, $\Box(\exists y:i.\; \Godlike(y))$.
- Therefore $\Diamond \Box(\exists y:i.\; \Godlike(y))$.
- In S5, $\Diamond \Box P$ implies $\Box P$ for any $P$.
- Therefore $\Box(\exists y:i.\; \Godlike(y))$
When I set out to understand this proof, I wanted to see where the proof was nonclassical — I initially thought it would be funny to constructivize his argument and announce the existence of a computer program which was a realizer for God. It turns out that this is impossible, since this is a deeply classical argument. However, there might still be some computational content in this proof, since Jean-Louis Krivine has looked at realizability interpretations of very powerful classical systems such as ZF set theory. AFAICT, the tricky part will be finding a specific predicate satisfying the axioms of $\Good$.
However, as far as understanding the proof goes, the use of excluded middle actually turns out to not bother me overmuch. After all, proving that it is not the case that God doesn't exist, sort of makes a good case for apophatic theology, which is pretty congenial to me as a cultural (albeit firmly atheist) Hindu!
Instead, the part I find most difficult to swallow is the proof of the possible existence of God, because it runs afoul of relevance. Specifically, the proof that $\Godlike(y) \Rightarrow \lnot \Godlike(y)$ does not use its hypothesis. As a result, I find myself quite dubious that being $\Godlike$ is a $\Good$ property (Axiom 3).
