Mechanized Analysis of Anselm's Modal Ontological Argument

John Rushby

International Journal for Philosophy of Religion. vol. 89, pp. 135--152, April 2021, first published online 4 August 2020.



We use a mechanized verification system, PVS, to examine the argument from Anselm's Proslogion Chapter III, the so-called "Modal Ontological Argument" for the existence of God. 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.

Freely available online and also (likely paywalled) via the journal.
Local copy (with better typesetting and some small addenda), also available as arXiv:2205.08628

PVS dump file: start PVS 7 and do "M-x undump" this file to recreate the specifications and proofs used in the paper.

A Technical Report describes the embedding of modal logics in PVS that is used here.

Note: for those not familiar with these topics, St. Anselm was Archbishop of Canterbury and a contemporary of William the Conqueror. His Ontological Argument is a 3-line proof of the existence of God that has fascinated logicians for nearly 1,000 years.

This paper is concerned with the Proslogion III (modal) form of the Argument. Another recent paper examines the Proslogion II (traditional) Ontological Argument rendered in classical (first- and higher-order) logics, while another extends the analysis to first order modal treatments of that argument. Please email me if you would like to receive a draft copy of any of these papers.

BibTeX Entry

  TITLE = {Mechanized Analysis  of {Anselm's} Modal Ontological Argument},
  AUTHOR = {John Rushby},
  JOURNAL = {International Journal for Philosophy of Religion},
  VOLUME = 89,
  PAGES = {135--152},
  MONTH = apr,
  YEAR = 2021,
  NOTE ={First published online 4 August 2020}

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page