×

zbMATH — the first resource for mathematics

Variants of Gödel’s ontological proof in a natural deduction calculus. (English) Zbl 1417.03153
Summary: This paper presents detailed formalizations of ontological arguments in a simple modal natural deduction calculus. The first formal proof closely follows the hints in Scott’s manuscript about Gödel’s argument and fills in the gaps, thus verifying its correctness. The second formal proof improves the first one, by relying on the weaker modal logic KB instead of S5 and by avoiding the equality relation. The second proof is also technically shorter than the first one, because it eliminates unnecessary detours and uses Axiom 1 for the positivity of properties only once. The third and fourth proofs formalize, respectively, Anderson’s and Bjørdal’s variants of the ontological argument, which are known to be immune to modal collapse.
MSC:
03B45 Modal logic (including the logic of norms)
03F03 Proof theory, general (including proof-theoretic semantics)
03A05 Philosophical and critical aspects of logic and foundations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Adams, R. M., Introductory note to [Gödel 1970], 1995.
[2] Anderson, CA, Some emendations of Gödel’s ontological proof, Faith and Philosophy, 7, 291-303, (1990)
[3] Anderson, C. A., and M. Gettings, Gödel’s ontological proof revisited, in P. Hájek (ed.), Gödel ’96, Springer, New York, 1996. · Zbl 0855.03005
[4] Bentert, M., C. Benzmüller, D. Streit, and B. WoltzenlogelPaleo, Analysis of an Ontological Proof Proposed by Leibniz. [to appear in] Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G. W. Leibniz, (C. Tandy, ed.), Ria University Press, Palo Alto, CA, 2016.
[5] Benzmüller, C; Brown, C; Kohlhase, M, Higher-order semantics and extensionality, Journal of Symbolic Logic, 69, 1027-1088, (2004) · Zbl 1071.03024
[6] Benzmüller, C., L. Weber, and B. WoltzenlogelPaleo, Computer-assisted analysis of the Anderson-Hájek ontological controversy, in R. S. Silvestre and J.-Y. Béziau (eds.), Handbook of the 1st World Congress on Logic and Religion, Springer, New York, 2015. · Zbl 1071.03024
[7] Benzmüller, C., L. Weber, and B. WoltzenlogelPaleo, Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy. To appear in: Logica Universalis volume 11, issue 1, S. Silvestre and J.-Y. Béziau (eds.), Springer, New York, 2017, pp. 1-11.
[8] Benzmüller, C., and B. WoltzenlogelPaleo, Gödel’s god on the computer, in S. Schulz, G. Sutcliffe, and B. Konev (eds.), Proceedings of the 10th International Workshop on the Implementation of Logics, 2013, pp. 1-2.
[9] Benzmüller, C., and B. WoltzenlogelPaleo, Gödel’s God in Isabelle/HOL. Archive of Formal Proofs, 2013. · JFM 66.1192.06
[10] Benzmüller, C., and B. WoltzenlogelPaleo, On logic embeddings and Gödel’s God, in M. Codescu et al. (eds.), Procedings WADT 2014: Revised Selected Papers of the 22nd International Workshop on Algebraic Development Techniques, Recent Trends in Algebraic Development Techniques, Springer-Verlag, New York, 2014, pp. 3-6.
[11] Benzmüller, C., and B. WoltzenlogelPaleo, On Logic Embeddings and Gödel’s God, in R. Diaconescu et al. (eds.), Preliminary Proceedings of the 22nd International Workshop on Algebraic Development Techniques, 2014, pp. 8-9. · JFM 66.1192.06
[12] Benzmüller, C., and B. WoltzenlogelPaleo, Formalization and automated verification of Gödel’s proof of God’s existence, in J.-Y. Béziau and K. Gan-Krzywoszyńska (eds.), Handbook of the World Congress on the Square of Opposition IV, 2014, pp. 24-25.
[13] Benzmüller, C., and B. WoltzenlogelPaleo, Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers, in T. Schaub et al. (eds.), Proceedings ECAI 2014—21st European Conference on Artificial Intelligence- Including Prestigious Applications of Intelligent Systems (PAIS 2014), 2014, pp. 93-98. · Zbl 1366.03169
[14] Benzmüller, C., and B. WoltzenlogelPaleo, Interacting with modal logics in the coq proof assistant, in L. D. Beklemishev and D. V. Musatov (eds.), Computer Science—Theory and Applications—Proceedings of the 10th International Computer Science Symposium in Russia, CSR 2015, Lecture Notes in Computer Science, Springer, New York, 2015, pp. 398-411. · Zbl 06496834
[15] Benzmüller, C., and B. Woltzenlogel Paleo, Higher-order modal logics: automation and applications, in W. Faber and A. Paschke (eds.), Reasoning Web. Web Logic Rules—11th International Summer School 2015. Tutorial Lectures, Lecture Notes in Computer Science, Springer, New York, 2015, pp. 32-74. · Zbl 1358.68273
[16] Benzmüller, C., and B. WoltzenlogelPaleo, Experiments in Computational Metaphysics: Gödel’s Proof of God’s Existence, in S. C. Mishra, S. Ghosh, and V. Agarwal (eds.), Science and Spiritual Quest: Proceedings of the 9th All India Students’ Conference on Science and Spiritual Quest, vol. 9, Bhaktivedanta Institute, Berkeley, 2015, pp. 23-40.
[17] Benzmüller, C., and B. WoltzenlogelPaleo, The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics, in S. Kambhampati (ed.), Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence—IJCAI, AAAI Press, Menlo Park, CA, 2016.
[18] Benzmüller, C., and B. WoltzenlogelPaleo, The Modal Collapse as a Collapse of the Modal Square of Opposition, in J.-Y. Béziau and G. Basti (eds.), Studies in Universal Logic. The Square of Opposition: A Cornerstone of Thought, Springer, New York, 2016, pp. 1-7.
[19] Bjørdal, F., Understanding Gödel’s ontological argument, in T. Childers (ed.), The Logica Yearbook 1998, Filosofia, Praha, 1999, pp. 214-217.
[20] Blackburn, P., M. deRijke, and Y. Venema. Modal Logic, Cambridge, 2001. · Zbl 0988.03006
[21] Church, A, ., A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 56-68, (1940) · JFM 66.1192.06
[22] Fitting, M., and R. Mendelsohn, First-Order Modal Logic, Synthese Library, vol. 277, Kluwer Academic Publishers, Dordrecht, 1998. · Zbl 1025.03001
[23] Fitting, M., Types, Tableaus, and Gödel’s God, Kluwer Academic Publishers, Dordrecht, 2002. · Zbl 1038.03001
[24] Fuhrmann, A., Existenz und Notwendigkeit—Kurt Gödel’s Axiomatische Theologie, in E. J. Olsson, P. Schröder-Heister, and W. Spohn (eds.), Logik in der Philosophie, Synchr.-Wissenschafts-Verlag, Söochtenau, 2005, pp. 349-374.
[25] Gabbay, D., Labelled Deductive Systems: Volume I, Oxford Science Publications, New York, 1996. · Zbl 0858.03004
[26] Gödel, K., Ontological proof, in S. Feferman et al. (eds.), Kurt Gödel Collected Works, vol. III, pp. 403-404, 139, 145 or Appendix A. Notes in Kurt Gödel’s hand in [Sobel 2001].
[27] HÁJEK, P., Magari and others on Gödel’s ontological proof, in A. Ursini et al. (eds.), Logic and Logical Algebra, Marcel Dekker, New York, 1996, pp. 125-136. · Zbl 0859.03010
[28] Koons, R, Sobel on Gödel’s ontological proof, Philosophia Christi, 2, 235-248, (2006)
[29] Magari, R., Logica e Teofilia. In: Notizie di Logica VII.4. 1988.
[30] Muskens, R., Higher order modal logic, in P. Blackburn, J. F. A. K. van Benthem, and F. Wolter (eds.), Handbook of Modal Logic, Studies in Logic and Practical Reasoning, Elsevier, Dordrecht, 2006, pp. 621-653.
[31] Nipkow, T., L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS, Springer, New York, 2002. · Zbl 0994.68131
[32] Oppenheimer, P., and E. Zalta, A computationally-discovered simplification of the ontological argument, Australasian Journal of Philosophy 89(2):333-349, 2011.
[33] Paulin-Mohring, C., Introduction to the calculus of inductive constructions, in D. Delahaye and B. Woltzenlogel Paleo (eds.), All about Proofs, Proofs for All, Mathematical Logic and Foundations, College Publications, London, 2015.
[34] Prawitz, D., Natural Deduction: A Proof-theoretical Study, Dover Publications, Mineola, NY, 2006 (1st ed. 1965). · Zbl 0173.00205
[35] Rushby, J., The Ontological Argument in PVS, in N. Shilov (ed.), Proceedings of CAV Workshop “Fun with Formal Methods”, St. Petersburg, 2013.
[36] Scott, D., 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, 2004, pp. 145-146.
[37] Sobel, J. H., Gödel’s ontological proof, in J. J. Thompson (ed.), On Being and Saying: Essays for Richard Cartwright, MIT Press, Cambridge, 1987.
[38] Sobel, J. H., Logic and Theism: Arguments for and Against Beliefs in God, Cambridge University Press, Cambridge, 2001.
[39] Thiele, R., Hilbert’s twenty-fourth problem, American Mathematical Monthly, January 2003. · Zbl 1031.01011
[40] Wang, H., A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge, 1996.
[41] WoltzenlogelPaleo, B., Automated verification and reconstruction of Gödel’s proof of God’s existence, Journal of the Austrian Computer Society 38:4-6, 2013.
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.