Skip to main content
SpringerLink
Log in

Mechanized analysis of Anselm’s modal ontological argument

  • Article
  • Published:
International Journal for Philosophy of Religion Aims and scope Submit manuscript

Abstract

We use a mechanized verification system, PVS, to examine the argument from Anselm’s Proslogion Chapter III, the so-called “Modal Ontological Argument.” We consider several published formalizations for the argument and show they are all essentially similar. Furthermore, we show that the argument is trivial once the modal axioms are taken into account. This work is an illustration of Computational Philiosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. We use \(\lnot \) for negation, \(\wedge \) for conjunction, \(\vee \) for disjunction and \(\supset \) for material implication.

  2. The modal logic with no accessibility relation has the same theorems as one whose accessibility relation is an equivalence.

  3. Hartshorne uses the arrow \(\rightarrow \) to mean strict implication, so his version of Hartshorne (1962, pp. 49–51) is that examined in Sect. 3.5. However, elsewhere, Hartshorne (1965, p. 97) does state “Anselm’s Principle” in the form used by Eder and Ramharter.

  4. Greater automation is possible using modern SMT solvers (Ge and de Moura 2009) but that can be less helpful when, as here, a proof fails and we want to understand why.

  5. The modal formula K is often mentioned, too, and the logic is then sometimes referred to as KT45; however, K is a theorem, true in all modal logics (alternatively, it can be seen to characterize what is a modal logic), so its mention is redundant; furthermore, T and 5 imply 4, so mention of 4 is also redundant.

  6. A relation R is Euclidean if \(\forall u, v, w: R(u, v) \wedge R(u, w) \supset R(v, w)\).

