Anselm’s Argument in First-Order Logic

2021-01-28, updated 2024-03-01 next - previous

In the language of first-order logic, I provide in this note a proof in natural deduction that translates Anselm’s ontological argument (i.e. his a priori proof of the existence of God).

Of course, such formal translations of Anselm’s argument have already be given by many others (for example, Tennant [1]), but the proof below is maybe the simplest, because it is based on the most elegant version of Anselm’s argument, that of Gaunilo [2]:

Someone who either doubts or denies that there is any such nature as that than which nothing greater can be thought is told that its existence is proved in the following way. First, the very person who denies or entertains doubts about this being has it in his understanding, since when he hears it spoken of he understands what is said. Further, what he understands must exist in reality as well and not only in the understanding. The argument for this claim goes like this: to exist in reality is greater than to exist only in the understanding. Now, if that being exists only in the understanding, then whatever also exists in reality is greater than it. Thus, that which is greater than everything else will be less than something and not greater than everything else, which is of course a contradiction. And so that which is greater than everything else, which has already been proved to exist in the understanding, must exist not only in the understanding but also in reality, since otherwise it could not be greater than everything else.

As Anselm pointed out to Gaunilo, the expression “greater than everything else” must be replaced by “what nothing greater can be thought of”, but this correction does not affect the validity of the argument. Here is the formal lexicon to translate this one:

• \(x > y\) means “x is [thought as being] greater than y”.
• \(\neg (x > y)\) means “it is false that x is [thought] as being greater than y”.
• \(d\) an individual constant that stands for the proper name “God”.

• \(Rd\) means “God is [thought as being] something that exists in reality.”

  Note that the predicate “to exist in the understanding” is in fact

useless, because the challenge is to prove that “to exist in reality” is true of God. To prove it formally,only three assumptions only are necessary, namely:

• Assumption \eqref{eq:1} is the definition of God: the being that is such that nothing greater can be thought of.
• Assumption \eqref{eq:2} is Gaunilo’s: everything that is [thought as] a thing that exists in reality is also [thought of] greater than anything that is not thought of as such. (This assumption, that is Gaunilo’s touch, sounds heretical, because its consequence it that anything that exists in reality, even mud for example, is claimed to be greater than God, if God exists only in understanding, by contrast with mud.)
• Assumption \eqref{eq:3} says that something exists in reality.

Anselm’s argument can be now translated by the following provable sequent:

\(\textcolor{white}{text}\)

Three remarks to conclude.

1. Contrarily to what it was sometimes claimed, Anselm’s argument is not paradoxical. It succumbs neither to Russell’s paradox [3] nor to Burali-Forti’s [4].

2. The discharge of the minor premiss (i.e. the discharge of \(\lnot Rd\) that is the negation that the existence predicate is a predicate of God) shows that Anselm’s argument is an ontological argument or, more exactly, a reductio ad absurdum of the negation of the ontological argument and thus it does not escape Kant’s objection [5]:

   Being [or existence] is evidently not a real predicate, that is, a conception of something which is added to the conception of some other thing. It is merely the positing of a thing, or of certain determinations in it.

   From a Free Logic point of view, that is a logic free of existence assumptions with respect to its terms, general and singular [6], neither \(d\) nor R have existential import.

3. Last, sequent \eqref{eq:4} is certainly valid, but it is valid only in classical logic. In intuitionistic logic, the use of rule \(\lnot I\) is the last step of the proof above, the classical rule of double negation elimination cannot be used and therefore it proves a sequent whose the conclusion is weaker than \eqref{eq:4}’s:

   \begin{equation} \label{eq:5} \forall y \neg (y > d), \forall x \forall y((\neg Rx \land Ry) \to (y > x)), Ra \vdash \lnot \lnot Rd \end{equation}

   It means that, from an intuitionistic point of view, if Kant’s

objection were to be forgotten, atheism could be considered refuted by Anselm’s argument, but not agnosticism.¹