# A Simplified Variant of G"odel's Ontological Argument

arXiv: https://arxiv.org/abs/2202.06264 · HTML: https://mlsanity.com/paper/2202.06264/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 24 references that are in the map.
- First posted on arXiv 13 Feb 2022.

## Builds on (most cited first, 3 of 3)

- [Formalization, Mechanization and Automation of G"odel's Proof of God's Existence](https://mlsanity.com/paper/1308.4526/) (2013)
- [Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of G"odel's Ontological Argument](https://mlsanity.com/paper/1910.08955/) (2019)
- [A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of G"odel's Ontological Argument](https://mlsanity.com/paper/2001.04701/) (2020)

## Abstract (arXiv)

A simplified variant of G"odel's ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by G"odel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments was the computer encoding of G"odel's argument, and then automated reasoning techniques were systematically applied to arrive at the simplified variant presented. The presented work thus exemplifies a fruitful human-computer interaction in computational metaphysics. Whether the presented result increases or decreases the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology.