Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument
| dc.contributor.author | Benzmüller, Christoph | |
| dc.contributor.author | Fuenmayor, David | |
| dc.date.accessioned | 2021-05-11T06:25:08Z | |
| dc.date.available | 2021-05-11T06:25:08Z | |
| dc.date.issued | 2020-06-30 | |
| dc.identifier.issn | 0138-0680 | |
| dc.identifier.uri | http://hdl.handle.net/11089/35468 | |
| dc.description.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. | en |
| dc.language.iso | en | |
| dc.publisher | Wydawnictwo Uniwersytetu Łódzkiego | pl |
| dc.relation.ispartofseries | Bulletin of the Section of Logic;2 | en |
| dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0 | |
| dc.subject | computational metaphysics | en |
| dc.subject | ontological argument | en |
| dc.subject | higher-order modal logic | en |
| dc.subject | higher-order logic | en |
| dc.subject | automated reasoning | en |
| dc.subject | modal ultrafilters | en |
| dc.title | Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument | en |
| dc.type | Other | |
| dc.page.number | 127–148 | |
| dc.contributor.authorAffiliation | Benzmüller, Christoph - Freie Universität Berlin, Institute of Computer Science; University of Luxembourg, Faculty of Science, Technology, and Communication | en |
| dc.contributor.authorAffiliation | Fuenmayor, David - Freie Universität Berlin, Institute of Computer Science | en |
| dc.identifier.eissn | 2449-836X | |
| dc.references | [1] C. A. Anderson, Some emendations of Gödel's ontological proof, Faith and Philosophy, vol. 7(3) (1990), pp. 291–303. | en |
| dc.references | [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). | en |
| dc.references | [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. | en |
| dc.references | [4] C. Benzmüller, Universal (meta-)logical reasoning: Recent successes, Science of Computer Programming, vol. 172 (2019), pp. 48–62. | en |
| dc.references | [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). | en |
| dc.references | [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. | en |
| dc.references | [7] C. Benzmüller, L. Paulson, Quantified multimodal logics in simple type theory, Logica Universalis, vol. 7(1) (2013), pp. 7–20. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [15] S. Burris, H.P. Sankappanavar, A course in universal algebra, Springer, New York, Heidelberg, Berlin (2012). | en |
| dc.references | [16] M. Fitting, Types, Tableaus, and Gödel's God, Kluwer, Dordrecht (2002). | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [19] J. Garson, Modal logic, [in:] E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University (2018). | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [23] P. Hájek, A new small emendation of Gödel's ontological proof, Studia Logica, vol. 71(2) (2002), pp. 149–164. | en |
| dc.references | [24] D. Kirchner, C. Benzmüller, E. N. Zalta, Computer science and metaphysics: A cross-fertilization, Open Philosophy, vol. 2 (2019), pp. 230–251. | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [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). | en |
| dc.references | [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. | en |
| dc.references | [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. | en |
| dc.references | [30] J. H. Sobel, Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge (2004). | en |
| dc.references | [31] K. Świętorzecka, Identity or equality of Gödelian God, draft paper, private communication, May 2019. | en |
| dc.contributor.authorEmail | Benzmüller, Christoph - c.benzmueller@gmail.com | |
| dc.contributor.authorEmail | Fuenmayor, David - david.fuenmayor@fu-berlin.de | |
| dc.identifier.doi | 10.18778/0138-0680.2020.08 | |
| dc.relation.volume | 49 |
Pliki tej pozycji
Pozycja umieszczona jest w następujących kolekcjach
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako http://creativecommons.org/licenses/by-nc-nd/4.0