10
$\begingroup$

For a decade or so, Christoph Benzmüller from Berlin has explored Gödel's ontological proof (and variants) of existence of God. He uses the proof assistant Isabelle/HOL. He recently posted a preprint, which was highlighted by the cover of the French magazine Science et Vie.

Well, I am not familiar with AI, yet even less with applications to metaphysics. But many practitioners of MO must be. I should like to know how serious is Benzmüller's work considered in this community. Is it controversial or is this considered a respectable research activity ?

Improve this question
$\endgroup$
12
  • 5
    $\begingroup$ My recollection is that Goedel's proof is fine, given his axioms, and that there is a single axiom that almost all philosophers do not find convincing. $\endgroup$
    – Ben McKay
    Commented Aug 11, 2020 at 19:24
  • 3
    $\begingroup$ You say "I recently posted a preprint", but the link is to a paper "A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument" by Benzmüller (not, I guess, you). Is that intentional? $\endgroup$
    – LSpice
    Commented Aug 11, 2020 at 19:30
  • 2
    $\begingroup$ @G.Rodrigues: Dipping our toes into philosophy, one can say that according to Descartes, if God thinks about the proof, then he exists; but following a more Douglas Adams route, if God knows that he exists, then he doesn't have to think about it, and therefore disappears from existence! $\endgroup$
    – Asaf Karagila ♦
    Commented Aug 11, 2020 at 20:58
  • 2
    $\begingroup$ @LSpice. Oups! Of course, I meant He recently posted. $\endgroup$
    – Denis Serre
    Commented Aug 12, 2020 at 5:36
  • 3
    $\begingroup$ @Joël : One of the traditional formulations of the ontological argument relies heavily on the word "necessary." So it is natural, when formalizing the argument, to use a logic where the word "necessary" has a direct formalization. $\endgroup$
    – Timothy Chow
    Commented Aug 12, 2020 at 21:38

2 Answers 2

Reset to default
10
$\begingroup$

Gödel’s proof has the nice feature that one can cleanly separate the logical core of the argument (which is uncontroversial—but see the next paragraph) from its alleged application to theology (which of course is going to be controversial). My opinion is that the main significance of Gödel’s proof is that it shows that there is something to the ontological argument; many people (including my teenage self), when first encountering the ontological argument, perceive it to be total nonsense. Immanuel Kant’s “existence is not a predicate” objection was taken by many to be a decisive refutation. So showing that the ontological argument isn’t completely free of content is already a significant intellectual achievement.

The work of Benzmüller (and Paleo) is interesting because it showed that a (fixable) mistake in Gödel’s proof was more serious than people had previously realized. See The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics for more details.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ Aside from Kant's objection on ontological arguments, I think the strongest criticism to Gödel's ontological proof is that his axioms imply modal collapse, that is, $\varphi \rightarrow \square \varphi$, which somehow undermines the point of modal logic. (That Gödel's axioms imply modal collapse was also verified in another work of Benzmüller and Paleo.) $\endgroup$
    – Burak
    Commented Aug 13, 2020 at 11:42
4
$\begingroup$

I know Benzmüller's work from a slightly different context, formalizing other interesting systems of modal logic. Hadn't heard of this specific project, but it seems very admirable.

  • Formalization of proofs is a highly respectable activity
  • Any "proof of existence of God" written by Gödel is bound to inspire curiosity and interest in logic among the public, thus contributing to education
Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .