HackerPapers

arXiv:1308.4526cs.LO

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

Christoph Benzmüller, Bruno Woltzenlogel Paleo

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.

arXiv comments
2 pages
Journal reference
Frontiers in Artificial Intelligence and Applications, Volume 263: ECAI 2014
DOI
doi:10.3233/978-1-61499-419-0-93
Subjects
cs.LOLogic in Computer Science cs.AIArtificial Intelligence math.LOLogic

On Hacker News

Linked by 3 identifiable commenters in 3 comments across 3 threads, from Oct 2013 to Jan 2024. Found in 1 HN submission from Sep 2013 to Sep 2013. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments3 threads

  1. Kurt Gödel, his mother and the argument for life after death 1 comment
  2. Gödel's Ontological Proof 1 comment
  3. Formalizations of Gödel's Ontological Proof of God's Existence 1 comment

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.