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.


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


Session GoedelGod