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


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.

Update (August 2020):

A recent paper by Oppenheimer and Zalta attempts to rebut my claim that the premise in their treatment that I call Greater1 is question begging.

I regret that my published paper does not illustrate its technical account with an intuitive reason why this is so. To see it, note that Greater1 could be replaced by its contrapositive

  Greater1cp: LEMMA FORALL x: (NOT EXISTS y: y > x) => re?(x)
and then note further that the left side of the implication is just God?(x), so the formula can be rewritten as follows
 Greater1cp_alt: LEMMA FORALL x: God?(x) => re?(x)
and this surely begs the question since it directly states that the other premise implies the conclusion. The original Greater1 is simply an obfuscated version of this and I claim that it inherits its question-begging character. This relationship is inevitable in a proof with only two premises, and I suggest the degree to which it should be considered question begging is related to how flimsy seems the obfuscation, once revealed.

Furthermore, using Greater1cp_alt, the theorems can be proved without opening the definition of God?. Since it is not used, we can attach any interpretation we like to this predicate, including Gaunilo's "most perfect island." Hence, this formalization of the argument is essentially vacuous. The same criticism applies to all the formal treatments considered in the paper. This topic is discussed in more detail in a subsequent paper.

These and some other items are noted in the updated version of this paper available as the PDF below.

Updated PDF

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

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

BibTeX Entry

	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