不完全性定理との関係
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/11 15:10 UTC 版)
停止性問題の決定不能性を利用してゲーデルの第一不完全性定理を示すことができる。 計算模型を適当に算術化すれば、「プログラム M は入力 x のもとで停止する」という述語 Halt(M,x) がΣ1述語となるようにできる。停止性問題の決定不能性はこの述語がΠ1述語でないことを述べている。したがって「プログラム M は入力 x のもとで停止しない」という述語はΠ1であるがΣ1でない。 述語論理を適当に算術化しておく。T をロビンソン算術を含む再帰的かつΣ1健全な理論とする。ここで T が再帰的とは、「x は T の公理のコードである」という述語が再帰的であることをいう。また T がΣ1健全とは、偽なΣ1文を証明しないことをいう。「x は T で証明可能な論理式のコードである」という述語 Pr(x) は再帰的可算であり、したがってΣ1述語である。 T が任意のΠ1文を証明または反証すると仮定して矛盾を導く。述語 Halt(M,x) を定義するΣ1論理式 halt(M,x) を取る。ここで ¬halt(M,x) は T 上でΠ1論理式であることに注意せよ。T はΣ1完全かつ無矛盾であるからΠ1健全である。仮定より T は任意のΠ1文を証明または反証するので、T はΠ1完全である。ゆえに、任意のプログラム M と入力 x について、以下は同値である： ¬Halt(M,x) が成り立つ ¬halt(M,x) は T で証明可能である Pr(¬halt(M, x)) が成り立つ ところで Pr(¬halt(M, x)) はΣ1述語だから、¬Halt(M,x) もΣ1述語である。これは上に述べたことと矛盾する。 この証明は直観的には次のような意味である。もし T が任意の文を証明または反証するならば、Tの定理を枚挙するプログラムを走らせて halt(M,x) または ¬halt(M,x) の形の定理が現れたらYESかNOを出力して停止する、という方法で停止性問題が肯定的に解けてしまう。（このプログラムの正当性は T のΣ1健全性とΠ1健全性、プログラムの停止性は任意の文を証明または反証するという仮定によって保証される。）これは停止性問題の決定不能性に反するので、 T では証明も反証もできない文が存在しなければならない。 以上の証明の停止性問題を再帰的でない任意の再帰的可算集合に置き換えることができる。例えば停止性問題の代りにラムダ計算の正規化可能性問題や述語論理の証明可能性問題を用いてもよい。
※この「不完全性定理との関係」の解説は、「停止性問題」の解説の一部です。
「不完全性定理との関係」を含む「停止性問題」の記事については、「停止性問題」の概要を参照ください。
- 不完全性定理との関係のページへのリンク
