この記事は検証可能な参考文献や出典が全く示されていないか、不十分です。出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方）
出典検索?: "ヒルベルト・プログラム" ? ニュース ・ 書籍 ・ スカラー ・ CiNii ・ J-STAGE ・ NDL ・ dlib.jp ・ ジャパンサーチ ・ TWL（2019年6月）

ヒルベルト・プログラムとは、ダフィット・ヒルベルトによって提唱された、数学を形式化しようとする試みのことをいう。ヒルベルト計画とも呼ばれる。
概要

ヒルベルトは、その証明を形式化することで、数学全体の完全性と無矛盾性を示そうと考えた。具体的には、
数学において真である命題は必ず証明できること

公理から形式化された推論をどれだけ行っても、矛盾が示されることは絶対にないということ

という事実を、有限の立場と呼ばれる確かな方法を用いて証明しようとする計画である。有名なヒルベルトの23の問題の2番目で、実数論の無矛盾性の証明を挙げている（よく自然数論の無矛盾性をさすものと誤解されている）。

1900年をはさんだ数年間に、数学の一部である集合論においていくつもの矛盾（パラドックスと呼ばれる。集合論の項を参照）が発見された。ヒルベルト・プログラムは、単にその矛盾を取り除く（＝無矛盾性）だけではなく、今後二度とこのような矛盾が現われないように、数学全体に確固とした基盤（＝完全性）を与える目的があった。

この計画は、1930年にクルト・ゲーデルが発表した不完全性定理により深刻な影響を受けた。とりわけ「自然数論を含む帰納的に記述できる公理系が、無矛盾であれば自身の無矛盾性を証明できない（第2不完全性定理）」は、有限な立場のみではあらゆる公理系の無矛盾性を証明できないとするもので、ヒルベルト・プログラムでは自然数論だけでなく、実数論、さらには集合論全体の無矛盾性をも、自然数論のような基本的な体系の上で示すことを目的としていたため、この定理によって大きな修正を迫られることになった。

ただしヒルベルト・プログラムは否定されたわけではなく、現在でも研究が続けられている。「不完全性定理が成立しない体系」および「ゲーデルの完全性定理」も参照

自然数論の無矛盾性については、1934年にゲルハルト・ゲンツェンによって、証明の正規化（カット除去定理）を用いることによって示されたとされた。しかしこの方法では、証明の正規化手続きの終了性がε0までの超限帰納法によってなされている。この証明方法の正しさは、ヒルベルトのような「有限の立場」に立っていると主張する研究者が、手続きが実行可能である点をその根拠としているが、ε0までの超限帰納法が「有限の立場」で正当な原理であるかは議論の余地がある。

実数論に関しては、ゲーデルに師事した竹内外史により、1954年に高階述語論理における証明の正規化によって無矛盾性が証明されることが示されており、さらに後にDag Prawitzおよび高橋元男によって、任意の証明に対してその正規化が存在することが示されている。しかしこの場合も証明の正規化手続き自体が知られているわけではないので、存在する事実だけでは有限の立場とはみなされない。
関連項目

幾何学基礎論

ゲーデルの完全性定理

公理的集合論

証明論

数学基礎論

数理論理学

逆数学

外部リンク

Hilbert's Program （英語） - スタンフォード哲学百科事典「ヒルベルト・プログラム」の項目。

典拠管理データベース: 国立図書館

ドイツ