Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset)

Christoph Benzmüller 📧

January 7, 2025

Abstract

Experimental studies with Isabelle/HOL on Kurt Gödel’s modal ontological argument and Dana Scott’s variant of it are presented. They implicitly answer some questions that the authors have received over the last decade(s). In addition, some new results are reported. Our contribution is explained in full detail in an associated journal article. This document presents the corresponding Isabelle/HOL dataset (which is only slightly modified to meet AFP requirements).

License

BSD License

Topics

Related publications

  • Notes on Gödel’s and Scott’s Variants of the Ontological Argument, Monatshefte für Mathematik, to appear.

Session Notes_On_Goedels_Ontological_Argument

Cite

× 
@article{Notes_On_Goedels_Ontological_Argument-AFP,
  author  = {Christoph Benzmüller},
  title   = {Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset)},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Notes_On_Goedels_Ontological_Argument.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest