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.