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 exposed a (fixable) mistake in Gödel’s proof. See The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics for more details.

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.