Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument

Christoph Benzmüller; David Fuenmayor

doi:10.18778/0138-0680.2020.08

Authors

Christoph Benzmüller Freie Universität Berlin, Institute of Computer Science; University of Luxembourg, Faculty of Science, Technology, and Communication
David Fuenmayor Freie Universität Berlin, Institute of Computer Science

DOI:

https://doi.org/10.18778/0138-0680.2020.08

Keywords:

computational metaphysics, ontological argument, higher-order modal logic, higher-order logic, automated reasoning, modal ultrafilters

Abstract

Three variants of Kurt Gödel's ontological argument, proposed by Dana Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously assessed on the computer. In contrast to Scott's version of Gödel's argument the two variants contributed by Anderson and Fitting avoid modal collapse. Although they appear quite different on a cursory reading they are in fact closely related. This has been revealed in the computer-supported formal analysis presented in this article. Key to our formal analysis is the utilization of suitably adapted notions of (modal) ultrafilters, and a careful distinction between extensions and intensions of positive properties.

References

[1] C. A. Anderson, Some emendations of Gödel's ontological proof, Faith and Philosophy, vol. 7(3) (1990), pp. 291–303.
Google Scholar

[2] C. A. Anderson, M. Gettings, Gödel's ontological proof revisited, [in:] Gödel'96: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6, pp. 167–172, Springer (1996).
Google Scholar

[3] C. Benzmüller, Computational metaphysics: New insights on Gödel's ontological argument and modal collapse, [in:] In S. Kovač, K. Świętorzecka (eds.), Formal Methods and Science in Philosophy III, Informal Proceedings, Dubrovnik, Croatia (2019), pp. 3–4.
Google Scholar

[4] C. Benzmüller, Universal (meta-)logical reasoning: Recent successes, Science of Computer Programming, vol. 172 (2019), pp. 48–62.
Google Scholar DOI: https://doi.org/10.1016/j.scico.2018.10.008

[5] C. Benzmüller, P. Andrews, Church's type theory, [in:] E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University (2019), pp. 1–62 (in pdf version).
Google Scholar

[6] C. Benzmüller, D. Fuenmayor, Can computers help to sharpen our understanding of ontological arguments?, [in:] S. Gosh, R. Uppalari, K. V. Rao, V. Agarwal, S. Sharma (eds.), Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science & Spiritual Quest (AISSQ), 6–7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India, The Bhaktivedanta Institute, Kolkata (2018), pp. 95–226.
Google Scholar

[7] C. Benzmüller, L. Paulson, Quantified multimodal logics in simple type theory, Logica Universalis, vol. 7(1) (2013), pp. 7–20.
Google Scholar

[8] C. Benzmüller, N. Sultana, L. C. Paulson, F. Theiß, The higher-order prover LEO-II, Journal of Automated Reasoning, vol. 55(4) (2015), pp. 389–404.
Google Scholar

[9] C. Benzmüller, B. Woltzenlogel Paleo, Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers, [in:] T. Schaub, G. Friedrich, B. O'Sullivan (eds.), ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263 (2014), pp. 93–98.
Google Scholar

[10] C. Benzmüller, B. Woltzenlogel Paleo, Interacting with modal logics in the Coq proof assistant, [in:] L. D. Beklemishev, D. V. Musatov (eds.), Computer Science – Theory and Applications – 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13–17, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9139 (2015), pp. 398–411.
Google Scholar

[11] C. Benzmüller, B. Woltzenlogel Paleo, The inconsistency in Gödel's ontological argument: A success story for AI in metaphysics, [in:] S. Kambhampati (ed.), IJCAI 2016, vol. 1–3, AAAI Press (2016), pp. 936–942.
Google Scholar

[12] C. Benzmüller, B. Woltzenlogel Paleo, An object-logic explanation for the inconsistency in Gödel's ontological theory (extended abstract, sister conferences), [in:] M. Helmert, F. Wotawa (eds.), KI 2016: Advances in Artificial Intelligence, Proceedings, Lecture Notes in Computer Science, vol. 6172, Springer, Berlin (2016), pp. 244–250.
Google Scholar

