Are there any notable mathematical or logical issues within Christoph Benzmüller and Bruno Woltzenlogel-Paleo formalized Gödel's ontological proof (pdf) that has been identified by the community?
$\begingroup$
$\endgroup$
5
-
1$\begingroup$ 2022 Benzmüller paper: arxiv.org/abs/2202.06264. $\endgroup$– Joel David HamkinsCommented Aug 8 at 1:19
-
1$\begingroup$ @JoelDavidHamkins Thank you :^). $\endgroup$– Alec RheaCommented Aug 8 at 3:43
-
1$\begingroup$ No, it has been formalised in a proof assistant, and the formalisation is small enough you can fit it on a page (actually it's only 43 lines of Isabelle code), and so peruse it for yourself. By the way, Benzmüller's paper in Joel's comment is published as doi.org/10.1007/978-3-031-42127-3_19 But the result doesn't say what one can imagine it says, as discussed on the Wikipedia page. $\endgroup$– David Roberts ♦Commented Aug 8 at 22:36
-
$\begingroup$ The links that Joel Hamkins so kindly provided should appear in the question. $\endgroup$– Andrej BauerCommented Aug 8 at 22:52
-
1$\begingroup$ Note that the version linked in Joel's comment is not the result referred to by the OP, but a streamlined version that proves the same result by an argument that is simpler and more transparent than Gödel's (i.e. it doesn't formalise Gödel's proof blow-by-blow) $\endgroup$– David Roberts ♦Commented Aug 8 at 23:30
Add a comment
|