×

zbMATH — the first resource for mathematics

Computer-assisted analysis of the Anderson-Hájek ontological controversy. (English) Zbl 1417.03131
Summary: 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.

MSC:
03B35 Mechanization of proofs and logical operations
03B15 Higher-order logic; type theory (MSC2010)
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop “Fun With Formal Methods”. St. Petersburg, Russia (2013)
[2] Oppenheimer, PE; Zalta, EN, A computationally-discovered simplification of the ontological argument, Australas. J. Philos., 89, 333-349, (2011)
[3] Gödel, K; Sobel, JH (ed.), Appx.A: notes in kurt Gödel’s hand, 144-145, (2004), Cambridge
[4] 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 · Zbl 1334.03014
[5] 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 · Zbl 1366.03169
[6] Benzmüller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence. arXiv:1308.4526
[7] 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 · Zbl 1356.68176
[8] Scott, D; Sobel, JH (ed.), Appx.B: notes in dana scott’s hand, 145-146, (2004), Cambridge
[9] Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)
[10] 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)
[11] 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)
[12] 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) · Zbl 0859.03010
[13] Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer, Dordrecht (2002) · Zbl 1038.03001
[14] Anderson, CA, Some emendations of Gödel’s ontological proof, Faith Philos., 7, 291-303, (1990)
[15] Hajek, P, A new small emendation of Gödel’s ontological proof, Stud. Log., 71, 149-164, (2002) · Zbl 1016.03020
[16] 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)
[17] Benzmüller, C; Paulson, LC, Quantified multimodal logics in simple type theory, Log. Univers., 7, 7-20, (2013) · Zbl 1334.03014
[18] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer (2002) · Zbl 0994.68131
[19] Brown, C.E.: Satallax: an automated higher-order prover. In: Proceedings of lJCAR 2012. LNAI 7364, pp. 111-117. Springer (2012) · Zbl 1358.68250
[20] 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) · Zbl 1144.68364
[21] 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)
[22] 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) · Zbl 1291.68326
[23] 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)
[24] Magari, R, Logica e teofilia, Notizie di Logica, 7, 11-20, (1988)
[25] 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) · Zbl 0855.03005
[26] Cocchiarella, NB, A completeness theorem in second order modal logic, Theoria, 35, 81-103, (1969) · Zbl 0205.00601
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.