Gödel's God in Isabelle/HOL

Christoph Benzmüller 🌐 and Bruno Woltzenlogel Paleo 🌐

November 12, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session GoedelGod

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{https://isa-afp.org/entries/GoedelGod.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: