Anselm’s Argument in First-Order Logic

2021-01-28, updated 2021-01-28 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, pp. 213–226]), 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, p. 99]:

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:

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}

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

\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 [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, p. 344]:

    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, p. 123], 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.1


N. Tennant, Introducing Philosophy. New York, London: Routledge, 2014.
Anselm, Basic Writings. Indianapolis, U.S.A.: Hackett Publishing Company, 2007.
C. Viger, “St. Anselm’s Ontological Argument Succumbs to Russell’s Paradox,” International Journal for Philosophy of Religion, vol. 52, no. 3, pp. 123–128, 2002 [Online]. Available:
J. Vuillemin, Le Dieu d’Anselme et les apparences de la raison, vol. 14. Paris: Aubier Montaigne, 1971.
I. Kant, Critique of Pure Reason, Rev Ed. London: Penguin Classics, 2007.
K. Lambert, Free Logic: Selected Essays. Cambridge, UK ; New York: Cambridge University Press, 2002.



A French version of these texts on Anselm and Descartes has been published in the Brasilian Review Revista de Filosofia moderna e contemporânea (v. 8 n. 1 (2020): Dossiê “Formas da Razão”). This paper can be downloaded here or there.


Made with Emacs 27.1 (Org mode 9.4.4) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.

orgmode emacs isso debian mxlinux