§０．ヒルベルトのプログラムＨＰとは
１９２０年代，数学の巨匠ヒルベルトは，記号の世界において数学そのものの模型， 今風にいうとバーチャルな数学を創造しょうと企てた． どんな数学の難問も，記号世界の数学模型に投影させれば，有限の組合せ問題になる． そうすれば，絡んだ糸がほぐれるように，いつか必ず解けると考えたのである． すでに６０歳に近かったヒルベルトは，この新機軸を証明論と名付けて粉骨砕身し， 多くの優秀な門弟たちとともに，数学基礎論の新分野，というよりも数学基礎論そのものを数学の一分野として，確立させた．
現在の数学基礎論には、証明論の他にモデル論、集合論、計算論などの分野がある． もっと今風的にいえば，（数学の）ロジックの中に，数学基礎論とその他３分野があるというべきかもしれない． 残念ながら，そんな中で証明論はすでに枯れた分野になっているという見方が広まっている． 確かに一つの技術な流れ（ゲンツェン流の証明論）だけを見れば先細りの感を免れないかもしれないが，証明論全体は多様な方向性と優れた技術手法を持った豊かな領域である． 世紀の変わり目のいま，世の中は激しく動いており，数学は何か，どうあるべきかが厳しく問いかけられており，数学基礎論はそれに答える役割を担っている． そんな状況の下で，証明論は数学基礎論の要としてますます重要になって行くと思う．
本論では，「ヒルベルトのプログラム」をＨＰと略称する． ＨＰとは，証明論の開発によって数学全体の明晰性をさらに高めて行こうというものである． 数学の明晰性は，完全性，無矛盾性，決定性（停止性），有限還元性(finitistic reduction)などの概念によって具現される． ヒルベルトは，数学の実世界と同型な記号世界を作れると信じていたので，これらの目標は同時に達成されるはずのものであった． しかし，現代的には無矛盾性プログラム，有限還元性プログラムなどと分けて考えるのが便利である． 最近の基礎論研究者の間では，有限還元性（還元主義）プログラムを単にＨＰと呼ぶことが多い．
§１．ＨＰの起源
● 幾何学基礎論から数学基礎論へ
ヒルベルトが1899年に発表した『幾何学基礎論』(文献[1])は，いまで言うところのモデル論の本である． ある公理系の中の一つの公理が他の公理から独立であることを示すモデル論的方法は，その公理だけを成り立たせず他をすべて成り立たせるモデルを構築するものである． すでに1870年代にクラインらは，この方法で第５公準（平行線の公理）の独立性をエレガントに示しているが，『幾何学基礎論』では，通常明らかと思われる諸公理に対しても公理同志の関係をモデルを使って系統的に調べている．
とくに重要な結果は，ユークリッド幾何全体の無矛盾性を示すために，その可算モデルを実数（代数的数）上に作ったことである． この方法によって，ユークリッド幾何の無矛盾性は，ある種の実数演算の体系（ヒルベルトが「算術」と呼ぶもの）の無矛盾性に還元された． そこで，「実数論の無矛盾性を証明せよ」というのが，ヒルベルトの第２問題となる． しかし，このとき実数論自体の公理化はまだ完成していなかったのである．
実数論の公理化の難しさは，その中での自然数の扱いと，完備性の記述にある． いま後者について簡単に説明しておこう． 実数とその上の演算に関するどんな公理系Ｔ（たとえば，実閉体の公理）に対しても，Ｒの真部分集合（たとえば，多項式の解となるような実数全体）でその公理をすべて満たすものが存在してしまう． そこでヒルベルトは，公理系Ｔのモデルの中で一番大きな（完備な）ものであるという主張を実数の公理に加えた． モデルが最大かどうかは，モデルの外の世界に依存する性質なので，完備性の公理が厳密な公理論の立場と相容れないのは明らかである． 自然数全体と自然数の集合たちを扱う２階算術（現代のものとは少し違う．ヒルベルト・ベルナイスの体系とも呼ぶ．）を用いることによって，実数論を初めて厳密形式化したのは，ヒルベルト・ベルナイスのザ『数学基礎論』(文献[2])である．この労作により，その後は２階算術の無矛盾性を示すことが第２問題であると考えられるようになった．
§２．決定可能性と完全性
● 公理系の完全性
ヒルベルトは，実数の完備性にならって，公理系Ｔが完全（英語ではどちちらもcomplete）であることを，それより真に大きな無矛盾な公理系がないことと定義した． つまり，完全な公理系Ｔから証明できない命題を１つでもＴに加えると矛盾した体系になる． したがって，Ｔが完全であることは，どんな命題に対しても，それ自身かその否定かがＴで証明できることと同じになる．
ヒルベルトは，どんな数学的な構造も完全な公理化が可能であると考えていた． その構造で成り立つ命題が全て公理であるといってしまえば１つの完全公理系ができるが，公理であるか否かが有限的に判定できないようなものは公理系と呼ぶに相応しくない． そして，もしある構造に対して完全な（厳密な意味での）公理化が可能であれば，その構造における任意の命題の真偽も有限的に判定できることがわかる． もう少し正確に説明するために，いくつかことばを用意しておこう．
● 再帰的集合と決定可能性
自然数もしく有限の記号列の集合が r.e.（recursively enumerable, 再帰的に枚挙可能）であるというのは，その要素をすべて並べあげる機械的な手続きがあることをいう． たとえば，偶数全体とか素数全体は r.e.集合である． r.e.集合で，その補集合もr.e.になるものを，再帰的 (recursive)という． 偶数全体も素数全体も再帰的集合である． 再帰的集合Ａに対しては，その要素を並べあげる手続きと非要素を並べあげる手続きが両方あるので，任意の自然数（また記号列）が与えられたとき，それがＡに属するか否かを，どちらの並べ上げに現れるかで有限時間内に判定できる． それゆえ，再帰的集合は決定可能集合とも呼ばれる．
我々が公理系と呼ぶものは，正確には再帰的公理系のことで，公理の集合が再帰的であることを要請する． そうすると，それから演繹される定理の集合が r.e. になるのは容易にわかる． さらに，もし公理系Ｔが完全であれば，Ｔの定理にならない命題Ａの集合は，¬ＡがＴの定理になるようなＡの集まりと同じだから，やはり r.e. になり，Ｔの定理の集合は再帰的である． したがって，ある数学的構造に対して完全な公理系が見つかれば，その構造における命題の真偽は決定可能である．
● 決定可能性と不可能性
ゲーデルが１９３０年に発見した第一不完全定理は，自然数論を含むどんな公理系も完全でなく，また決定可能でないというものである． これから直ちに，ペアノ算術ＰＡやＺＦ集合論が不完全であることや，自然数の構造（Ｎ,＋,・,＜）や有理数の構造（Ｑ,＋,・,＜）における真偽が決定不能であることが導ける． さらに群論，環論，述語論理（の定理全体）なども決定不能である．
他方，決定可能な完全理論としては，自然数上の足し算のみの体系，実閉体，代数的閉体，p-進体などが知られている． したがって，実数の構造（Ｒ,＋,・,＜）や複素数の構造（Ｃ,＋,・）における真偽は決定可能である．
ある公理系（または構造）の決定可能性を示す有力な方法に，タルスキが開発した量化記号消去法がある． 実（順序）閉体の場合，∃x (ax^2 + bx + c = 0) が量化記号のない式 b^2 - 4ac >= 0 と同値になることはお馴染みであるが，実数体上のどんな論理式（例えば，１１次多項式が丁度７つの解をもつことを表すもの）も，量化記号∀x,∃xのない等式，不等式だけの論理式に書き直せる． これを使えば，実数の命題の真偽判定は，計算問題として解けるのである． また，このことは，実数の構造（Ｒ,＋,・,＜）の上で，整数であるという性質がうまく定義でないことを意味している．
§３．無矛盾性と有限還元性
● 無矛盾性プログラム
『幾何学基礎論』でユークリッド幾何の無矛盾性を実数論のそれに帰着させたように，ある理論のモデルを別の理論の中に構成することで，相対的無矛盾性を示す方法はすでに確立された． しかし，どこかに絶対無矛盾の拠り所を定めない限り，この論法では永久に真の無矛盾性は保証されない． その拠り所となるのが，有限の記号を有限的にだけ扱う立場，いわゆる有限の立場である． 有限の立場は，現代的には原始再帰的算術ＰＲＡ(Primitive Recursive Arithmetic)として形式化されることが多いが，その詳しい説明は省略する．
有限の立場で扱える命題は，量化記号∀x, ∃xを含まない算術的な論理式であると考えてよい． しかし，x+y = y+x のように自由変数を含んでよいので，これを ∀x∀x (x+y = y+x) のように書き換えれば，外側だけに∀xのついた自由変数のない論理式（Pi^0_1 文と呼ぶ）を扱うと言い直しても差し支えない． そして，有限の立場で正しいことが示されたPi^0_1 文は，絶対に正しいということを以下の議論の大前提とする．
さて，ある公理系Ｔの無矛盾性を示すにはどうしたらいいだろうか？ ＨＰでは，矛盾命題（たとえば，０＝１）が証明されないことを示すために，公理系Ｔで証明されるPi^0_1文がすべて有限の立場でも（したがって絶対に）正しいことを示すことを目標とした．
証明可能性を表す記号├を用いて，この目標を形式的に見てみると，２通りの解釈ができる．
１つは，
任意のPi^0_1文Ａについて，（Ｔ├Ａ）→Ａ (1)
が正しいことを有限の立場で検証するもので，これを
無矛盾性プログラム という．
ここで，文(1)全体がPi^0_1文になっていることが重要である．
もう１つは，
任意のPi^0_1文Ａについて，
（Ｔ├Ａ）→（有限の立場でＡが正しい） (2)
を示すものである．
こちらの方が幾分素直な解釈だと思うが，これを証明するためには有限の立場を形式化した上で，たとえば
任意のPi^0_1文Ａについて，
（Ｔ├Ａ）→（ＰＲＡ├Ａ） (2')
をＰＲＡで証明することになる．（(2')はPi^0_1文に
ならない．）
これを有限還元性プログラムという．
無矛盾性プログラムにおいて， Ａを矛盾命題（０＝１）とおけば，（Ｔ├０＝１）→０＝１は Ｔ not├ ０＝１と同値で，これをゲーデルはＴの無矛盾性を表す文 Con(Ｔ) と定義した． 従って，無矛盾性プログラムが成功すれば，Con(Ｔ) が導かれるわけだが，逆に Con(Ｔ) から無矛盾性プログラムを導くことも容易にできる（演習問題）． ゲーデルは，ある程度の自然数論を展開できるどんな無矛盾な公理系Ｔ（例：ペアノ算術PA，ＺＦ集合論）も自らの無矛盾性Con(T)を証明できないことを示した．これを第２不完全性定理という．
ゲンツェンは，順序数ε_0までの超限帰納法を用いて，ペアノ算術PAの無矛盾性 Con(PA) を証明した． もちろん，ペアノ算術内部ではそのような超限帰納法は使えないのだが，有限の立場にそれを加えることによってペアノ算術を包含するような強い理論ができるわけではないことも注意しておこう． PAを自然に（PAで定義できる集合を扱えるように）２階算術に拡張してできる公理系を ACA_0 というが，ゲンツェンの結果から直ちにこの体系の無矛盾性も得られる． ACA_0 では，そこで定義される実数に対してボルツァーノ・ワイエルシュトラスの性質などが導けるので，ACA_0 を実数論として見ても優れた体系であり，ゲンツェンの結果は第２問題のかなりいい部分解になっていると考えられる． さらに強い２階算術の体系については，現在もさまざまな研究が進行中である．
● 還元性プログラム
Ｔ＝ＰＲＡとしても，無矛盾性プログラム（Ｔ├Ａ）→Ａは，ＰＲＡで証明できない． しかし，有限還元性プログラム（Ｔ├Ａ）→（ＰＲＡ├Ａ）は，Ｔをある程度大きくとってもＰＲＡで証明できるのである．
ＰＲＡに再帰的な集合が存在するという再帰的内包公理を付け加えた２階算術の体系を RCA_0 といい，さらに無限２分木がかならず無限の道をもつという弱ケーニヒの補題を公理に加えた体系を WKL_0 という． WKL_0 では，実数の有界閉区間がハイネ・ボレルの意味でコンパクトであることがいえるし，解析学もある程度展開できる． にもかかわらず，Pi^0_1文Ａにたいして（WKL_0├Ａ）→（ＰＲＡ├Ａ）となることがＰＲＡで証明できる． これをヒルベルトのプログラムの部分的実現と見なすこともできる．
他方，Ｔを数学全体扱う大きな体系ＺＦ＋ＡＣ（選択公理）＋ＣＨ（連続体仮説）とおいたとき，任意の算術命題Ａにたいして（Ｔ├Ａ）→（ＺＦ├Ａ）が成り立つ事実も重要である． これは，上に述べたゲーデルの模型Ｌの応用として導かれるが，相対無矛盾性の結果Con(ＺＦ)→Con(ＺＦ＋ＡＣ＋ＣＨ)より実用的である． たとえば，フェルマーの定理の証明に選択公理が使われているなら，使わないような証明もあるということを意味している． 一般に，２つの形式体系 Ｔ_1⊂Ｔ_2 に対して，ある論理式のクラスΓに属する Ｔ_2 の定理はすべてＴ_1 の定理でもあるとき，Ｔ_2 はΓに関するＴ_1 の保存的拡大であるという． いろいろな体系の間で，いろいろなクラスに関する保存的拡大の関係が調べられている．
§４．最近の話題から
最後に，ヒルベルトのプログラムの延長上にある（本来の趣旨からは多少それるかもしれないが）比較的最近の証明論の研究をいくつか紹介する．
● 数学的な独立命題の発見
ある公理系で，証明も反証もできない命題を独立命題という． ペアノ算術において、いわゆる自己言及文ではなく、数学的に意味を持つ独立命題が存在するか否かは、ゲーデル以来長らく基礎論の研究者の関心の的であったが、１９７７年にパリスとハーリントンがラムゼイの定理の一変種がそれになることを示した．
余白が少ないので，非常に大雑把な説明をしておく． 二つの自然数 a < b が大きく離れていることを，その間にある種のラムゼイ性が成り立つこととして，算術的述語 PH(a,b) を定義する． このとき，∀a∃b PH(a,b) は正しいのだけど，a から b へは算術的に定義される関数では決して到達できないということが起こる． つまり，∀a∃b PH(a,b) は，ペアノ算術ＰＡで証明できない真なる命題になる． 具体的には，この命題からCon(PA)を導くことによって，その証明不可能性が示される．
パリス・ハーリントン以降、２階算術の諸体系や集合論に対してまで種々の独立命題が発見されている．
● ゲーデルのプログラム
パリス・ハーリントンの命題は，ペアノの算術ＰＡでは証明できないけれど，ある程度強い２階算術の体系，たとえば算術的超限再帰(Arithmetical Transfinite Recursion)の体系ATR_0なら問題なく証明できる． 上にも述べたように，２階算術の体系にもいろいろな独立な命題があって，それに対しては，さらに高階の算術体系や集合論を持ってくれば，たいがい証明ある いは反証されるようになる． そして，ＺＦ集合論の独立命題に対しては，巨大基数の公理を仮定することで決定されるものが多い．
こうして次々高度な集合を認める理論を作って行けば，最終的にどんな命題の真偽もどこかで決定できるのではないかというのがゲーデルの予想であり，とくにこの方法で連続体仮説の否定を証明しようというのがゲーデルのプログラムである．
ゲーデルが，自分の研究において，ヒルベルト学派からの影響を隠蔽する傾向があったことはしばしば指摘される． しかし，いくらひた隠しても，ヒルベルトの思想がいたるところから滲み出してしまうのだ． それにしても，ゲーデルのプログラムは，あまりにヒルベルト的であった．「われわれは知らねばならない，そして知るであろう」というヒルベルトの信念を，いつのまにかゲーデルも共有していた．
● 逆数学プログラム
逆数学は，２階算術の枠組みにおいて，ある定理を証明するのにどの程度の集合存在公理が必要かを調べるものである． 必要な存在公理によって数学の命題の世界に等高線を入れてみると，数学史の流れや，異なる理論間の感覚的な類似性が，うまく捉えられるというのがこの研究の売り物である． たとえば，中間値の定理より実数の連続性公理（例：ワイエルシュトラスの上限に関する公理）の方が強い存在公理を必要とすることが証明される． それは数学史の流れがより高度な集合論を求める方向に進んだとも解釈できるであろう．
すでに，２階算術の体系 RCA_0, WKL_0, ACA_0, ATRo を導入したが，この他に (Pi^1_1)-CAoという体系もよく知られている．
１９７４年頃 H.フリードマンは，次のような現象に気付いた：
数学の定理の多くはRCA_0で証明できるか，そうでなければ上にあげた他の
４つの体系のどれかと論理的に同値であることがRCA_0において証明できる．
これは「逆数学現象」と呼ばれ，その後もこのパターンに当てはまる数多くの定理が S.シンプソンを中心とする研究グループによって発見されている．
例えば，ボルツァーノ・ワイエルシュトラスの定理はACA_0で証明できることを
上に述べたが，逆にボルツァーノ・ワイエルシュトラスの定理からACA_0も導ける
のである．
● 実効還元性プログラム
有限還元性プログラムは，無限を扱う超越的な数学（の無矛盾性）を有限の立場（のそれ）に還元するものであった． 有限の立場は，現代的には原始再帰的算術 PRA として形式化されると上に書いた． しかし，計算量理論の発達により，もはや原始再帰的な計算は十分に構成的であるという感覚が薄らぎ，それに変わって多項式時間計算可能性が，より実際的な計算可能性を表すという見方が強くなってきた．
多項式時間計算可能（実効的）関数の形式体系には，コブハムの定理を基にしてクックが導入した PV がよく知られているが，その他にも限定算術の体系 S^1_2 などがある． そこで，これらと無矛盾性において同等になる２階算術の体系を定義し，そこでどれだけの数学が展開出来るかを調べようという研究が，最近始まった．これを実効還元性プログラムと呼ぶ．PV に対しPi^0_2保存拡大になっていて，かつかなりの数学が展開できそうな体系として BTFA が有力視されているが，いまのところまだあまり成果は得られていない．
● プール＝エルとクリプキの定理
１９６０年代，プール＝エルとクリプキは，算術を含むどんな理論も，字面だけ見ればみんな同型になっているというすごい定理を発見した． 不完全性定理の最強バージョンともいえるこの結果には，さすがのゲーデルも驚いたらしい．
昨年末のことであるが，この定理が有限還元性プログラムについての筆者の予想を解く鍵になるというメールが，この分野の大家であるＳ．シンプソン教授から届いた． 現時点では，まだ確かなことは言えないが，なかなか面白い事実が潜んでいそうな予感である．
（追記）田中の予想とその解法について興味ある方は，以下の資料を参考にしてほしい．
シンプソン教授の講演資料 pdf
完全な証明は，Simpson-T.-Y.の共著論文として発表される予定である．
参考文献
[1] ヒルベルト著（中村訳）『幾何学基礎論』弘文堂
[2] ヒルベルト・ベルナイス著（吉田・渕野抄訳）『数学の基礎』
シュプリンガー・フェアラーク東京
[3] 杉浦光夫編『ヒルベルト２３の問題』 日本評論社
[4] 田中一之編著『数学基礎論講義』 日本評論社
[5] 田中一之編『数学の基礎をめぐる論争』
シュプリンガー・フェアラーク東京