ヒルベルトのプログラム

数学において、1920年代初頭にドイツの数学者ダフィット・ヒルベルトによって定式化されたヒルベルト・プログラム^{[ 1 ]}は、数学の基礎を明確にしようとする初期の試みがパラドックスや矛盾を抱えていることが判明した際に、数学の基礎的危機に対する解決策として提案されたものでした。解決策として、ヒルベルトは既存のすべての理論を有限かつ完全な公理系に基礎づけ、これらの公理が矛盾しないことを証明することを提案しました。ヒルベルトは、実解析のようなより複雑なシステムの矛盾性は、より単純なシステムによって証明できると提案しました。最終的には、すべての数学の矛盾性は基本的な算術に還元できるとしました。

1931年に発表されたゲーデルの不完全性定理は、ヒルベルトの計画が数学の重要な分野において達成不可能であることを示した。第一定理において、ゲーデルは、計算可能な公理系を持ち、算術を表現できる無矛盾な体系は決して完全ではないことを示した。すなわち、真であることが証明できる命題を構成することは可能だが、その命題は体系の形式的な規則からは導き出せないということである。第二定理において、ゲーデルは、そのような体系は自身の無矛盾性を証明できないため、より強力な体系の無矛盾性を確実に証明するために用いることは決してできないことを示した。これは、有限体系は自身の無矛盾性を証明でき、したがって他のすべてを証明できるわけではないというヒルベルトの仮定を否定するものである。

ヒルベルトのプログラムの主な目的は、あらゆる数学に確固たる基礎を提供することであった。具体的には、以下の点が含まれるべきである。

• すべての数学を定式化すること。言い換えれば、すべての数学的命題は、厳密な形式言語で記述され、明確に定義された規則に従って操作されるべきである。
• 完全性：すべての真の数学的命題がその形式体系で証明できることの証明。
• 一貫性：数学の形式体系において矛盾が生じないことの証明。この一貫性証明は、有限な数学的対象に関する「有限主義的」推論のみを用いることが望ましい。
• 保存則：非可算集合などの「理想対象」に関する推論を用いて得られた「実対象」に関するあらゆる結果は、理想対象を用いずに証明できるという証明。
• 決定可能性：あらゆる数学的命題の真偽を判定するためのアルゴリズムが存在するべきである。

クルト・ゲーデルは、ヒルベルトのプログラムの目標のほとんどが、少なくとも最も明白な解釈では達成不可能であることを示した。ゲーデルの第二不完全性定理は、整数の加算と乗算を符号化するのに十分な力を持つ無矛盾な理論は、自身の無矛盾性を証明できないことを示している。これはヒルベルトのプログラムに対する課題となる。

• 形式体系においてすべての数学的真命題を形式化することは不可能である。なぜなら、そのような形式化を試みると、必ずいくつかの数学的真命題が欠落してしまうからである。計算可能な列挙可能な公理系に基づく、ペアノ算術の完全かつ一貫した拡張は存在しない。
• ペアノ算術のような理論は、自身の無矛盾性さえ証明できないのだから、その限定された「有限主義的」部分集合が、集合論のようなより強力な理論の無矛盾性を証明することは到底不可能である。
• ペアノ算術のいかなる無矛盾な拡張においても、命題の真偽（または証明可能性）を判定するアルゴリズムは存在しない。厳密に言えば、この判定問題に対する否定的な解決策は、ゲーデルの定理から数年後に現れた。なぜなら、当時はアルゴリズムの概念が正確に定義されていなかったからである。

証明論や逆数学など、数理論理学における現在の多くの研究分野は、ヒルベルトの当初のプログラムの自然な継続と見なすことができる。その多くは、目標を少し変更することで救済可能であり（Zach 2005）、以下の修正を加えることで、その一部は成功裏に完了した。

• すべての数学を形式化することは不可能だが、人々が日常的に使用する数学のほぼすべてを形式化することは可能である。特に、ツェルメロ＝フレンケル集合論と一階述語論理を組み合わせることで、現代のほぼすべての数学に対して、満足のいく、そして広く受け入れられている形式体系が得られる。
• ペアノ算術を少なくとも表現できるシステム（あるいは、より一般的には、計算可能な公理系を持つシステム）の完全性を証明することは不可能ですが、他の多くの興味深いシステムについては、完全性の形式を証明することが可能です。完全性が証明されている非自明な理論の例として、与えられた標数の代数的閉体の理論が挙げられます。
• 強理論の有限無矛盾性証明が存在するかどうかという問いに答えるのは難しい。主な理由は、「有限証明」の一般的に受け入れられている定義が存在しないからである。証明論のほとんどの数学者は、有限数学はペアノ算術に含まれると考えているようで、この場合、十分に強い理論の有限証明を与えることは不可能である。一方、ゲーデル自身は、ペアノ算術では形式化できない有限方法を用いて有限無矛盾性証明を与える可能性を示唆しており、どのような有限方法が許容されるかについて、より寛容な見解を持っていたようである。数年後、ゲンツェンはペアノ算術の無矛盾性証明を与えた。この証明の中で明らかに有限ではない唯一の部分は、順序数ε ₀までのある種の超限帰納法であった。この超限帰納法を有限方法と認めれば、ペアノ算術の無矛盾性の有限証明が存在すると主張できる。竹内嘉紀らによって、より強力な二階算術の部分集合の無矛盾性証明が与えられており、これらの証明がどれほど有限的あるいは構成的であるかについては、再び議論の余地がある。（これらの方法によって無矛盾性が証明された理論は非常に強力であり、ほとんどの「通常の」数学が含まれる。）
• ペアノ算術における命題の真偽を判定するアルゴリズムは存在しないが、そのようなアルゴリズムが発見されている興味深く非自明な理論は数多く存在する。例えば、タルスキは解析幾何学における任意の命題の真偽を判定できるアルゴリズムを発見した（より正確には、実閉体理論が判定可能であることを証明した）。カントール＝デデキントの公理を前提とすれば、このアルゴリズムはユークリッド幾何学における任意の命題の真偽を判定するアルゴリズムとみなすことができる。ユークリッド幾何学を自明な理論と考える人はほとんどいないため、これは重要なことである。

• 数学の基礎
• 数学の基礎的危機

• G. ゲンツェン、1936/1969 年。 Die Widerspruchfreiheit der Reinen Zahlentheorie。数学アンナレン112:493–565。ゲルハルト・ゲンツェンの論文集、ME Szabo (編)、1969 年に「算術の一貫性」として翻訳。
• D. ヒルベルト「初等数論の基礎づけ」『数学年報』 104:485–94。W. エヴァルト訳『初等数論の基礎づけ』、 マンコス編『ブロウワーからヒルベルトへ：1920年代の数学の基礎づけに関する議論』オックスフォード大学出版局、ニューヨーク、266–273頁。
• SG Simpson、1988年。「ヒルベルトのプログラムの部分的実現（pdf）」。Journal of Symbolic Logic 53:349–363。
• R. Zach、2006年。「ヒルベルトのプログラム：過去と現在」。『論理哲学』 5:411–447、arXiv:math/0508572 [math.LO]。

• リチャード・ザック。「ヒルベルトのプログラム」。エドワード・N・ザルタ編『スタンフォード哲学百科事典』所収。ISSN 1095-5054。OCLC 429049174。