ヒルベルト・プログラム
出典: Wikipedio
|
|
ヒルベルト・プログラムとは、数学を形式化すること、すなわちその証明を形式化することで、数学全体の完全性と無矛盾性を示そうという試みのことをいう。詳しく言い換えれば、数学において真である命題は必ず証明できること、また公理から形式化された推論をどれだけ行っても、矛盾が示されることは絶対にないということを、有限の立場と呼ばれる確かな方法を用いて証明しようとする計画である。ダフィット・ヒルベルトによって唱えられた。ヒルベルトは、有名なヒルベルトの23の問題の2番目で、実数論の無矛盾性の証明を挙げている（よく自然数論の無矛盾性をさすものと誤解されている）。
1900年をはさんだ数年間に、数学の一部である集合論においていくつもの矛盾（パラドックスと呼ばれる。集合論の項を参照）が発見された。ヒルベルト・プログラムは、単にその矛盾を取り除くだけではなく、今後二度とこのような矛盾が現われないように、数学全体に確固とした基盤を与える目的があった。
この計画に大きな変化をもたらすことになったのが、クルト・ゲーデルによる不完全性定理（1930年）である。この定理は、大雑把に言って自然数論より強い理論では自己の無矛盾性を証明することが不可能であるとするものであった。ヒルベルト・プログラムでは自然数論だけでなく、実数論、さらには集合論全体の無矛盾性をも、自然数論のような基本的な体系の上で示すことを目的としていたため、この定理によって大きな修正を迫られることになった。
自然数論の無矛盾性については、その後、ゲルハルト・ゲンツェンによって、証明の正規化（カット消去）を用いることによって示された。この場合、証明の正規化手続きの終了性が、数学的帰納法では示し得ず、超限帰納法によってなされている。上記証明が有限の立場に立つと主張する人達は、手続きが実行可能である点をその根拠としているが、問題が手続きの終了性にあると考えた場合、十分とは云えない。
実数論に関しては、竹内外史により、高階述語論理における証明の正規化によって無矛盾性が証明されることが示されており、プラヴィッツ及び高橋元男によって、任意の証明に対してその正規化が存在することが示されているが、証明の正規化手続きが知られているわけではないので、実行可能性によっても有限の立場とはみなされない。
関連項目
外部リンク
Template:SEPcs:Hilbertův program de:Hilbertprogramm en:Hilbert's program fa:برنامه هیلبرت fr:Programme de Hilbert it:Programma di Hilbert nl:Programma van Hilbert pt:Programa de Hilbert sk:Hilbertov program zh:希尔伯特计划
