Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. (English) Zbl 1461.03021

Summary: 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.


03B45 Modal logic (including the logic of norms)
03B35 Mechanization of proofs and logical operations
03-08 Computational methods for problems pertaining to mathematical logic and foundations
Full Text: DOI arXiv


[1] C. A. Anderson, Some emendations of Gödel’s ontological proof, Faith and Philosophy, vol. 7(3) (1990), pp. 291-303.
[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). · Zbl 0855.03005
[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.
[4] C. Benzmüller, Universal (meta-)logical reasoning: Recent successes, Science of Computer Programming, vol. 172 (2019), pp. 48-62.
[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).
[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.
[7] C. Benzmüller, L. Paulson, Quantified multimodal logics in simple type theory, Logica Universalis, vol. 7(1) (2013), pp. 7-20. · Zbl 1334.03014
[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. · Zbl 1356.68176
[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. · Zbl 1366.03169
[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. · Zbl 1465.03051
[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.
[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. · Zbl 1370.68258
[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. · Zbl 1314.68272
[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. · Zbl 1291.68326
[15] S. Burris, H.P. Sankappanavar, A course in universal algebra, Springer, New York, Heidelberg, Berlin (2012). · Zbl 0478.08001
[16] M. Fitting, Types, Tableaus, and Gödel’s God, Kluwer, Dordrecht (2002). · Zbl 1038.03001
[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.
[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.
[19] J. Garson, Modal logic, [in:] E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University (2018). · Zbl 1109.03001
[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.
[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. · Zbl 0859.03010
[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.
[23] P. Hájek, A new small emendation of Gödel’s ontological proof, Studia Logica, vol. 71(2) (2002), pp. 149-164. · Zbl 1016.03020
[24] D. Kirchner, C. Benzmüller, E. N. Zalta, Computer science and metaphysics: A cross-fertilization, Open Philosophy, vol. 2 (2019), pp. 230-251.
[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.
[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.
[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). · Zbl 0994.68131
[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.
[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.
[30] J. H. Sobel, Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (2004).
[31] K.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.