 Versions of the ontological argument have formed an important thread in recent work employing theorem provers, both because of their inherent interest and the technical challenges they bring with them. Prover9 and Mace have again been used recently by Jack Horner in order to analyze a version of the ontological argument in Spinoza’s Ethics (found invalid) and to propose an alternative (Horner 2019). Significant work has been done on versions of Anselm’s ontological argument (Oppenheimer &amp; Zalta 2011; Garbacz 2012; Rushby 2018). Christoph Benzmüller and his colleagues have applied higher-order theorem provers, including including Isabelle/HOL and their own Leo-II and Leo-III, in order to analyze a version of the ontological argument found in the papers of Kurt Gödel (Benzmüller &amp; Paelo 2016a, 2016b; Benzmüller, Weber, &amp; Paleo 2017; Benzmüller &amp; Fuenmayor 2018). A previously unnoticed inconsistency was found in Gödel’s original, though avoided in Dana Scott’s transcription. Theorem-provers confirmed that Gödel’s argument forces modal collapse—all truths become necessary truths. Analysis with theorem-provers makes it clear that variations proposed by C. Anthony Anderson and Melvin Fitting avoid that consequence, but in importantly different ways (Benzmüller &amp; Paleo 2014; Kirchner, Benzmüller, &amp; Zalta  2019).[13]