Gödel's God in Isabelle/HOL

Christoph Benzmüller and Bruno Woltzenlogel Paleo

12 November 2013

Abstract

Dana Scott's version of Gödel's proof of God's existence is formalized in quantified modal logic KB (QML KB). QML KB is modeled as a fragment of classical higher-order logic (HOL); thus, the formalization is essentially a formalization in HOL.
BSD License

Topics

Theories

Cite

×
@article{GoedelGod-AFP,
  author  = {Christoph Benzmüller and Bruno Woltzenlogel Paleo},
  title   = {Gödel's God in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = November,
  year    = 2013,
  note    = {\url{http://isa-afp.org/entries/GoedelGod.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download