Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic

Fuenmayor, David; Benzmüller, Christoph

doi:10.1007/978-3-319-67190-1_9

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic

Fuenmayor, David; Benzmüller, Christoph

2017 • In KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI

Peer reviewed

Permalink
https://hdl.handle.net/10993/33693

DOI
10.1007/978-3-319-67190-1_9

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

C65.pdf

Author preprint (493.52 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Ontological Argument; Intensional Higher-Order Modal Logic; Formal Methods; Automated Reasoning

Abstract :

[en] A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work.

Disciplines :

Computer science
Religion & theology
Philosophy & ethics

Author, co-author :

Fuenmayor, David

Benzmüller, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

External co-authors :

yes

Language :

English

Title :

Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic

Publication date :

September 2017

Event name :

40th Annual German Conference on AI

Event date :

from 25-09-2017 to 29-09-2017

Audience :

International

Main work title :

KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI

Publisher :

Springer International Publishing AG, Cham, Switzerland

ISBN/EAN :

978-3-319-67189-5

Peer reviewed :

Peer reviewed

Focus Area :

Computational Sciences

Additional URL :

http://christoph-benzmueller.de/papers/C65.pdf

Available on ORBilu :

since 14 December 2017

Statistics

Number of views

127 (4 by Unilu)

Number of downloads

166 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

Alama, J., Oppenheimer, P.E., Zalta, E.N.: Automating Leibniz’s theory of concepts. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 73–97. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6 4
Anderson, A., Gettings, M.: Gödel ontological proof revisited. In: Hajek, P. (ed.) Gödel 1996: Logical Foundations of Mathematics, Computer Science, and Physics. Lecture Notes in Logic, vol. 6, pp. 167–172. Springer (2001)
Anderson, C.: Some emendations of Gödel’s ontological proof. Faith Philos. 7(3), 291–303 (1990)
Benzmüller, C.: Universal reasoning, rational argumentation and human-machine interaction. arXiv (2017). http://arxiv.org/abs/1703.09620
Benzmüller, C., Claus, M., Sultana, N.: Systematic verification of the modal logic cube in Isabelle/HOL. In: Kaliszyk, C., Paskevich, A. (eds.) PxTP 2015, EPTCS, Berlin, Germany, vol. 186, pp. 27–41 (2015)
Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univers. (Special Issue on Multimodal Logics) 7(1), 7–20 (2013)
Benzmüller, C., Weber, L., Woltzenlogel-Paleo, B.: Computer-assisted analysis of the Anderson-Hájek controversy. Logica Univers. 11(1), 139–151 (2017)
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. Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93–98. IOS Press (2014)
Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics. In: IJCAI 2016 (2016)
Benzmüller, C., Woltzenlogel Paleo, B.: An object-logic explanation for the inconsistency in Gödel’s ontological theory (extended abstract). In: Helmert, M., Wotawa, F. (eds.) KI 2016: Advances in Artificial Intelligence. LNAI, vol. 9904, pp. 205–244. Springer, Berlin (2016)
Bjørdal, F.: Understanding Gödel’s ontological argument. In: Childers, T. (ed.) The Logica Yearbook 1998. Filosofia (1999)
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5 11
Church, A.: A formulation of the simple theory of types. J. Symbol. Logic 5, 56–68 (1940)
Fitelson, B., Zalta, E.N.: Steps toward a computational metaphysics. J. Philos. Logic 36(2), 227–247 (2007)
Fitting, M.: Types, Tableaus and Gödel’s God. Kluwer, Dordrecht (2002)
Fitting, M., Mendelsohn, R.: First-Order Modal Logic. Synthese Library, vol. 277. Kluwer, Dordrecht (1998)
Fuenmayor, D., Benzmüller, C.: Types, Tableaus and Gödel’s God in Isabelle/HOL. Archive of Formal Proofs (2017). Formally verified with Isabelle/HOL
Gallin, D.: Intensional and Higher-Order Modal Logic. N.-Holland, Amsterdam (1975)
Gödel, K.: Appx. A: notes in Kurt Gödel’s hand. In: pp. 144–145 (2004)
Hájek, P.: A new small emendation of Gödel’s ontological proof. Studia Logica 71(2), 149–164 (2002)
Kripke, S.: Naming and Necessity. Harvard University Press, Cambridge (1980)
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Oppenheimera, P., Zalta, E.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333–349 (2011)
Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop “Fun With Formal Methods”, St. Petersburg, Russia (2013)
Scott, D.: Appx.B: notes in Dana Scott’s hand. pp. 145–146 (2004)
Sobel, J.: Gödel’s ontological proof. In: On Being and Saying. Essays for Richard Cartwright, pp. 241–261. MIT Press (1987)
Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge U. Press, Cambridge (2004)
Wisniewski, M., Steen, A., Benzmüller, C.: Einsatz von Theorembeweisern in der Lehre. In: Schwill, A., Lucke, U. (eds.) Hochschuldidaktik der Informatik: 7. Fach-tagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik, 13–14 September 2016 an der Universität Potsdam, Commentarii informaticae didacticae (CID), Potsdam, Germany (2016)