停止性問題
プログラムAにデータxを入力して実行する、ということをA(x)と書き、A(x)がyを出力するときy=A(x)と書くことにする。
現代のコンピュータの使い方であれば、中身がプログラムであるバイナリの実行ファイルを、単なるデータファイルとして扱うこともできる、ということから、プログラムを、他のプログラムへの入力データにできる、ということは感覚的にわかる。また具体的には、エミュレータに実行ファイルを渡す、というのが一例である。チューリングは、「いかなるチューリングマシンをも模倣できるチューリングマシン」である「万能チューリングマシン」が可能であることを示し、模倣されるチューリングマシンはそのテープの初期状態に記述される、というようにして議論を進めた。
以下記号を簡単にする為、「データとしてのプログラムA」も、Aと書く。 よって例えばプログラムA、Bがあったとして、「A(B)」は、「プログラムAに、データとしてのプログラムBを入力として渡す」の意である。停止性問題とは、「プログラムAとデータxが与えられたとき、A(x)が停止するかどうかを決定せよ」という問題である。
また「停止性問題の決定不能性」とは、停止性問題を常に正しく解くプログラムは存在しない、ということである。 すなわち以下の性質を満たすプログラムHは存在しない。
全てのプログラムAと全てのデータxに対し、
A(x)の実行は停止する ⇒ H(A,x)はYESを出力する。
A(x)の実行は停止しない ⇒ H(A,x)はNOを出力する。
停止性問題の決定不能性を利用してゲーデルの第一不完全性定理を示すことができる。
計算模型を適当に算術化すれば、「プログラム 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完全である。
対角線論法は、集合Sからその冪集合P(S)への全単射が存在しない(カントールの定理)事を示す為にゲオルク・カントールが使った論法である。
実は上述の証明は対角線論法も利用している。以下簡単の為、プログラムの入力は全て自然数とする。前述したようにプログラムは0と1からなる数字で書き表せるので、プログラム全体の集合は自然数全体の集合 N {\displaystyle \mathbb {N} } と自然に同一視できる。本当は N {\displaystyle \mathbb {N} } の中にはプログラムに対応していないものもあるが、簡単の為その辺の事情は略する。
φ : N × N ↦ { 0 , 1 } {\displaystyle \phi :\mathbb {N} \times \mathbb {N} \mapsto \{0,1\}} を次のように定義する:
A(x)が停止すればφ(A,x)=1、そうでなければφ(A,x)=0。
以下φ(A,x)の事をφA(x)と定義する。 g : N ↦ { 0 , 1 } {\displaystyle g:\mathbb {N} \mapsto \{0,1\}} を、g(A)=¬φA(A)により定義する。ただしここで「¬」は0と1を反転する写像。すなわち¬0=1、¬1=0。
すると対角線論法により、g=φMとなるMは存在しない。
さて、仮に停止性問題を常に正しく解くプログラムHが存在するとする。M(A)を、H(A,A)=YESなら停止せず、H(A,A)=NOなら0を出力して停止するプログラムとすると、MとHの定義よりg=φMが成立し、矛盾。したがって停止性問題を常に正しく解くプログラムは存在しない。