[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.
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Date de publication/diffusion :
septembre 2017
Nom de la manifestation :
40th Annual German Conference on AI
Date de la manifestation :
from 25-09-2017 to 29-09-2017
Manifestation à portée :
International
Titre de l'ouvrage principal :
KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI
Maison d'édition :
Springer International Publishing AG, Cham, Suisse
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)
