新井敏康「ゲーデルの無矛盾性証明」

ヒルベルトのプログラムについて、どれくらいの人が、ご存知なのだろうか。
ヒルベルトは、カントールが進めた集合論が、さまざまな矛盾、パラドックスを生みだしてしまった、反省から、一つの、プログラムを提唱する。
数学を、その文法から、反省することで、完全に、有限の文字列の、配列として、解釈し、記述し直す。
そして、数学の証明とは、その文字列の、有限回の、並べ変えの、操作、として、定式化してみよう、という考え、だ。
ここで、重要なキーワードとなるのが、「有限の立場」である。
これは、どういうものなのか。
ヒルベルトは、数学の危機から、数学を守りたかったのだ。そのために、彼が考えたやるべきこととは、数学を、安全だと分かっている、「もの」、「操作」、それだけで、全部、作っていこう、ということだ。そうすれば、その範囲で、安全だ、と考えられる。
では、ここで言っていることを、真面目に、「字義通り」、うけとってみようではないか。

1. 初めに、succ(;a)=a+1 は問題ないだろう。ここで a は数字を走る変数として、その数字の最後にもう一度 +1 を書き加えた数字を考えればよいから。
2. 次に add(x;a)=a+x であるが、これは数字 x の生成過程を、0 からでなく数字 a から始めて、なぞればよい。add(0;a)=a 、add(x+1;a)=succ(;add(x;a)) つまり a+0=a 、a+(x+1)=(a+x)+1 。
3. さらに mult(x,y;)=x*y なら、mult(x,0;)=0 、mult(x,y+1;)=add(x;mult(x,y;)) つまり x*0=0 、x*(y+1)=x*y+x なので、数字の y の表す +1 の反復の代わりに、操作 a -> add(x;a)=a+x の反復だと思えばよい：mult(x,y;)=0+x...+x (y 回）。
4. 一般には、既に定義された関数 g(y_1,..,y_n;a_1,..,a_m) と h(y_1,..,y_n,x;a_1,..,a_m,b) から、次のようにして原始帰納法でつくられた関数 (y_1,..,y_n,x;a_1,..,a_m) も許容できる。f(y_1,..,y_n,0;a_1,..,a_m)=g(y_1,..,y_n;a_1,..,a_m)、f(y_1,..,y_n,x+1;a_1,..,a_m)=h(y_1,..,y_n,x;a_1,..,a_m,f(y_1,..,y_n,x;a_1,..,a_m))、但しここで、変数 y_1,..,y_n,x は g、h、f の定義もしくは計算において、数字として表示されていることが必要である（ことの可能性のある）もので、他方、変数 a_1,..,a_m,b はそれらの計算で数字一般でありさえすればいくつであるかは知る必要のないものである。

しかし、これは、かなり「狭い」ことになっている。

• それでは指数関数 exp(x;)=2^x はどうであろうか？ これを x に関する帰納法で、exp(0;)=1 、exp(x+1;)=exp(x;)+exp(x;) すなわち 2^0=1、2^(x+1)=2^x+2^x と定義しようとすると、帰納法の仮定から数字を表すことは分かってはいるが、何回 +1 を反復した過程の自然数であるか不明である 2^x 同士の足し算になってしまう。足し算 add(x;a)=a+x は、数字 x が表す反復過程をなぞって得られたので、いくつになるか分からない 2^x を足すことはできない。あるいはもう少し穏便に述べて、いくつなのか分からない数を足す過程を想像し難い。

このように、基本的な、指数関数さえ、この世界では、考えられなくなってしまった（ちなみに、このような方法を、可述的帰納法（predicative recursion）というのだそうだ）。
もちろん、これは、数学そのもの、ではない、数学を記述している、言語、その文字列上の操作の話なので、これでもけっこうなことはやれるのかもしれないし、よく分からない。
ただ、普通の計算可能性としては、もう少し広い、原始帰納的関数、というのを使う。ここにおいては、上記の指数関数も定義できるわけだが、その違いは、ある「過程の完結」の把握にある、という。

しかし注意しなければならないことは、ここに含まれていることは自然数の概念より高位の抽象性であり、論理的に言えば既に見つかった証拠の略記としてでなく、存在が推量できるがゆえにそれを仮定できるという意味の存在量化子をもってしてしか「仮定の完結」は表現できないということである。また、可述的帰納法での二種類の変数の使い分け（一般的な数字を指し示す表現と数字そのもの）も無効にする。

やっと、ふつうの数学に近くなってはきましたね。
まあ、このあたりが、ヒルベルトの有限の立場の意図と考えるところが、無難なのでしょう。
しかし、私が言いたいと思ったことは、上記の指摘は、数学というものがなにをやっているのかを考える上で、たいへん重要なポイントが入っていると思うんですね。ヒルベルトの、有限の立場は、このように、多少ではあっても、厳密な有限からは、このように、逸脱している。そんなの、たいしたことじゃねえや、と考えるのは勝手であるが、それは、他方で、上記の考察では、どこまでやれるのか、をちゃんと把握した上でないと、ということでしょう。
また、こういったことを分かってないと、気持ち悪い、「抽象」の魔術、という罠の中から、抜けられなくなって、神秘的な夜迷い言を、さとりすましたように、ごたくせんをたれることになっってしまう、ってわけでしょう。
さて、この掲題の論考ですが、一階の古典論理上の自然数論の、無矛盾性の証明、に関わる、ゲーデルの仕事の紹介となる。ここで、あれ、っと思った人もいるかもしれない（いないか）。ゲーデルの不完全性定理によって、無矛盾性、は証明できないんじゃなかったのか。
もちろん、そうなのであるが、要するに、ちょっと、体系を広げたものを用意して、その中で、元の体系を証明しよう、というアイデアで、証明論では、ゲンツェンが、超限順序数を使っ（た帰納法によっ）て証明したわけだ（もちろん、これが、じゃあ、なにをやっていることになっているのか、という話は、あるんだろうが）。
これを、有限型、をもった、原始帰納的汎関数、に代替したもの、でゲーデルは証明した、というわけですね。
このあたりまでくると、直観主義論理、や、プログラミング言語、カーリー=ハワードの同型定理、とも、かかわってきて、ここでも、結局、たいていのことは、ゲーデルから、始まってるんだな、といった結論でしょうか。

現代思想2007年2月臨時増刊号 総特集=ゲーデル