Computer-supported Assessments of Gödel’s ontological variant 

(and its variants by Scott, Anderson, Fitting)

Background reading

Kurt Gödel's ontological argument and emendations of it (including Dana Scott’s variant) are discussed in various texts, including:

• Sobel, J., 1987, “Gödel’s Ontological Proof”, in On Being and Saying: Essays for Richard Cartwright, J. Thomson (ed.), Cambridge, MA: MIT Press, pp. 241–61.
• Anderson, C., 1990, “Some Emendations on Gödel’s Ontological Proof”, Faith and Philosophy, 7: 291–303.
• Adams, R., 1995b, “Introductory Note to *1970” in K. Gödel Collected Works Volume III: Unpublished essays and lectures, S. Feferman, et al. (eds.), New York: Oxford University Press, pp. 388–402.
• Hazen, A., 1999, “On Gödel’s Ontological Proof”, Australasian Journal of Philosophy, 76: 361–377.
• Fitting, M., 2002, Types, Tableaus, and Gödel’s God, Dordrecht: Kluwer.

Recommended readings on Gödel’s ontological argument (and on ontological arguments in general) also include:

• Sobel, J., 2004, Logic and Theism, New York: Cambridge University Press.
• Sobels’s book in particular contains: 
• K. Gödel. Appx. A: Notes in Kurt Gödel’s Hand, pages 144–145. In [Sobel 2004], 1970.  
• D.Scott, Appx. B: Notes in Dana Scott’s Hand, pages 145–146. In [Sobel 2004], 1972. 

• Szatkowski, M., ed., 2012, Ontological Proofs Today. Ontos Verlag. 
• Oppy, Graham, "Ontological Arguments", The Stanford Encyclopedia of Philosophy (Spring 2020 Edition), Edward N. Zalta (ed.)

Computer-supported formal assessment of Gödel’s ontological argument (and also Scott’s variant)

In 2013 Gödel’ ontological argument was formally reconstructed and assessed by us on the computer:

• Formalization, Mechanization and Automation of Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), Technical report, CoRR, number arXiv:1308.4526, 2013. (complete-formalisation) [bibtex] [url]
• Gödel's God in Isabelle/HOL (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Archive of Formal Proofs, pp. 1--5, 2013. (Note: verified data publication) [bibtex] [url]

The findings include: Gödel’s 1970 variant is inconsistent, Scott’s variant is consistent, modal collapse and monotheism is implied, the argument works already in higher-order modal logic KB. 

Different aspects of our initial studies were presented at several conferences and events:

• Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In ECAI 2014 (Torsten Schaub, Gerhard Friedrich, Barry O'Sullivan, eds.), IOS Press, Frontiers in Artificial Intelligence and Applications, volume 263, pp. 93 -- 98, 2014. (slides) (Preprint: https://www.researchgate.net/publication/265050231) [bibtex] [doi]
• Interacting with Modal Logics in the Coq Proof Assistant (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (Lev D. Beklemishev, Daniil V. Musatov, eds.), Springer, LNCS, volume 9139, pp. 398--411, 2015. (Preprint: https://www.researchgate.net/publication/273201458) [bibtex] [doi]
• Higher-Order Modal Logics: Automation and Applications (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Reasoning Web 2015 (Adrian Paschke, Wolfgang Faber, eds.), Springer, LNCS, number 9203, pp. 32-74, 2015. (Preprint: https://www.researchgate.net/publication/281677232) [bibtex] [doi]
• Experiments in Computational Metaphysics: Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Science & Spiritual Quest, Proceedings of the 9th All India Students' Conference, 30th October -- 1 November, 2015, IIT Kharagpur, India (Subhash C. Mishram, Ramgopal Uppaluri, Varun Agarwal, eds.), Bhaktivedanta Institute, Kolkata, www.binstitute.org, pp. 23-40, 2015. (slides) (Preprint: https://www.researchgate.net/publication/311587544) [bibtex]
• On Logic Embeddings and Gödel's God (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers (Mihai Codescu, Razvan Diaconescu, Ionut Tutu, eds.), Springer, LNCS, number 9563, pp. 3-6, 2015. (Preprint: https://www.researchgate.net/publication/300112614) [bibtex] [doi]
• The Modal Collapse as a Collapse of the Modal Square of Opposition (Christoph Benzmüller, Bruno Woltzenlogel Paleo), Chapter in The Square of Opposition: A Cornerstone of Thought (Collection of papers related to the World Congress on the Square of Opposition IV, Vatican, 2014, Jean-Yves Béziau, Gianfranco Basti, eds.), Birkhäuser Basel, Studies in Universal Logic, pp. 307-313, 2016. (Preprint: https://www.researchgate.net/publication/268211774) [bibtex] [doi]

Assessment of the inconsistency in Gödel’s 1970 variant (which was unknowingly corrected by Scott)

The inconsistency in Gödel’s 1970 variant, which is avoided in Scott’s variant, is assessed in more detail in the following papers:

• The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In IJCAI 2016 (Subbarao Kambhampati, ed.), AAAI Press, volume 1-3, pp. 936-942, 2016. (poster, proceedings-version) (Url: http://www.ijcai.org/Proceedings/16/Papers/137.pdf) [bibtex]
• An Object-Logic Explanation for the Inconsistency in Gödel's Ontological Theory (Extended Abstract, Sister Conferences) (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In KI 2016: Advances in Artificial Intelligence, Proceedings (Malte Helmert, Franz Wotawa, eds.), Springer, LNCS, pp. 244-250, 2016. (Preprint: https://www.researchgate.net/publication/311455987) [bibtex] [doi]

Assessment of the Anderson-Hajek controversy on Gödel’s ontological argument

A formal assessment of Melvin Fitting’s intensional variant of Gödel’s ontological argument (see his 2002 book):

We also formalised Fitting’s intensional variant on the computer, and we assessed it and compared it with the variants of Scott and Anderson:

• Types, Tableaus and Gödel's God in Isabelle/HOL (David Fuenmayor, Christoph Benzmüller), In Archive of Formal Proofs, pp. 1--34, 2017. (Note: verified data publication) [bibtex] [url]
• Can Computers Help to Sharpen our Understanding of Ontological Arguments? (Christoph Benzmüller, David Fuenmayor), In Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science & Spiritual Quest (AISSQ), 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India (Sudipto Gosh, Ramgopal Uppalari, K. Vasudeva Rao, Varun Agarwal, Sushant Sharma, eds.), The Bhaktivedanta Institute, Kolkata, www.binstitute.org, pp. 195-226, 2018. (Preprint: http://doi.org/10.13140/RG.2.2.31921.84323) [bibtex]

The latter paper starts using (modal) ultrafilters as a mathematical tool for the comparison of the different variants.

Ultrafilter-based assessments and simplifications of Gödel’s ontological argument 

Using (modal) ultrafilters, Gödel’s ontological argument can be more deeply studied, and it can be further simplified: 

• Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument (Christoph Benzmüller, David Fuenmayor), In Bulletin of the Section of Logic, Department of Logic, University of Lodz, volume 49, number 2, 2020. (In print, preprint: https://www.researchgate.net/publication/336742445) [bibtex]
• A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument (Christoph Benzmüller), Technical report, CoRR, number arXiv:2001.04701, 2020. (See also: https://www.researchgate.net/publication/338594183) [bibtex] [url]

Further references in which our computer-supported assessments of Gödel’s ontological argument is discussed:

• Universal (Meta-)Logical Reasoning: Recent Successes (Christoph Benzmüller), In Science of Computer Programming, volume 172, pp. 48-62, 2019. (Preprint: http://doi.org/10.13140/RG.2.2.11039.61609/2) [bibtex] [doi]
• Computer Science and Metaphysics: A Cross-Fertilization (Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta), In Open Philosophy (Patrick Grim, ed.), volume 2, pp. 230–251, 2019. [bibtex] [doi]
• Section 3.5. of:  Grim, Patrick and Singer, Daniel, "Computational Philosophy", The Stanford Encyclopedia of Philosophy (Spring 2020 Edition), Edward N. Zalta (ed.).
• Section 4.6 of: Portoraro, Frederic, "Automated Reasoning", The Stanford Encyclopedia of Philosophy (Spring 2019 Edition), Edward N. Zalta (ed.).

Studies of other, related ontological arguments with our technique and tools:

• Analysis of an Ontological Proof Proposed by Leibniz (Matthias Bentert, Christoph Benzmüller, David Streit, Bruno Woltzenlogel Paleo), Chapter in Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G.W. Leibniz (Charles Tandy, ed.), Ria University Press, 2016. (Preprint: https://www.researchgate.net/publication/311456135) [bibtex] [url]
• Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument (David Fuenmayor, Christoph Benzmüller), In Archive of Formal Proofs, pp. 1--19, 2017. (Note: verified data publication) [bibtex] [url]
• A Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument (David Fuenmayor, Christoph Benzmüller), In Journal of Applied Logic - IfCoLoG Journal of Logics and their Applications (special issue on Formal Approaches to the Ontological Argument), volume 5, number 7, pp. 1567-1603, 2018. (To be published also as chapter in the book 'Beyond Faith and Rationality: Essays on Logic, Religion and Philosophy' printed in the Springer book series 'Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures', preprint: https://www.researchgate.net/publication/333804824) [bibtex]

Related pioneering works on computational metaphysics by Ed Zalta and colleagues is mentioned in:

• Section 3.5. of:  Grim, Patrick and Singer, Daniel, "Computational Philosophy", The Stanford Encyclopedia of Philosophy (Spring 2020 Edition), Edward N. Zalta (ed.).