Notes 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.