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

Christoph Benzmüller; David Fuenmayor

Bulletin of the Section of Logic (2020)

  • Volume: 49, Issue: 2
  • ISSN: 0138-0680

Abstract

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

How to cite

top

Christoph Benzmüller, and David Fuenmayor. "Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument." Bulletin of the Section of Logic 49.2 (2020): null. <http://eudml.org/doc/295554>.

@article{ChristophBenzmüller2020,
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.},
author = {Christoph Benzmüller, David Fuenmayor},
journal = {Bulletin of the Section of Logic},
keywords = {computational metaphysics; ontological argument; higher-order modal logic; higher-order logic; automated reasoning; modal ultrafilters},
language = {eng},
number = {2},
pages = {null},
title = {Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument},
url = {http://eudml.org/doc/295554},
volume = {49},
year = {2020},
}

TY - JOUR
AU - Christoph Benzmüller
AU - David Fuenmayor
TI - Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument
JO - Bulletin of the Section of Logic
PY - 2020
VL - 49
IS - 2
SP - null
AB - 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.
LA - eng
KW - computational metaphysics; ontological argument; higher-order modal logic; higher-order logic; automated reasoning; modal ultrafilters
UR - http://eudml.org/doc/295554
ER -

References

top
  1. [1] C. A. Anderson, Some emendations of Gödel's ontological proof, Faith and Philosophy, vol. 7(3) (1990), pp. 291–303. 
  2. [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). 
  3. [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. [4] C. Benzmüller, Universal (meta-)logical reasoning: Recent successes, Science of Computer Programming, vol. 172 (2019), pp. 48–62. 
  5. [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. [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. [7] C. Benzmüller, L. Paulson, Quantified multimodal logics in simple type theory, Logica Universalis, vol. 7(1) (2013), pp. 7–20. 
  8. [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. 
  9. [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. 
  10. [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. 
  11. [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. [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. 
  13. [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. 
  14. [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. 
  15. [15] S. Burris, H.P. Sankappanavar, A course in universal algebra, Springer, New York, Heidelberg, Berlin (2012). 
  16. [16] M. Fitting, Types, Tableaus, and Gödel's God, Kluwer, Dordrecht (2002). 
  17. [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. [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. [19] J. Garson, Modal logic, [in:] E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University (2018). 
  20. [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. [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. 
  22. [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. [23] P. Hájek, A new small emendation of Gödel's ontological proof, Studia Logica, vol. 71(2) (2002), pp. 149–164. 
  24. [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. [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. [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. [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). 
  28. [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. [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. [30] J. H. Sobel, Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (2004). 
  31. [31] K. Świętorzecka, Identity or equality of Gödelian God, draft paper, private communication, May 2019. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.