Hilbertのプログラム

前提知識: Hilbertの第2問題, 無矛盾性, Gödelの不完全性定理, 原始再帰関数

Hilbert のプログラム（Hilbert's program）は、Hilbert が 1920 年代の初めに提案した数学の基礎づけの計画である。数学全体を公理系の中に形式化し、形式化された証明を有限の記号列として調べ、有限の方法だけを使ってその公理系が矛盾しないことを証明する（Zac23 冒頭、Rat06 pp. 45–46）。この計画は Hilbert が Bernays・Ackermann・von Neumann らとともに進めたが、Gödel の不完全性定理により、元の形では実現できないと考えられるようになった。ただし、部分的な実現や相対化された形は、証明論 の中心的な研究として続いている（Zac23 冒頭）。
出発点の問いは Hilbertの第2問題 で扱う。そこでは問題の内容、実数の公理、無矛盾性から全称文の正しさが従うこと、弱い算術の無矛盾性の直接の証明を述べている。この記事は計画全体の案内で、各段階の内容と、それを詳しく扱う記事を示す。計画の論理の骨格として次の 3 つを証明する。

計画の組み立て

計画は 4 つの部分からなる。

Hilbert は無限の全体を前提する推論や非構成的な存在証明を捨てることを求めたのではなく、それらを正当化しようとした（Rat06 p. 46、Zac05 §2.2）。

経過

有限の立場

有限の立場（finitary standpoint）は、数学の思考を、すべての部分を見渡せる具体的な対象と、完結した無限の全体を前提しない操作に限る方法上の立場である（Zac05 §3.1）。

• 対象：数字（線を並べた列 $|,\ ||,\ |||,\dots$）と、式・証明を作る記号の列である。
• 命題：数字の等式・不等式、原始再帰で定義される演算についての計算、素数であることのような判定できる性質、有界な量化である。「すべての $n$ で $1+n=n+1$」のような一般の命題は否定が有限の命題にならないので、Hilbert は数字を与えるたびに確かめられるという仮言的な判断として扱った（Zac23 §2.2）。
• 方法：Hilbert 自身は範囲を厳密には定めなかった。Hilbert–Bernays（1934）は、原始再帰による定義と帰納法による証明を有限のものとして認めた。数の領域でのこれらの方法は、次の体系で形式化できる（Zac05 §3.2）。

Hilbertの第2問題 の開いた算術は、この体系の関数記号を後者・和・積に限った部分である。有限の方法の範囲を $\mathsf{PRA}$ と同一視するかどうかは、計画の評価を左右する。

Hilbert と Bernays の無矛盾性の証明の中には、原始再帰を超える方法も有限のものとして使われていた（Zac05 §3.2）。Gödel 以前に有限のものと認められていた方法がすべて $\mathsf{PA}$ の中で形式化できることは、1934 年ごろ以降ほぼ一般に受け入れられている（Zac05 §3.4）。

実在的な命題と理想的な命題

1920 年代の半ばから、Hilbert は数学の式を 2 種類に分けて論じた。実在的な命題（real）は変数を含まない、計算で直接確かめられる式である。理想的な命題（ideal）は量化記号や無限の全体を含み、それ自体としては有限の内容をもたない。Hilbert はこれを、複素解析で実数に付け加える虚数の要素になぞらえた（Zac23 §3）。変数を含み、各数字の代入が計算で確かめられる式 $A(x)$ は一般の実在的命題とよばれることがある。
この記事では、一般の実在的命題を次の形の文で表す。算術的階層 の言葉で、$\Delta_0$ 論理式 は量化記号がすべて有界な $L_A$ の論理式であり、$\Sigma^0_1$ 文 は $\Delta_0$ 論理式 $\theta$ による $\exists x_1\cdots\exists x_k\,\theta$ の形の文、$\Pi^0_1$ 文 は $\Sigma^0_1$ 文の否定である。Goldbach 予想は $\Pi^0_1$ 文である。理論 $T$ の無矛盾性 $\mathrm{Con}_T$ も、$\mathrm{Pr}_T$ を自然に $\Sigma^0_1$ 論理式にとれば $\Pi^0_1$ 文である（記号は Gödelの不完全性定理 の節「第2不完全性定理」のとおり）。
理想的な手段の正当化は、次の性質の形をとる。保存拡大 の考え方を、文のクラスを限って使う。

$F$ は有限の方法を、$T$ は理想的な数学を表すと考える。計画の目標をこの意味の保存性と読む解釈を広めたのは Kreisel である（Zac05 §3.3）。

$\varepsilon$ 計算と代入法

Hilbert の学派が無矛盾性の証明のために開発した形式が $\varepsilon$ 計算である。論理式 $A(x)$ について $\varepsilon xA(x)$ は「$A(x)$ を満たすものがあればその 1 つ」を表す項で、量化記号は
$$ \exists xA(x)\ \equiv\ A(\varepsilon xA(x)),\qquad \forall xA(x)\ \equiv\ A(\varepsilon x\lnot A(x)) $$
と定義される。必要な公理は超限公理 $A(t)\to A(\varepsilon xA(x))$ である（Zac05 §2.2）。証明の中の $\varepsilon$ 項を数字に置き換えて、量化記号のない導出にする方法を$\varepsilon$ 代入法という。最も簡単な場合を証明する。
数値式を、$0,S,+,\cdot$ で作った閉項の等式から $\lnot,\to$ で作った式とする。数値式の真偽は計算で決まる。$A(x)$ を $x$ だけを自由変数とする量化記号のない式とし、$e$ を $\varepsilon$ 項 $\varepsilon xA(x)$ を表す新しい定数記号とする。

証明が使うのは閉項の計算と場合分けだけで、有限の方法の中に収まる。$n$ は導出から計算で求まるので、$\exists xA(x)$ の形の結論からは証拠の数が取り出せる。$\varepsilon$ 項が入れ子になると選び直しの手順は大きく複雑になり、Ackermann の 1924 年の学位論文の証明には誤りがあった。von Neumann が帰納法のない体系で証明を与え、Hilbert はこの方向の延長で算術と解析学の無矛盾性が得られると期待した（Zac05 §2.2）。

無矛盾性から保存性へ

無矛盾性の証明がなぜ還元になるのかを、形式的な理論の間の関係として述べる。Hilbert の 1928 年の議論を $F$ の中で行う形である（Zac05 §3.3）。外から見た形は Hilbertの第2問題 の定理「無矛盾な理論は全称の算術の文を誤らない」にある。
$F,T$ を $\mathsf Q$ を含む決定可能な公理系とし、$\mathrm{Pr}_T$ を $\Sigma^0_1$ 論理式にとる。$\bot$ は $0=S0$ である。次の 2 条件を考える。

• (C1) すべての文 $\varphi$ で $F\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\land\mathrm{Prov}_T(\ulcorner\lnot\varphi\urcorner)\to\mathrm{Prov}_T(\ulcorner\bot\urcorner)$。
• (C2) すべての $\Sigma^0_1$ 文 $\sigma$ で $F\vdash\sigma\to\mathrm{Prov}_T(\ulcorner\sigma\urcorner)$。
  (C1) は $F$ が導出の組み合わせを形式化できること、(C2) は「真な $\Sigma^0_1$ 文は $T$ で証明できる」を $F$ の中で証明できることをいう。$F=T=\mathsf{PA}$ なら (C1) は導出可能性条件 (D2) から従い、(C2) は (D3) を含む条件である。$F$ が $\mathsf{PA}$ を含み、$\mathsf Q$ を含む $T$ の公理系が原始再帰的に与えられ、$\mathrm{Pr}_T$ をその定義どおりに自然に書き下したものにとれば、どちらも成り立つ（$\mathrm{Prf}_T$ を表現する別の論理式にとると成り立つとは限らない）。(C1) は $T$ の導出をつなぐ操作を $F$ の中で書くだけである。(C2) の筋は次のとおりである（細部は省く）。$\Sigma^0_1$ 文は $\exists y_1\cdots\exists y_k\,\theta$（$\theta$ の量化子は有界）の形である。否定を原子式まで下ろした有界な式 $\theta(\vec x)$ の組み立てについて外側で帰納し、$F\vdash\forall\vec x\,(\theta(\vec x)\to\mathrm{Prov}_T(\ulcorner\theta(\dot{\vec x})\urcorner))$ を示す。ここで $\ulcorner\theta(\dot{\vec x})\urcorner$ は、$\theta$ に $\vec x$ の値の数項を代入した式の Gödel 数を $\vec x$ の関数として $F$ の中で表したものである。原子式とその否定では、数の計算が $T$ で導出できることを $F$ の中の帰納法で示す。$\land,\lor$ では導出をつなぎ、有界量化子では $F$ の中の帰納法で有限個の導出をつなぐ。最後に $\theta$ から存在記号を付ける導出を足せば (C2) になる。

