Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mechanized Analysis of Anselm's Modal Ontological Argument

John Rushby

TL;DR

The paper mechanizes Anselm's Modal Ontological Argument by encoding its propositional modal forms in the PVS verification system. It analyzes five published formalizations (e.g., EderRamharter15, Kane84, Malcolm60, Adams71, and Hartshorne-based treatments) and shows they are essentially equivalent under standard Alethic modal axioms, making the argument trivial when these axioms hold, e.g., via $g \supset \Box g$ and related reasoning. The study demonstrates computational philosophy as a practical tool for validating and detecting errors in modal reasoning and includes an addendum that clarifies the translation from Anselm's informal presentation to formal embeddings. Overall, the work highlights the utility of mechanized reasoning for foundational debates in philosophy and provides a clear, reproducible workflow for modal-logic verification.

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 philosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning. This is a minor update with better typesetting and some small addenda to a paper published in the International Journal for Philosophy of Religion, vol. 89, pp. 135--152, April 2021.

Mechanized Analysis of Anselm's Modal Ontological Argument

TL;DR

The paper mechanizes Anselm's Modal Ontological Argument by encoding its propositional modal forms in the PVS verification system. It analyzes five published formalizations (e.g., EderRamharter15, Kane84, Malcolm60, Adams71, and Hartshorne-based treatments) and shows they are essentially equivalent under standard Alethic modal axioms, making the argument trivial when these axioms hold, e.g., via and related reasoning. The study demonstrates computational philosophy as a practical tool for validating and detecting errors in modal reasoning and includes an addendum that clarifies the translation from Anselm's informal presentation to formal embeddings. Overall, the work highlights the utility of mechanized reasoning for foundational debates in philosophy and provides a clear, reproducible workflow for modal-logic verification.

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 philosophy and, in addition, shows how these methods can help detect and rectify errors in modal reasoning. This is a minor update with better typesetting and some small addenda to a paper published in the International Journal for Philosophy of Religion, vol. 89, pp. 135--152, April 2021.
Paper Structure (3 sections, 2 equations, 1 figure)

This paper contains 3 sections, 2 equations, 1 figure.

Table of Contents

  1. Preamble
  2. Introduction
  3. Propositional Modal Logic in PVS

Figures (1)

  • Figure 1: The Complete Chapter III of St. Anselm's Proslogion Anselm:Proslogion.