Anselm’s Argument in First-Order Logic

2020-06-07, updated 2020-06-07 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 tennant2014), but the proof below is maybe the simplest, because it is based on the most elegant version of Anselm’s argument, that of Gaunilo anselm2007:

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:

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:

\begin{equation} \label{eq:1} \forall y \neg (y > d) \end{equation} \begin{equation} \label{eq:2} \forall x \forall y((\neg Rx \land Ry) \to (y > x)) \end{equation} \begin{equation} \label{eq:3} Ra \end{equation} \begin{equation} \label{eq:4} \forall y \neg (y > d), \forall x \forall y((\neg Rx \land Ry) \to (y > x)), Ra \vdash Rd \end{equation}
\begin{prooftree} \AxiomC{$\forall y\lnot(y > d)$} \RightLabel{$\scriptsize{\forall E}$} \UnaryInfC{$\lnot(a > d)$} \AxiomC{$\forall x \forall y((\lnot Rx \land Ry) \to (y > x))$} \RightLabel{$\scriptsize{\forall E}$} \UnaryInfC{$\forall y((\lnot Rd \land Ry) \to (y > d))$} \RightLabel{$\scriptsize{\forall E}$} \UnaryInfC{$(\lnot Rd \land Ra) \to (a > d)$} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$\lnot Rd$} \AxiomC{$Ra$} \RightLabel{$\scriptsize{\land I}$} \BinaryInfC{$\lnot Rd \land Ra$} \RightLabel{$\scriptsize{\to E}$} \BinaryInfC{$a > d$} \RightLabel{$\scriptsize{\lnot E}$} \BinaryInfC{$\bot$} \RightLabel{$\scriptsize{DN, 1}$} \UnaryInfC{$Rd$} \end{prooftree}


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 viger2002 nor to Burali-Forti’s vuillemin1971.
  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 kant2007:

    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 lambert2002, 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.



Author: Joseph Vidal-Rosset

Date: 2020-06-07 dim. 17:37


Made with Emacs 26.3 (Org mode 9.3.7) and Org export head (Many thanks to Ivan Tadeu Ferreira Antunes Filho!;)