理想的な数学 $T$ が有限の方法 $F$ を含むなら、$F\vdash\mathrm{Con}_T$ から $F$ 自身の無矛盾性が $F$ で証明されることになり、次の節で見るように、この仮定は実現しない。定理が実質をもつのは、$F$ が $T$ に含まれず、$T$ も $F$ に含まれない場合である（$T$ が $F$ に含まれるなら結論は明らかである）。Gentzen の結果（Gentzenの無矛盾性証明）は、有限の推論を体現する理論 $\mathsf F$ に、$\mathsf{PA}$ では証明できない $\varepsilon_0$ までの超限帰納法を加えると $\mathrm{Con}_{\mathsf{PA}}$ が証明できる、という形に述べられる（Rat06 式 (1)、p. 47）。この理論は上の「$F$ が $\mathsf{PA}$ を含み」の場合として扱えないので、定理を当てるには (C1)・(C2) を別に確かめる必要がある。それが確かめられれば、$\mathsf{PA}$ で証明された $\Pi^0_1$ 文はこの理論でも証明できる。

不完全性定理の影響

第 2 不完全性定理（Gödelの不完全性定理）によれば、$\mathsf Q$ を含む無矛盾な決定可能な公理系 $T$ は、$\mathrm{Prov}_T$ が (D2)・(D3) を満たす限り $\mathrm{Con}_T$ を証明しない。有限の方法が $T$ の中で形式化できるなら、$T$ の無矛盾性の有限の証明はないことになる。この推論は Hilbertの第2問題 の系「部分理論では無矛盾性を証明できない」で述べた。Bernays は 1931 年の Gödel への手紙で、有限の推論がすべて形式化できるならこの結論になると書いた（Zac05 §3.4）。
Smoryński はさらに、保存性そのものが崩れると論じた（Zac05 §3.4）。次の定理はその要点である。

$F=\mathsf{PA}$ なら、$\mathsf{PA}$ の無矛盾性は集合論の中で標準モデルから証明できるので（無矛盾性 の例「Peano 算術」）、集合論は算術の言語の文へ翻訳して $\mathsf{PA}$ の上で保存的でない。理想的な数学が有限の方法の無矛盾性を証明できる限り、def-hp-conservative は成り立たない。Detlefsen は、計画に必要なのは保存性より弱く、実在的な部分に誤りを生まないことだけだと論じ、この議論に反論した（Zac23 §4）。

計画のその後

元の形の計画が実現しなくても、有限の手段を別のものに替える、対象を数学の一部に限る、という 2 つの方向で研究が続いた（Zac05 §4.2・§4.3）。

Simpson は、可分な場合の Hahn–Banach の定理や Brouwer の不動点定理を含む多くの定理が $\mathsf{WKL}_0$ で証明でき、$\mathsf{WKL}_0$ が $\mathsf{PRA}$ の上で $\Pi^0_2$ 文について保存的であることを、Hilbert のプログラムの部分的な実現と位置づけている（Sim06 Theorem I.10.3、Remark I.10.5・I.10.6、pp. 37–39）。ここで $\Pi^0_2$ 文の保存性の証明はこの記事では与えない（保存拡大 の例「算術と集合論の保存拡大」も参照）。

読む順

関連項目

• 前提: Hilbertの第2問題, 無矛盾性, Gödelの不完全性定理, 原始再帰関数
• 比較: 直観主義論理, Hilbertの公理系, Hilbert流の証明体系
• 道具: 保存拡大, 算術的階層, Peano算術
• 発展: 証明論, Gentzenの無矛盾性証明, 逆数学