ヒルベルト・プログラム

(サイエンス)

【ひるべるとぷろぐらむ】

ヒルベルト・プログラムとは文字通りヒルベルトによって提唱された，論理主義，直観主義と並んで数学の基礎付けを目指すプログラムの事である．ただしヒルベルトが数学の基礎付けに関わった時期は大きく分けて1920年代以前と以後に分かれる．通常「ヒルベルト・プログラム」と言った場合には，後者の時期に掲げられたプログラムを指す．

ヒルベルト・プログラムは「形式主義」という特定の哲学的な立場に基いて遂行される．この「形式主義」は，数学の命題は一様に無意味な記号列であり数学はこの記号列を変形していく営みである，としばしば特徴付けられるような形式主義とは異なっている事に注意されたい．いわゆるヒルベルト・プログラム以前のヒルベルトの「形式主義」はこのように特徴付けられるかもしれないが*1．
ヒルベルト・プログラムは次のようにして数学の基礎付けを目指す*2．

数学全体の命題，及び推論を二つのグループに分ける．第一のものは「レアールな数学」と呼ばれ，そこで用いられる命題，推論は有意味である．第二のものは「イデアールな数学」と呼ばれ，ここで用いられる命題，推論は意味を持たない．

この時，レアールな数学として認められるのはレアールな要素のみを含む命題や，それに関する組み合わせ論的な操作である．レアールな要素とは，自然数のように有限ステップで構成可能な対象（例えば自然数はある種の記号列として考えられる）や帰納関数（述語）*3のような有限ステップで計算できる関数（述語）の事である．だから例えば3 + 5 = 8などはレアールな命題であり，これらから命題論理の結合子を用いて作られた命題は全てレアールな命題である．ただし，こうした有意味な命題としてヒルベルトはレアールな命題として自由変数を含む命題も考えていた（例えばa + 0 = 0 +a）．これは有限ステップという観点からすれば奇妙であるが，ヒルベルトはこの時普遍量化子に関する構成的な解釈によって正当化できると考えた*4．さらにレアールな数学は数学的営みの基礎として考えられ，「安全」で基礎付けはそれ以上必要ない，とされる．この範囲の数学はしばしば「有限の立場における数学」などと言われる．

イデアールな数学はレアールな数学以外の部分である(例えばペアノ算術，二階の論理ベースで定式化される実数論，ZF集合論など．)．ここで許される推論は古典論理の全体を含む．
ヒルベルトは以上のように数学を二つの部分に分けるが，数学のかなりの部分はイデアールな数学に属する事に注意されたい（例えば集合論の定理など）．ヒルベルトは直観主義のような改訂主義，すなわち数学を切り詰める事に対して反対していた．つまりヒルベルトはイデアールな数学に対しても基礎付けを与えようとしたのである．この事は「道具主義」と言われる立場に基いてなされる．
イデアールな数学は確かにそれだけでは無意味であるが，有意味なレアールな命題を導出する便利な道具として考えられる．つまり，イデアールな数学にそうした道具としての意味を認める事でヒルベルトは正当化しようとした．しかしながら次のような問いが起こるであろう．

イデアールな数学は道具として安全か？

この問いに答えるには，イデアールな数学の使用が偽であるレアールな命題を導かない事を保証すればよい．つまり，イデアールな数学を使用して証明されたレアールな命題は（有限の立場において）真である事が言えればよいのである．この道具としての信頼性を保証する命題は，数学的命題ではなくて，メタ数学的命題である事に注意されたい*5．

ここでメタ数学に目を転ずれば，メタ数学とは数学の体系そのものの性質（典型的には無矛盾性や独立性）を探求する営みである．メタ数学が扱う対象はある数学体系の命題そのもの，証明そのもの，等であるが，これらは全て有限ステップで帰納的に定義されるような有限の図形として考えられる．すなわち，メタ数学の対象は有限の立場によって正当化される．さらに，レアールな数学で用いられる論法は安全なのであったから，メタ数学においてこうしたレアールな数学で用いられる論法のみを用いて証明されたメタ定理はその安全性が保証されていると言ってよい．故にこの制限されたメタ数学で道具としての安全性を保障すればよい．
ヒルベルトの偉大な発見は，この道具としての信頼性を表わす命題と，イデアールな数学体系の無矛盾性が（ある基礎的な条件の元で）同値である事を発見した事にある*6．故にヒルベルト・プログラムはイデアールな数学の無矛盾性を有限の立場のメタ数学において証明することを目標とするのである．

このように考えると，ヒルベルト・プログラムは数学の基礎付けという哲学的な問いを，数学的な問題として定式化し，数学的に解決する事を目指す試みであると言える．

しかしながら，ゲーデルによって証明された第二不完全性定理はこのヒルベルト・プログラムに対して甚大な打撃を与えた．というのも，大雑把にいって，イデアールな数学体系の無矛盾性を証明するためにはこの体系で用いられている手段以上のものが必要であるからであり，（有限の立場において許される手段はイデアールな数学体系で用いられる手段よりも遥かに狭いのだから）故に有限の立場でイデアールな数学の無矛盾性を証明することは殆ど不可能である．
ただし，この第二不完全性定理がヒルベルト・プログラムを打ち砕いたか，について完全に決着が着いたかは定かではない．ここでは詳述する事ができないが，文献表にある論文が参考になる．

