林晋「形式化と無矛盾性のパラドックス」

プログラミングと、数学の証明には、非常に大きな、相関関係がある。それが、カリーハワードの結果、だったか。そのことは、ちょっと意外に思われる。プログラムは、いーかげんで、証明は、なにか「厳密」な、なにか、のように思われているから。
数学の証明について、だれもが思うことは、これを、コンピュータに自動でやらせられないかな、ということであろう。
たしかにこれは、コンピュータに定理生成の、指針を、与えてやらないと、順列・組合せで、なんでもやろうとするだろうから、非効率的、であろう。
だったら、せめて、自分たちがつくった数学の定理を、なんとか、それが、「正しい」のかどうかを判断してくれるものなら、できるのではないか。
そうやって、いくつかの、プロジェクトが、実際にあるようである。
ただ、そのどれも、あまり、おもしろい結果を生んでいるようには思えない。なぜ、普及しないか。それは、めんどっちー、んですね。人間の日々やってる証明って、以下同様、とか、ここは一般化できる、とか、簡単に、「一言」ですましちゃう。
でもそれって、コンピュータには通用しない。コンピュータ、そんな、一般化、抽象化の手法なんて、教えられてないんですから。勢い、「n = 2、の場合」の定理を証明したら、ついでに、「n = 3、の場合」の証明も、つくっておかないといけない、なんていう、アホらしい事態になる。
でも、しょーがない。人間の一般化、抽象化、の能力は、ものすごくて、このレベルまで、完全に、コンピュータ、のロジックを引き上げようとすると、とほうもないことになる。場合に応じて、適宜、やっていくにこしたことはないのである（ただ、後でも言いますけど、この状況は、ちょっと、おもしろい。なぜなら、私たちは、その場、その場、で、適宜、「公理」や、推論規則、を作っていることを意味するからだ）。
しかし、もう少し、よくばってみようじゃないか。
この、検証ツール。
「完璧」だったらいいなー...。
はて。
私は、何と、のたまった。
なんと、だいそれたことを言ってしまったのか。
数学の形式体系の、無矛盾性に、挑戦したのが、ヒルベルトのプログラム、であった。彼は、無矛盾な体系による、完璧な、証明マシン、を夢想した。
しかし、その夢は、あの、ゲーデルによって、相当に、難しそうだ、ということにされてしまった。
ここで、掲題のエッセイは、ちょっと、皮肉な「パラドックス」、を紹介する。
「あらゆる定理は、矛盾、しない」、っていう、公理、を追加しちゃえばいいじゃん（Ｓ'、とする）。
これは、例の、ゲンツェンの証明体系における、カット除去定理、にも、流用できる。「カット除去されていない、証明、を、証明と認めない」としちゃえばいいじゃん（Ｓ^*、とする）。
しかし、この要求は、ロジックに親しんでいる人にとっては、まさに「トンデモ」である。これによって、モダス・ポーネス（Ａ、かつ、ＡならばＢ、なら、Ｂ）の、普遍性をあきらめよう、というのだから。
しかし、もう一度、原点に戻ってみよう。われわれは、矛盾している、体系など、欲しくないのだ。矛盾しているなら、その、体系を捨てるのに、なんの躊躇もない。なら、上記の前提を置くことに、なんの困ることがあろう。
こうやって考えてくると、「証明」、とは、何をやっているのだろう、という気分になってくる。

もし事実に反して形式的体系が完全だったら、こういう変なことは起きなかった。Ｓの無矛盾性だろうが、Ｓ'、Ｓ^* のモダスポネスだろうが、正しいことは、Ｓ や Ｓ'や Ｓ^* で全部証明できるはずだからである。

ヒルベルトの形式的理論機械的であるが故に客観的で安定し信頼性が高い。形式的体系の中ならば、ある文章が証明かどうかを、議論の余地無く計算で確かめることができるからである。

形式化は現実世界をコピーするためのものだった。決着をつけるべきは、現実世界の論争であり人工世界の論争ではない。現実世界の決着をつけるべく、人工世界を利用するにすぎない。しかし、現実世界の問題を人工世界にコピーする方法に疑義が生じ得るのだから、形式的体系を使っても論争が消え去る保証はない。もし、誰かが、Ｓ'や Ｓ^* で数学の無矛盾性証明は達成されるから、ゲーデルの不完全性定理は意味がないと主張し始めたらどうすればよいのだろうか。形式的体系を使って、その意見を説得することはできない。そうならば形式化とは一体何なのだろうか？

ゲーデルの言う、「形式的体系が不完全である」、という意味...。
そもそも、上で行っているような議論とは、なにをしていることになるのであろう。そう考えると、なにが「正しい」以前に、自分たちがやっていることこそ、疑わしい、と考えるべきだ、ということなのだろう。
著者は、そこにあの有名な、クリプキの「ウィトゲンシュタインのパラドックス」を見出す。

この議論はクワスとプラスという形式的アルゴリズムを Ｓ'、Ｓ^* という形式的理論、そして「現実の数学」や「無矛盾という現実の概念」を「プラス」という日常言語における言葉に対応させれば、ほぼ同じ議論である。

私たちは、そもそも、「なに」が正しいとか、正しくないとか、言いたかったのであろう。それは、当然だが、「現実世界」なのだろう。その話をしていたはずなのに、なぜか、この「コピー」の世界の、形式化が、完璧であることの方に、議論が、すりかえられている。
つまり、最初から、「コピー」は現実を解析するための、補助手段にすぎなかったことを忘れているのだ。問題は、どんなに「コピー」の動作が立派だろうと、なんの関係もない。コピーをコピーたらしめるために入力した、最初の情報「公理」「定義」「補題」が、どれくらいのレベルなのかが、最初から、問われていたはずなのだ。
そして（著者は言う）、この実感は、私たちの、日々の、コンピュータ・プログラミング、において、さんざん、実感していることであったはずだ。

形式化は非常に困難かもしれないが、いったん、仕様とプログラム開発過程の形式化が実施されれば、誤りを徹底的に排除することが可能であり、テスト、デバッグ、検査などの伝統的技術は必要なくなるというのが形式的技法のうたい文句だった。しかし現実は異なり、現実を形式化するという過程においてこそ致命的な誤りが忍び込む危険性があり、それは形式的でない方法の助けをかりて発見されるのである。

微分方程式のような解析学の言語を使って、自然現象や機械を記述することを一種の形式化と考えれば、実は、これは応用数学者や工学者たちが、何世紀も解析学を使って行ってきたことなのである。だから、これは不思議でもなんでもない。むしろ論理学による形式化というものに解析学による物理世界の探究以上の厳密性絶対性を見る視点の方が奇妙だったのである。

だれだって、プログラムがおかしかったら、バグの解析、をやってるじゃないか。それを、棚に上げて、なんだってんだ。
最後の引用にあるように、しょせん、人間が調べたいと思うものがあるから、それに合わせた、「文法」を人間が考えて、それが、それなりに使えているから、まるで、「一般的」なものであるかのように扱われる。でも、だからといって、最初から、それだけのことであろう（しょせん、言えるとしても、完全性定理までです）。人間の活動は、人間が有用と思う範囲で、自然とのやりとりの中で、成立してきたにすぎない。「あらゆる人間の産物」は、いろいろ、バグをとっていって、なんとなく使えているだけなんです。普遍性うんぬんなど、傲慢もいいところ。
でも、そんなことは最初から、分かっていたことだろう。今さら、何を言っているのか...。

パラドックス!