论文标题
安塞尔姆模态本体论论点的机械化分析
Mechanized Analysis of Anselm's Modal Ontological Argument
论文作者
论文摘要
我们使用机械化的验证系统PVS来检查Anselm的Proslogion第三章的论点，即所谓的“模态本体论论据”。我们考虑了该论点的几种已发表的形式化，并表明它们基本相似。此外，我们表明，一旦考虑了模态公理，该论点是微不足道的。 这项工作是计算理念的例证，此外，还显示了这些方法如何帮助检测和纠正模态推理中的错误。 这是一个较小的更新，并在《国际宗教哲学杂志》上发表的一篇论文，第1卷。 89，第135--152页，2021年4月。
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.
