 In the same tradition as St. Anselm’s, Gödel also provided an ontological proof of God’s existence (Gödel 1970, Scott 1972). An important difference between the two is Gödel’s use of modal operators to represent metaphysical possibility and necessity and, of course, his use of symbolic logic for added reasoning precision. In his proof, Gödel begins by framing the concept of “positive property” using two axioms, and he introduces a definition stating that “A God-like being possesses all positive properties”. This is enough logical machinery to prove as a theorem the possibility of God’s existence, ◊∃xG(x); three more axioms and two additional definitions allow Gödel to further his proof to establish not only that God exists, ∃xG(x), but that this is so by necessity, □∃xG(x). Gödel’s proof is in the formalism of higher-order modal logic (HOML) using modal operators and quantification over properties. Gödel never published his proof but he shared it with Dana Scott who produced the version presented below, which is taken from (Benzmüller &amp; Paleo 2014) along with its English annotation to aid the reader with its intended interpretation: 