ゲーデルと神の存在証明 (番外編その2) [趣味の数学]

明日までに200ページほどの横文字を読み、しかるのちその内容をダブルスペースでレータサイズ10枚程度（つまり、レターサイズにぎっちり5枚、ということですね）にまとめねばならぬのに、「読み」という点においても「書き」という点においてもほとんど手をつけていないにひとしく、ゆえに、ゲーデルの神の存在証明の論理的側面における問題点検証なんてことはちょっとやってる暇がないわけで、今回は「番外編その2」と称して、なにゆえにこのようなつづきものを書くにいたったか、という、そのそもそものところについて、すこし。

さて、このつづきものの初回や番外編その1でも言ったとおり、こうしたことをやろうと思ったきっかけは、メルヴィン・フィッティングのTypes, Tableaus, and Gödel's God で、ゲーデルの神の存在証明について読んだから、であった。

しかし、くだんのフィッティング本は、けっしてゲーデルの神の存在証明についての本ではなく、その主眼は、elementary logicの既習者に向けて、タブローメソッドによる高階述語論理、およびそれの様相ヴァージョンのエッセンスを描くこと、にある。そして、最後の総まとめとしてゲーデルの証明が、言うなればひとつの「症例」として提出され、その証明をいままでのツールで分析することで、ゲーデルの意図や、そしてその問題点を析出する、という構成になっている。

この構成はじつに見事なもので、高階論理や、そしてその様相ヴァージョンについて得た知識が、ゲーデルの証明という、それなりに「生きた例」を通じてその運用例が示され、そして、一般書での取扱いからはけっして望みえないような、ゲーデルの証明にひそむ決定的な問題点についての「腑に落ちる」説明が得られる。

だから、煎じ詰めて言えば、ゲーデルの証明がはたして正しいだのなんだのということはout of questionなのであって、正しかろうが正しくなかろうが、本質的には高階述語様相論理を用いた議論の一例として重要なのであり、そして、さらに重要なことは、フィッティング本でそれまで学んだことがある具体的な問題の決定的な解決に益する、という体験をすることで、そうしたツールのパワーと、そして限界を身にしみて感じることができる、という点である。

ゆえに、こういうモチヴェーションのもとゲーデルの神の存在証明について書きついできたのだから、次なるステップとしては当然それら高階述語論理やその様相ヴァージョンに筆を進めることが妥当ではあるのだが、これ以上「一人暴走状態」をつづけてもあれかな、という思いもあるし、何より、そんなことをすればそれはじっさいの専門にちかい書きものになってしまい、「息抜き」というこのブログの重要ないちコンセプトから大きく逸脱するので、止めておこう。

ともあれ、次回はゲーデルの神の存在証明にひそむ決定的な問題点を、ややテクニカルなところまで突っ込んで見てみよう、と思う。