1. Introduction
The purpose of this webpage is to provide a proof of the modal ontological argument’s logical validity in S5 modal logic (which is a variety of symbolic logic). The modal ontological argument for God’s existence goes something like this:
- Necessarily: If God exists, he exists necessarily.
- Possibly, God exists.
- Therefore, God exists.
In logic, an argument is valid if the conclusion follows the premises necessarily by the rules of logic. Thus, if I prove the above ontological argument’s validity, I’ll be proving that the conclusion follows from the premises.
I’ll recap some logic stuff in this webpage, but it won’t be a full introduction to propositional logic. For that, see my introductory logic series. I will however briefly describe some relevant concepts of S5 modal logic.
2. Some Symbolic Logic
Some of the logic I will use (including the various names for the rules of logic) can be found in this introductory logic page. I won’t go into the various rules of logic here but I will explain what some symbols mean. First there are symbols of basic propositional logic:
| Type of connective | English | Symbolic Logic | When it’s true/false |
|---|---|---|---|
| Conjunction | p and q | p ∧ q | True if both are true; otherwise false |
| Disjunction | p or q | p ∨ q | False if both are false; otherwise true |
| Conditional | If p, then q | p → q | False if p is true and q is false; otherwise true |
| Biconditional | p, if and only if q | p ↔ q | True if both have the same truth-value (i.e. both are true or both are false); otherwise false |
| Negation | Not-p | ¬p | True if p is false; false if p is true |
In philosophy, a possible world is a complete description of the way reality is or could have been like. On possible world semantics, a proposition is possibly true if and only if it is true in at least one possible world, and a proposition is necessarily true if and only if it is true in all possible worlds (at least in S5 modal logic).
| English | Symbolic Logic | When it’s true/false |
|---|---|---|
| p is possible | ◊p | True if p is true in at least on possible world; otherwise false |
| p is necessary | □p | True if p is true in all possible worlds; otherwise false |
| p is not possible | ¬◊p | True if p is false in all on possible worlds; otherwise true |
Note that ¬◊p is equivalent to □¬p. Indeed, the ◊ and □ operators can even be defined in terms of each other; e.g. one could define ◊ as “true in at least one possible world” and then define □ as this:
□p ≝ ¬◊¬p
As suggested earlier, I won’t recap the rules of propositional logic here (for that, see my introductory logic series) but I’ll explain relevant rules of S5 modal logic which go as follows:
| necessity elimination |
|---|
|
□p ∴ p |
| T-reiteration, necessity introduction | ||||||
|---|---|---|---|---|---|---|
| ||||||
| S5-reiteration, necessity introduction | ||||||
|---|---|---|---|---|---|---|
| ||||||
3. The Proof
With that out of the way, here’s a proof of the modal ontological argument:
| (1) | □(G → □G) | |||
| (2) | ◊G | |||
| (3) | ◊¬G | indirect proof assumption | ||
| (4) | □ | ◊¬G | 3, S5-reiteration | |
| (5) | ¬□¬¬G | 4, equivalence | ||
| (6) | ¬□G | 5, double negation | ||
| (7) | G → □G | 1, T-reiteration | ||
| (8) | ¬G | 6, 7, modus tollens | ||
| (9) | □¬G | 4-8, necessity introduction | ||
| (10) | ¬◊¬¬G | 9, equivalence | ||
| (11) | ¬◊G | 10, double negation | ||
| (12) | ¬◊G ∧ ◊G | 2, 11, conjunction introduction | ||
| (13) | ¬◊¬G | 3-12, indirect proof | ||
| (14) | □G | 13, equivalence | ||
| (15) | G | 14, necessity elimination | ||