ヒルベルト・プログラム以降，ゲンツェンや竹内外史によって受け継がれた証明論の流れは，大雑把にいって次のものである．「有限の立場」と言われる範囲を拡張し，尚且つ安全である事を示す．そしてこの立場において数学体系の無矛盾性を示すのが最終的な目標である．この目標は竹内外史が1954に予想した「竹内予想」として知られており，1960年代後半にD. Prawitz, W. Tait, 高橋元男らによって肯定的に解かれた．ただし，そこでの証明は竹内外史が提唱する「有限の立場」を越えているので，竹内予想の完全な解決には至っていない．

参考図書

「ゲーデル」竹内外史著　日本評論社 1998年（新版）: この本には思い出話と，ここに挙げたヒルベルト・プログラムに対する解説が含まれている。インフォーマルな解説としては秀逸。
『証明論入門』　竹内外史,八杉満利子共著　共立出版 1988: 日本語で読める数少ない証明論の本。この本は完全性定理，不完全性定理は解説されていないが，ヒルベルト以来の証明論の成果がある程度収められた貴重な本。ゲンツェンが証明した一階述語論理のカット消去定理，ゲンツェンの自然数論の無矛盾性証明，ゲーデルの自然数論の無矛盾性の体系Tのそれへの帰着（いわゆる「ディアレクティカ解釈」），より現代的な二階の証明論（実数論など）の導入など，証明論を勉強する上で欠かせない定理が収められている。理論整然としてコンパクトなので読むのは少し大変かもしれない。さらに進んだ本としては最後に挙げる同じ著者の本がよい。
Hilbert's Program : an essay on mathematical instrumentalism, M. Detlefsen, Dordrecht, D. Reidel, 1986.: ゲーデルの不完全性定理はヒルベルト・プログラムを打ち破ったという主張がどれだけ維持できるのか，について詳細に論じた本。著者のヒルベルト・プログラムの見方は相当に偏っていて，そのままでは普通受け入れることのできない議論もあるが，刺激的な事は事実。ちなみにこうした話に興味があれば，ディトレフセンの他の論文やゲオルグ・クライゼル(G. Kreisel)のいくつかの論文もお勧め。
Philosophies of Mathematics, Alexander George & Daniel J. Velleman, Blackwell Pub, 2001.: この本はいわゆる論理主義，直観主義，形式主義というゲーデル以前の数学の哲学を最低限必要な数学的，論理学的知識とともに学べる貴重な本。前提となる知識は一階述語論理の初歩程度であろう。ただし，細かい点については書いてないので，正確な理解の為には他の専門書を読む必要がある。
"Hilbert's programme", G. Kreisel, in Philosophy of Mathematics, Paul Benacerraf and Hilary Putnam, eds., Cambridge University Press, 1986(2nd.ed.), 207-238.: ヒルベルト自身の著作はその多くが曖昧な点を多く含んでいるが，現代的なヒルベルト・プログラムの解釈を提出したのはクライゼルによるこの論文であろう。クライゼルらしく，非常に難解で，追える所と追えない所が入り混じっている。クライゼルが最初に指摘したと言われる，（ゲーデルの第二不完全性定理が成り立つ）形式的体系Tについて，Tの無矛盾性を表しているように見えて，かつTで証明できるような論理式が存在する，に関連する話も入っている。大変重要な論文。
"Mathematical Logic", G. Kreisel, in Bertrand Russell : Philosophy of the Century, R. Shoenmann ed., Allen & Unwinn, 1967, pp. 201-273.: このクライゼルの論文で本文に書いた，イデアールな数学の道具としての信頼性を表わす言明とイデアールな数学体系の無矛盾性が同値である事が示されている(p. 236)。ヒルベルト・プログラムの解説も含まれている。これもクライゼルらしく，非常に長くて難解な論文。クライゼルは現代の論理学，数学基礎論を牽引した偉大な論理学者であり，数学の基礎付けに対するこだわりや，色々なリマーク（説教？）も盛りだくさん。哲学的にも有益。
From Brouwer to Hilbert, P. Mancosu ed., Oxford University Press, 1998.: この本は数学基礎論史，数学の哲学における第一人者であるMancosuが編集した本で，今までに翻訳されていないヒルベルトの論文が読める。ただ，章の初めについているMancosuのイントロダクションは非常に参考になる。
Proof Theory,　Gaisi Takeuti, North-Holland, 1987: 現代の証明論の教科書。一階述語論理の完全性定理，カット消去定理や不完全性定理，二階の証明論，infinitary logic，Consistency Proofなどなど盛りだくさん。いわゆる「竹内予想」の超限的な論法を用いた証明も載っており，ヒルベルト自身の「有限の立場」を拡張した，著者の立場に基くヒルベルト・プログラムを受け継ぐ無矛盾性プログラムが展開されている。ヒルベルト・プログラムの延長線上にある現代の証明論を知るには必須の本。ちなみに，他には線形論理のパイオニアである，ジラールの"Proof Theory and Logical Complexity"(Bibliopolis)や，シュッテ学派のポーラーズの"Proof theory : an introduction"(Lecture notes in mathematics, Springer-Verlag, 1407)も定評がある。ジラールの本は重厚な本で，様々な話題が盛り込んである．不完全性定理，カット消去定理，正規化定理，完全性定理，竹内予想の超限的論法を用いた証明，竹内予想のジラールによる分析，ω-logic，ディアレクティカ解釈などなど。ポーラーズの本はシュッテ学派だけあって，いわゆるordinal analysis周辺の話題を中心に扱っている。