[13] J. C. Blanchette, S. Böhme, L. C. Paulson, Extending Sledgehammer with SMT solvers, Journal of Automated Reasoning, vol. 51(1) (2013), pp. 109–128.
Google Scholar

[14] J. C. Blanchette, Tobias Nipkow, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, [in:] M. Kaufmann, L. C. Paulson (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, Springer, Berlin (2010), pp. 131–146.
Google Scholar

[15] S. Burris, H.P. Sankappanavar, A course in universal algebra, Springer, New York, Heidelberg, Berlin (2012).
Google Scholar

[16] M. Fitting, Types, Tableaus, and Gödel's God, Kluwer, Dordrecht (2002).
Google Scholar DOI: https://doi.org/10.1007/978-94-010-0411-4

[17] D. Fuenmayor, C. Benzmüller, Automating emendations of the ontological argument in intensional higher-order modal logic, [in:] KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI, Dortmund, Germany, September 25–29, 2017, Proceedings, Lecture Notes in Artificial Intelligence, vol. 10505, Springer (2017) pp. 114–127.
Google Scholar

[18] D. Fuenmayor, C. Benzmüller, Types, Tableaus and Gödel's God in Isabelle/HOL, Archive of Formal Proofs (2017), pp. 1–34. Note: verified data publication.
Google Scholar

[19] J. Garson, Modal logic, [in:] E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University (2018).
Google Scholar

[20] K. Gödel, Appendix A. Notes in Kurt Gödel's Hand, [in:] J. H. Sobel (ed.), Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (1970), pp. 144–145.
Google Scholar

[21] P. Hájek, Magari and others on Gödel's ontological proof, [in:] A. Ursini, P. Agliano (eds.), Logic and algebra, Dekker, New York (1996), pp. 125–135.
Google Scholar

[22] P. Hájek, Der Mathematiker und die Frage der Existenz Gottes, [in:] B. Buldt et al. (eds.), Kurt Gödel. Wahrheit und Beweisbarkeit, obv & hpt Verlagsgesellschaft mbH, Wien (2001), pp. 325–336.
Google Scholar

[23] P. Hájek, A new small emendation of Gödel's ontological proof, Studia Logica, vol. 71(2) (2002), pp. 149–164.
Google Scholar

[24] D. Kirchner, C. Benzmüller, E. N. Zalta, Computer science and metaphysics: A cross-fertilization, Open Philosophy, vol. 2 (2019), pp. 230–251.
Google Scholar DOI: https://doi.org/10.1515/opphil-2019-0015

[25] S. Kovač, Modal collapse in Gödel's ontological proof, [in:] M. Szatkowski (ed.), Ontological Proofs Today, Ontos Verlag, Heusenstamm (2012), pp. 50–323.
Google Scholar

[26] E. J. Lowe, A modal version of the ontological argument, [in:] J.P. Moreland, K. A. Sweis, C. V. Meister (eds.), Debating Christian Theism, chapter 4, Oxford University Press, Oxford (2013), pp. 61–71.
Google Scholar

[27] T. Nipkow, L. C. Paulson, M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002).
Google Scholar

[28] D. S. Scott, Appendix B: Notes in Dana Scott's Hand, [in:] J. H. Sobel (ed.), Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (1972), pp. 145–146.
Google Scholar

[29] J. H. Sobel, Gödel's ontological proof, [in:] J. J. Tomson (ed.), On Being and Saying. Essays for Richard Cartwright, MIT Press, Cambridge, Mass. (1987), pp. 241–261.
Google Scholar

[30] J. H. Sobel, Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (2004).
Google Scholar

[31] K. Świętorzecka, Identity or equality of Gödelian God, draft paper, private communication, May 2019.
Google Scholar