Abstract
A computer-formalisation of the essential parts of Fitting's
textbook "Types, Tableaus and Gödel's God" in
Isabelle/HOL is presented. In particular, Fitting's (and
Anderson's) variant of the ontological argument is verified and
confirmed. This variant avoids the modal collapse, which has been
criticised as an undesirable side-effect of Kurt Gödel's (and
Dana Scott's) versions of the ontological argument.
Fitting's work is employing an intensional higher-order modal
logic, which we shallowly embed here in classical higher-order logic.
We then utilize the embedded logic for the formalisation of
Fitting's argument. (See also the earlier AFP entry “Gödel's God in Isabelle/HOL”.)