References

  • Adams, R. M. (1971). The logical structure of Anselm’s arguments. The Philosophical Review, 80(1), 28–54.

    Article  Google Scholar 

  • Anselm, S. (1078). Proslogion. In Internet medieval sourcebook. Fordham University (in English, the original is in Latin).

  • Anselm, S. (circa 1079). Apologetic in reply to Gaunilo. In Internet medieval sourcebook. Fordham University (in English, the original is in Latin).

  • Benzmüller, C., & Woltzenlogel-Paleo, B. (2014). Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In ECAI 2014: 21st European conference on artificial intelligence (pp. 93–98). Prague: Czech Republic.

  • Campbell, R. (2018). Rethinking Anselm’s arguments: A vindication of his proof of the existence of god. Leiden: Brill.

    Book  Google Scholar 

  • Campbell, R. (2019). That Anselm’s god exists and Gaunilo’s Island does not. In Considering religions, rights and bioethics: For Max Charlesworth, Sophia studies in cross-cultural philosophy of traditions and cultures, vol. 30 (pp. 115–137). Springer.

  • Cresswell, M. J., & Hughes, G. E. (1996). A new introduction to modal logic. Abingdon: Routledge.

    Google Scholar 

  • Eder, G., & Ramharter, E. (2015). Formal reconstructions of St. Anselm’s ontological argument. Synthese, 192(9), 2795–2825.

    Article  Google Scholar 

  • Garbacz, P. (2012). Prover9’s simplifications explained away. Australasian Journal of Philosophy, 90(3), 585–592.

    Article  Google Scholar 

  • Gaunilo, a Monk of Marmoutier (circa 1079) In behalf of the fool. In Internet medieval sourcebook. Fordham University (in English, the original is in Latin).

  • Ge, Y., & de Moura, L. (2009). Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer-Aided verification, CAV ’09 (pp. 306–320). Grenoble: Springer.

  • Grim, P., & Singer, D. (2020). Computational philosophy. In E. N. Zalta (Ed.), The Stanford encyclopedia of philosophy, spring (2020th ed.). Stanford: Metaphysics Research Lab, Stanford University.

    Google Scholar 

  • Hartshorne, C. (1961). The logic of the ontological argument. The Journal of Philosophy, 58(17), 471–473.

    Article  Google Scholar 

  • Hartshorne, C. (1962). The logic of perfection. La Salle, IL: Open Court.

    Google Scholar 

  • Hartshorne, C. (1965). Anselm’s discovery: A re-examination of the ontological argument for god’s existence. La Salle, IL: Open Court.

    Google Scholar 

  • Jacquette, D. (1997). Conceivability, intensionality, and the logic of Anselm’s modal argument for the existence of god. International Journal for Philosophy of Religion, 42, 163–173.

    Article  Google Scholar 

  • Kane, R. (1984). The modal ontological argument. Mind, 93(371), 336–350.

    Article  Google Scholar 

  • Ladstaetter, K. (2012). On tracy Lupher’s “A logical choice: the role of modal logics in the modal ontological argument”. Southwest Philosophy Review, 28(2), 101–106.

    Article  Google Scholar 

  • Lewis, D. (1970). Anselm and actuality. Noûs, 4(2), 175–188.

    Article  Google Scholar 

  • Malcolm, N. (1960). Anselm’s ontological arguments. The Philosophical Review, 69(1), 41–62.

    Article  Google Scholar 

  • Matthews, G. B. (2005). The ontological argument. In W. E. Mann (Ed.), The blackwell guide to the philosophy of religion (pp. 81–102). Hoboken: Blackwell Publishing.

    Google Scholar 

  • Oppenheimer, P. E., & Zalta, E. N. (2011). A computationally-discovered simplification of the ontological argument. Australasian Journal of Philosophy, 89(2), 333–349.

    Article  Google Scholar 

  • Priest, G. (2002). Beyond the limits of thought. Oxford: Oxford University Press.

    Book  Google Scholar 

  • PVS (constantly updated) PVS home page. http://pvs.csl.sri.com/.

  • Rushby, J. (2013). The ontological argument in PVS. In: Shilov N. (eds) Fun with formal methods. St. Petersburg, Russia, workshop in association with CAV’13.

  • Rushby, J. (2017). PVS embeddings of propositional and quantified modal logic. In Technical reports on, computer science laboratory. Menlo Park, CA: SRI International.

  • Rushby, J. (2018). A mechanically assisted examination of begging the question in Anselm’s ontological argument. Journal of Applied Logics—IFCoLog Journal of Logics and their Applications, 5(7), 1473–1497.

    Google Scholar 

  • Rushby, J. (2019). Mechanized analysis of modal reconstructions of Anselm’s traditional ontological argument. In Technical reports on computer science laboratory. Menlo Park, CA: SRI International.

  • Rushby, J. (2020). A mechanically assisted examination of vacuity and question begging in Anselm’s ontological argument. In R. Silvestre, P. Gocke, J. Y. Beziau, & P. Bilimoria (Eds.), Beyond faith and rationality: Essays on logic, religion and philosophy. Berlin: Springer. to appear.

    Google Scholar 

  • Smith, A. D. (2014). Anselm’s other argument. Cambridge, MA: Harvard University Press.

    Book  Google Scholar 

  • Sobel, J. H. (2003). Logic and Theism: Arguments for and Against Beliefs in God. Cambridge, MA.

  • Wikipedia (retrieved 2019) Standard Translation (of modal logic into first-order logic). https://en.wikipedia.org/wiki/Standard_translation.

Download references

Acknowledgements

The challenging comments of a reviewer helped me improve the paper. I am also grateful to my colleagues Stéphane Graham-Lengrand and N. Shankar for discussions on modal logic and its automation. This work was funded by SRI International and by my retirement fund.

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, 333 Ravenswood Ave, Menlo Park, CA, 94025, USA

    John Rushby

Authors
  1. John Rushby
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Rushby.

Ethics declarations

Conflict of interest

The author declares he has no conflict of interest.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Rushby, J. Mechanized analysis of Anselm’s modal ontological argument. Int J Philos Relig 89, 135–152 (2021). https://doi.org/10.1007/s11153-020-09768-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11153-020-09768-6

Keywords

Search

Navigation