IT用語集 › プログラミング › ゲーデルの不完全性定理

ゲーデルの不完全性定理

プログラミング Svenska → 更新: 2026-10-22

十分に強い形式体系には、証明できない真理があり、自分自身の無矛盾性すら保証できないことを示した1931年の証明。

クルト・ゲーデルは25歳でウィーンにおり、愛想のない題名『『プリンキピア・マテマティカ』および関連する体系の形式的に決定不能な命題について』の論文を発表した。第一定理は、算術を含むほど強く、無矛盾で、公理が機械的に列挙できる体系には、その体系内では証明も反証もできない命題が存在する、というもの。第二定理は、そのような体系は自らの無矛盾性を証明できない、というものだ。数学に最終的な土台を与えるはずだったヒルベルト・プログラムは、困難であるだけでなく不可能だと分かった。

受け継がれたのは手法である。ゲーデルは式に番号を振った。あらゆる命題が数になり、証明の各ステップが数同士の算術的関係になるので、体系は算術の外に出ずに自分自身について語れる。彼はその符号化のもとで「私は証明できない」と主張する命題を作った。証明できるなら偽で、体系は偽を証明することになる。証明できないなら真であり、かつ証明不能である。

同じ対角線論法は5年後に停止性問題として、またライスの定理、クワイン、静的解析が決して決着をつけられない結果すべてに再び現れる。ゲーデルは式を数として符号化し、ノイマン型の機械はプログラムを同じメモリにデータとして保存する。同じ一つの技法が、一方では証明に、もう一方では機械の構築に使われたのである。

← 用語集に戻る