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

TL;DR

This paper introduces a simplified, valid version of G"odel's ontological argument that avoids complex predicates and modal collapse, derived through automated reasoning and human-computer interaction.

Contribution

It presents a new, simplified variant of G"odel's ontological argument, validated in basic modal logics, obtained via automated reasoning and proof assistant interaction.

Findings

Valid in modal logics K and KT

Avoids modal collapse and complex predicates

Demonstrates effective human-computer collaboration

Abstract

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.