ゲーデルの不完全性定理と計算

ゲーデルの不完全性定理は、十分に強力で無矛盾な形式体系には、証明できない真の命題が含まれることを示しており、これは計算可能性理論で発見された決定不能性と深く関連する結果である。

Definition

不完全性定理は、基本的な算術を表現できる任意の無矛盾な形式体系は不完全であり、証明できない真の算術命題を含み、自身の無矛盾性を証明できないと述べている。計算論的には、証明可能な命題の集合は認識可能であるが、その補集合は認識不可能であり、決定不能性を反映している。

Scope

このトピックでは、第一および第二不完全性定理、算術化とゲーデル数化による自己言及の技法、不完全性と停止問題および一階述語論理の決定不能性との密接な関係、そして形式的推論と自動証明の限界に対するその影響について扱う。

Core questions

• なぜ、いかなる無矛盾で十分に強力な形式体系も、すべての真の算術命題を証明できないのか？
• ゲーデル数化による自己言及は、どのようにして証明不可能な真の文を生み出すのか？
• 不完全性と停止問題の決定不能性は、どのようにして一つの現象の二つの側面と見なされるのか？
• 不完全性は自動定理証明の限界に対して何を意味するのか？

Key theories

第一不完全性定理

算術を符号化するのに十分強力な任意の無矛盾な形式体系には、それ自身が証明できない、あるいは反証できない真の命題が含まれる。これは、実質的に自身の証明不可能性を主張する文によって構成される。

計算可能性を通じた不完全性

不完全性は停止問題の決定不能性から導かれる。もしすべての算術的真理が証明可能であれば、証明を探すことによって停止性を決定できることになるが、これは決定不能な問題の存在が証明不可能な真理の存在を強制することを示している。

Clinical relevance

不完全性とその計算論的対応物は、自動推論に厳格な限界を課す。いかなるアルゴリズムもすべての算術的真理を決定したり、すべての数学的問題を解決したりすることはできないため、定理証明器や検証システムは、完全な自動決定ではなく、人間の指導、制限された理論、または対話型証明に依存する必要がある。

History

ゲーデルは1931年に不完全性定理を証明し、数学の完全で自己正当化される形式化というヒルベルトの希望を打ち砕いた。5年以内にチャーチとチューリングはこれらの限界を決定不能性と結びつけ、停止問題を通じた不完全性の計算論的解釈は計算可能性理論の主要な要素となった。

Key figures

• Kurt Gödel
• Alan Turing
• Alonzo Church
• John Barkley Rosser

Seminal works

• godel1931
• boolos2007

Frequently asked questions

不完全性定理は数学が破綻していることを意味するのか？

そうではない。それは、単一の無矛盾な形式体系がすべての算術的真理を証明できるわけではないことを意味するのであって、数学が無矛盾でないとか信頼できないということではない。数学者は形式体系の中や間で作業しており、不完全性定理は、特定の固定された体系が捉えられるものに内在する限界を示すに過ぎない。

ゲーデルの定理は停止問題とどのように関連しているのか？

両者は密接に関連している。停止問題の決定不能性は不完全性を意味する。もし形式体系がどのプログラムが停止するかについてのすべての真理を証明できるとすれば、証明を探すことによって停止性を決定できることになり、これはチューリングの結果と矛盾する。両者は、論理と計算において、形式的手法の同じ根本的な限界を表現している。