CPT : ゲーデルによる神の存在証明についてどう考えていますか？

JYB:    11世紀のカンタベリーのアンセルムス（Anselm of Canterbury）から始まる「神の存在証明」には長い歴史があります。ゲーデルによる存在論的な証明は非常に興味深いものです。そこから集合論と算術の無矛盾性の証明を導くことが可能です。そして、これは、なぜか（ある意味では）ゲーデルの第2不完全性定理と矛盾します。このことは、私達がインドのバラナシ（ヒンズー教と仏教の両方で有名な都市）で開催した「第3回論理と宗教に関する世界会議（3rd World Congress on Logic and Religion）」（2022年11月）において講演を行った Piergiorgio Odifreddi によって示されたことです。

この結果は奇妙に思えるかもしれません。しかし、その不完全性の結果は絶対的なものではありません。実際、ゲーデルによって不完全性定理が証明されてすぐに、ゲンツェン（Gerhard Gentzen）は算術の無矛盾性の相対的な証明を与えました。そして、ゲンツェンはゲーデルのお気に入りの論理学者の一人でした。ゲーデルは、数理論理学における彼の最後の重要な結果を示しました。これは、「Dialectica Proof」として知られる算術の無矛盾性の証明です。この結果は1958年にSwiss Journal Dialecticaの特別号で発表されました。この特別号はスイスの論理学者パウル・ベルナイス（Paul Bernays）の70歳の誕生日を祝したものでした。パウル・ベルナイスは、デビッド・ヒルベルト（David Hilbert）の論理学分野における主要な共同研究者です。

面白いことに、Chistoph BenzmuellerとDov Gabbayは、コンピュータ技術とのインタラクションは、存在論的な議論の形式的評価を可能にするだけでなく、関連する概念の理解をシャープにすることに役立つということを示しました。この仕事は、ワルシャワで2017年に開催された「第2回論理と宗教に関する世界会議（2nd World Congress on Logic and Religion）」で発表されました。この国際会議には、Saul Kripke（Schlock Prize）、Laurent Lafforgue（Fields Medal）、Michał Heller （Templeton Prize）らも参加しました。