Benzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Scott, DanaDanaScott2025-04-232025-04-2320251436-5081https://fis.uni-bamberg.de/handle/uniba/107698Notes on Kurt Gödel’s modal ontological argument and Dana Scott’s variant of it are presented. These remarks, supported by experimental studies with a proof assistant system for classical higher-order logic, implicitly answer some questions the authors have received over the last decade(s). In addition, some new insights resulting from the conducted experiments are reported.engGödel’s ontological argumentInteractive and automated theorem provingHigher-order modal logicarticle10.1007/s00605-025-02078-xhttps://link.springer.com/content/pdf/10.1007/s00605-025-02078-x.pdf