Formalization, Mechanization and Automation of G\"odel's Proof of God's Existence

TL;DR

This paper provides a comprehensive formal analysis of G"odel's ontological proof of God's existence using multiple theorem provers and proof assistants, enhancing understanding and verification of the proof's validity.

Contribution

It introduces a detailed formalization and mechanization of G"odel's proof, employing various automated tools and proof assistants for the first time.

Findings

Verification of axioms' consistency with Nitpick

Automated theorem proving with LEO-II and Satallax

Step-by-step formalization in Coq and Isabelle

Abstract

G\"odel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis.