Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Employing a Restricted Set of Qualitative Relations in Recognizing Plain Sketches Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

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

verfasst von : David Fuenmayor, Christoph Benzmüller

Erschienen in: KI 2017: Advances in Artificial Intelligence

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Improving the Cache-Efficiency of Shortest Path Search
Nächstes Kapitel Real-Time Public Transport Delay Prediction for Situation-Aware Routing
Fußnoten
1
In this paper we work with the Isabelle/HOL proof assistant [22], which explains the chosen abbreviation. Generally, however, the work presented here can be mapped to any other system implementing Church’s simple type theory [13].
 
2
This term was originally coined by Fitelson and Zalta in [14] and describes an emerging, interdisciplinary field aiming at the rigorous formalization and deep logical assessment of philosophical arguments in an automated reasoning environment.
 
3
More loosely related work studied Anselm’s older, non-modal version of the ontological argument directly in Prover9 [23] and PVS [24].
 
4
In contrast to deep semantic embeddings, where the embedded logic is presented as an abstract datatype, our shallow semantic embeddings avoid inductive definitions and maximize the reuse of logical operations from the meta-level. In particular, tedious new binding mechanisms are avoided in our approach.
 
5
Possibilist and actualist quantification can be seen as the semantic counterparts of the concepts of possibilism and actualism in the metaphysics of modality. They relate to natural-language expressions such as ‘there is’, ‘exists’, ‘is actual’, etc.
 
6
The notion of rigid designation was introduced by Kripke in [21], where he discusses its many interesting ramifications in logic and the philosophy of language.
 
7
We prove theorems in Isabelle by using the keyword ‘by’ followed by the name of a proof method. Some methods used here are: simp (term rewriting), blast (tableaus), meson (model elimination), metis (ordered resolution and paramodulation), auto (classical reasoning and term rewriting) and force (exhaustive search trying different tools). In our computer-formalization and assessment of Fitting’s textbook [17], we provide further evidence that our embedded logic works as intended by verifying the book’s theorems and examples.
 
8
We utilize here (counter-)model finder Nitpick [12] for the first time. For the conjectured lemma, Nitpick finds a countermodel (not shown here), i.e. a model satisfying all the axioms which falsifies the given formula.
 
9
The de dicto/de re distinction is used regularly in the philosophy of language for disambiguation of sentences involving intensional contexts.
 
10
Implication can also be proven in the reverse direction (which is not needed for our purposes). Using these definitions, we can derive axioms for the most common modal logics (see also [5]). Thereby we are free to use either the semantic constraints or the related Sahlqvist axioms. Here we provide both versions. In what follows we use the semantic constraints for improved performance.
 
11
To prove T1, the fact is used that positive properties cannot entail negative ones (A2), from which the possible instantiation of positive properties follows. A computer-formalization of Leibniz’s theory of concepts can be found in [1], where the notion of concept containment in contrast to ordinary property entailment is discussed.
 
12
We provide a proof in Isabelle/Isar, a language specifically tailored for writing proofs that are both computer- and human-readable. We refer the reader to [17] for other proofs not shown in this article.
 
13
Essence is defined here (and in Fitting’s variant) in the version of Scott; Gödel’s original version leads to the inconsistency reported in [9, 10].
 
14
In what follows, the ‘ https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-67190-1_9/450601_1_En_9_IEq29_HTML.gif ’ parentheses are used to convert an extensional object into its ‘rigid’ intensional counterpart (e.g. https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-67190-1_9/450601_1_En_9_IEq30_HTML.gif ).
 
15
Fitting’s original treatment in [15] left several details unspecified and we had to fill in the gaps by choosing appropriate formalization variants (see [17] for details).
 
16
Gödel’s original axioms (without Scott’s addition) are proven inconsistent in [9].
 
17
This theorem’s proof could be completely automatized for Gödel’s and Fitting’s variants. For Anderson’s version however, we had to reproduce in Isabelle/HOL the original natural-language proof given by Anderson (see [3], Theorem 2*, p. 296).
 
Literatur
1.
2.
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)
3.
Anderson, C.: Some emendations of Gödel’s ontological proof. Faith Philos. 7(3), 291–303 (1990)CrossRef
4.
5.
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)
6.
Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univers. (Special Issue on Multimodal Logics) 7(1), 7–20 (2013)MathSciNetMATH
7.
Benzmüller, C., Weber, L., Woltzenlogel-Paleo, B.: Computer-assisted analysis of the Anderson-Hájek controversy. Logica Univers. 11(1), 139–151 (2017)MathSciNetCrossRefMATH
8.
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)
9.
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)
10.
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)
11.
Bjørdal, F.: Understanding Gödel’s ontological argument. In: Childers, T. (ed.) The Logica Yearbook 1998. Filosofia (1999)
12.
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 CrossRef
13.
14.
15.
16.
Fitting, M., Mendelsohn, R.: First-Order Modal Logic. Synthese Library, vol. 277. Kluwer, Dordrecht (1998)
17.
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
18.
Gallin, D.: Intensional and Higher-Order Modal Logic. N.-Holland, Amsterdam (1975)MATH
19.
Gödel, K.: Appx. A: notes in Kurt Gödel’s hand. In: [27], pp. 144–145 (2004)
20.
21.
Kripke, S.: Naming and Necessity. Harvard University Press, Cambridge (1980)
22.
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
23.
Oppenheimera, P., Zalta, E.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333–349 (2011)CrossRef
24.
Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop “Fun With Formal Methods”, St. Petersburg, Russia (2013)
25.
Scott, D.: Appx.B: notes in Dana Scott’s hand. In: [27], pp. 145–146 (2004)
26.
Sobel, J.: Gödel’s ontological proof. In: On Being and Saying. Essays for Richard Cartwright, pp. 241–261. MIT Press (1987)
27.
Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge U. Press, Cambridge (2004)
28.
Wisniewski, M., Steen, A., Benzmüller, C.: Einsatz von Theorembeweisern in der Lehre. In: Schwill, A., Lucke, U. (eds.) Hochschuldidaktik der Informatik: 7. Fachtagung 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)
Metadaten
Titel
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
verfasst von
David Fuenmayor
Christoph Benzmüller
Copyright-Jahr
2017
Buch
KI 2017: Advances in Artificial Intelligence

Print ISBN: 978-3-319-67189-5

Electronic ISBN: 978-3-319-67190-1

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-67190-1_9

Premium Partner

    Bildnachweise