Abstract
A universal reasoning approach based on shallow semantical embeddings of higher-order modal logics into classical higher-order logic is exemplarily employed to analyze several modern variants of the ontological argument on the computer. Several novel findings are reported which contribute to the clarification of a long-standing dispute between Anderson and Hájek. The technology employed in this work, which to some degree realizes Leibniz’s dream of a characteristica universalis and a calculus ratiocinator for solving philosophical controversies, is ready to be fruitfully adopted in larger scale by philosophers.
Similar content being viewed by others
References
Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop “Fun With Formal Methods”. St. Petersburg, Russia (2013)
Oppenheimer, P.E., Zalta, E.N.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333–349 (2011)
Gödel, K.: Appx.A: notes in Kurt Gödel’s hand. In: Sobel, J.H. (ed.) Logic and Theism: Arguments for and Against Beliefs in God, pp. 144–145. Cambridge University Press, Cambridge (2004)
Benzmüller, C., Woltzenlogel Paleo, B.: The Inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016, vol. 1–3, pp. 936-942. AAAI Press (2016). URL: http://www.ijcai.org/Proceedings/16/Papers/137.pdf
Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O’Sullivan, B. (eds.) ECAI 2014, vol. 263. Frontiers in Artificial Intelligence and Applications, pp. 93–98. IOS Press, Amsterdam (2014). doi:10.3233/978-1-61499-419-0-93
Benzmüller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence. arXiv:1308.4526
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015). doi:10.1007/s10817-015-9348-y
Scott, D.: Appx.B: notes in Dana Scott’s hand. In: Sobel, J.H. (ed.) Logic and Theism: Arguments for and Against Beliefs in God, pp. 145–146. Cambridge University Press, Cambridge (2004)
Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)
Sobel, J.H.: Gödel’s ontological proof. In: On Being and Saying. Thomson, JJ. (ed.) Essays for Richard Cartwright, pp. 241–261. MIT Press, Cambridge, Mass (1987)
Hajek, P.: Der Mathematiker und die Frage der Existenz Gottes. In: Buldt, B., Köhler, E., Stöltzner, M., Weibel P., Klein, C., Depauli-Schimanowich-Göttig, W. (eds.) Kurt Gödel. Wahrheit und Beweisbarkeit. ISBN 3-209-03835-X. öbv & hpt, Wien, pp. 325–336 (2001)
Hajek, P.: Magari and others on Gödel’s ontological proof. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra, pp. 125–135. Dekker, New York (1996)
Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer, Dordrecht (2002)
Anderson, C.A.: Some emendations of Gödel’s ontological proof. Faith Philos. 7(3), 291–303 (1990)
Hajek, P.: A new small emendation of Gödel’s ontological proof. Stud. Log. 71(2), 149–164 (2002). doi:10.1023/A:1016583920890
Bjørdal, F.: Understanding Gödel’s ontological argument. In: Childers, T. (ed.) The Logica Yearbook 1998. Institute of Philosophy of the Academy of Sciences of the Czech Republic, Filosofia (1999)
Benzmüller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Log. Univers. 7(1), 7–20 (2013). doi:10.1007/s11787-012-0052-y
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer (2002)
Brown, C.E.: Satallax: an automated higher-order prover. In: Proceedings of lJCAR 2012. LNAI 7364, pp. 111–117. Springer (2012)
Paulson, L.C., Susanto, K.W.: Source-Level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10–13, 2007, Proceedings, vol. 4732. Lecture Notes in Computer Science. Springer, pp. 232–245 (2007)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies/Tactics in Higher Order Logics, NASA Tech. Rep. NASA/CP-2003-212448, pp. 56–68 (2003)
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Proceedings of lTP 2010. LNCS 6172, pp. 131–146. Springer (2010)
Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson–Hajek ontological controversy (presentation abstract). In: Silvestre, R.S., Beziau, J.-Y. (eds.) Handbook of the 1st World Congress on Logic and Religion, pp. 53–54. Joao Pessoa, Brasil (2015)
Magari, R.: Logica e Teofilia. Notizie di Logica 7(4), 11–20 (1988)
Anderson, A.C., Gettings, M.: Gödel 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)
Cocchiarella, N.B.: A completeness theorem in second order modal logic. Theoria 35, 81–103 (1969)
Author information
Authors and Affiliations
Corresponding author
Additional information
This work was supported by German National Research Foundation (DFG) under Grants BE 2501/9-1 and BE 2501/11-1.
Rights and permissions
About this article
Cite this article
Benzmüller, C., Weber, L. & Woltzenlogel Paleo, B. Computer-Assisted Analysis of the Anderson–Hájek Ontological Controversy. Log. Univers. 11, 139–151 (2017). https://doi.org/10.1007/s11787-017-0160-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-017-0160-9
Keywords
- Ontological argument
- Universal reasoning
- Shallow semantical embedding
- Higher-order modal logic
- Classical higher-order logic
- Higher-order automated theorem proving