Formalization, Mechanization and Automation of Gödel's Proof of God's Existence

Abstract

Gödel'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.

2 pages

Cited by in corpus (6)

• Systematic Verification of the Modal Logic Cube in Isabelle/HOL
• Universal Reasoning, Rational Argumentation and Human-Machine Interaction
• An Expressive Probabilistic Temporal Logic
• Learning $\text{Ex Nihilo}$
• Locating possible sources of physical indeterminism
• Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument