停止性問題
ゆえに、任意のプログラム 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 では証明も反証もできない文が存在しなければならない。
以上の証明の停止性問題を再帰的でない任意の再帰的可算集合に置き換えることができる。例えば停止性問題の代りにラムダ計算の正規化可能性問題や述語論理の証明可能性問題を用いてもよい。
停止性問題を解くプログラムHが存在すると仮定して矛盾を導く。証明は嘘つきのパラドックスに類似している。
M(A)を、H(A,A)=YESならM(A)自身は停止せず、H(A,A)=NOなら0を出力してM(A)を停止するプログラムとする。(H(A,A)と無限ループを組み合わせる事でM(A)を作る事ができる。)
M(M)は停止するだろうか?
M(M)が停止したとすると、Mの定義よりH(M,M)=NO。Hの定義より H(M,M)=NOとなるのはM(M)が停止しないときのみなので、矛盾。
M(M)が停止しないとすると、Mの定義よりH(M,M)=YES。Hの定義より、H(M,M)=YESとなるのはM(M)が停止するときのみなので、矛盾。
よって停止性問題を解くプログラムHは存在しない。