Skip to main content
SpringerLink
Log in
SpringerLink
Log in

On Logic Embeddings and Gödel’s God

  • Conference paper
  • First Online:
Recent Trends in Algebraic Development Techniques (WADT 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9463))

Included in the following conference series:

Abstract

We have applied an elegant and flexible logic embedding approach to verify and automate a prominent philosophical argument: the ontological argument for the existence of God. In our ongoing computer-assisted study, higher-order automated reasoning tools have made some interesting observations, some of which were previously unknown.

C. Benzmüller—This work has been supported by the German Research Foundation DFG under grants BE2501/9-1,2 and BE2501/11-1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    Some Notes on THF, which is a concrete syntax for HOL: $i and $o represent the HOL base types i and o (Booleans). $i>$o encodes a function (predicate) type. Predicate application as in A(X, W) is encoded as ((A@X)@W) or simply as (A@X@W), i.e., function/predicate application is represented by @; universal quantification and \(\lambda \)-abstraction as in \(\lambda {A}_{i\rightarrow o} \forall {W_i} (A\,W)\) and are represented as in \(\mathtt{\hat{}}\)[X:$i>$o]:![W:$i]:(A@W); comments begin with %.

References

  1. Anderson, C.A.: Some emendations of Gödel’s ontological proof. Faith Philos. 7(3), 291–303 (1990)

    Article  Google Scholar 

  2. Anderson, C.A., Gettings, M.: Gödel ontological proof revisited. In: Gödel’96: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6, pages 167–172. Springer, (1996)

    Google Scholar 

  3. Benzmüller, C.: Automating quantified conditional logics in HOL. In: Proceedings of IJCAI 2013, pp. 746–753, Beijing, China (2013)

    Google Scholar 

  4. Benzmüller, C.: A top-down approach to combining logics. In: Proceedings of ICAART 2013, pp. 346–351. SciTePress Digital Library, Barcelona, Spain (2013)

    Google Scholar 

  5. Benzmüller, C., Paleo, B.W.: Gödel’s God in Isabelle/HOL. Arch. Formal Proofs (2013)

    Google Scholar 

  6. Benzmüller, C., Paleo, B.W.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: ECAI 2014. Frontiers in AI and Applications, vol. 263, pp. 163–168. IOS Press (2014)

    Google Scholar 

  7. Benzmüller, C., Weber, L., Paleo, B.W.: Computer-assisted analysis of the Anderson-Hájek ontological controversy. Handbook of the 1st World Congress on Logic and Religion, João Pessoa, Brazil (2015)

    Google Scholar 

  8. Benzmüller, C., Woltzenlogel Paleo, B.: Interacting with modal logics in the coq proof assistant. In: Beklemishev, L.D. (ed.) CSR 2015. LNCS, vol. 9139, pp. 398–411. Springer, Heidelberg (2015)

    MATH  Google Scholar 

  9. Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univers. (Spec. Issue Multimodal Logics) 7(1), 7–20 (2013)

    Article  MathSciNet  Google Scholar 

  10. Benzmüller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Bjørdal, F.: Understanding Gödel’s ontological argument. In: The Logica Yearbook 1998. Filosofia (1999)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  13. Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111–117. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68 (1940)

    Article  MathSciNet  Google Scholar 

  15. Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Synthese Library, vol. 277. Kluwer, Dordrecht (1998)

    Book  Google Scholar 

  16. Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer, Norwell (2002)

    Book  Google Scholar 

  17. Fuhrmann, A.: Existenz und Notwendigkeit – Kurt Gödels axiomatische Theologie. In: Logik in der Philosophie, Heidelberg (Synchron) (2005)

    Google Scholar 

  18. Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996)

    MATH  Google Scholar 

  19. Gödel, K.: Appx.A: notes in Kurt Gödel’s hand. In: [25], pp. 144–145 (2004)

    Google Scholar 

  20. Hajek, P.: A new small emendation of Gödel’s ontological proof. Stud. Logica: Int. J. Symbolic Logic 71(2), 149–164 (2002)

    Article  MathSciNet  Google Scholar 

  21. Hajek, P.: Ontological proofs of existence and non-existence. Stud. Logica: Int. J. Symbolic Logic 90(2), 257–262 (2008)

    Article  MathSciNet  Google Scholar 

  22. Oppenheimera, P.E., Zalta, E.N.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333–349 (2011)

    Article  Google Scholar 

  23. Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop “Fun With Formal Methods”, St. Petersburg, Russia (2013)

    Google Scholar 

  24. Scott, D.: Appx.B: notes in Dana Scott’s hand. In: [25], pp. 145–146 (2004)

    Google Scholar 

  25. Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)

    Google Scholar 

  26. Stalnaker, R.C.: A theory of conditionals. In: Rescher, N. (ed.) Studies in Logical Theory, pp. 98–112. Blackwell, Oxford (1968)

    Google Scholar 

  27. Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1–27 (2010)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Freie Universität Berlin, Berlin, Germany

    Christoph Benzmüller

  2. Vienna Technical University, Vienna, Austria

    Bruno Woltzenlogel Paleo

Authors
  1. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Woltzenlogel Paleo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christoph Benzmüller .

Editor information

Editors and Affiliations

  1. Otto-von-Guericke-Universität Magedeburg , Magdeburg, Germany

    Mihai Codescu

  2. Simion Stoilow Institute of Mathematics of the Romanian Academy, Bucharest, Romania

    Răzvan Diaconescu

  3. Royal Holloway University of London, Egham, UK

    Ionuț Țuțu

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Benzmüller, C., Paleo, B.W. (2015). On Logic Embeddings and Gödel’s God. In: Codescu, M., Diaconescu, R., Țuțu, I. (eds) Recent Trends in Algebraic Development Techniques. WADT 2015. Lecture Notes in Computer Science(), vol 9463. Springer, Cham. https://doi.org/10.1007/978-3-319-28114-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28114-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28113-1

  • Online ISBN: 978-3-319-28114-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation