A Mechanically Assisted Examination of Begging the Question in Anselm's Ontological Argument

Note: this paper is now obsolete and is replaced by this extended version

John Rushby

Journal of Applied Logics---IFCoLog Journal of Logics and their Applications, Special Issue on Formal Approaches to the Ontological Argument, Vol. 5 No. 7, October 2018, pp. 1473--1496

Abstract

I use mechanized verification to examine several first- and higher-order formalizations of Anselm's Ontological Argument against the charge of begging the question. I propose three different criteria for a premise to beg the question in fully formal proofs and find that one or another applies to all the formalizations examined. My purpose is to demonstrate that mechanized verification provides an effective and reliable technique to perform these analyses; readers may decide whether the forms of question begging so identified affect their interest in the Argument or its various formalizations.

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.

Note: this paper is now obsolete and is replaced by this extended version

journal site (original paper and complete issue available here).

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

BibTeX Entry


@article{Rushby18:begging,
	AUTHOR = {John Rushby},
	TITLE = {A Mechanically Assisted Examination of Begging the Question
		in {Anselm's Ontological Argument}},
	JOURNAL = {Journal of Applied Logics---IFCoLog Journal of Logics
		and their Applications},
	YEAR = 2018,
	VOLUME = 5,
	NUMBER = 7,
	PAGES = {1473--1496},
	MONTH = oct
}
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