**
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.

#### 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

@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