ライスの定理

一般性を失うことなく、いかなる入力に対しても決して停止しないプログラムが計算する至る所未定義の関数 $\emptyset$ が性質 $P$ を持たないと仮定する——そうでなければ、$P$ が決定可能であることとちょうど同値な補性質 $\lnot P$ で議論する。$P$ は非自明なので、その関数 $\varphi_{e_0}$ が性質 $P$ を持つプログラム $e_0$ を一つ固定する。

背理法で、$P$ がある判定アルゴリズム $D$ によって決定可能であると仮定する(プログラム索引が与えられると、$D$ は停止し、そのプログラムの関数が性質 $P$ を持つかどうかを正しく報告する)。$P$ に停止問題を還元し、定理1と矛盾させる。

任意の組 $(e,x)$ に対し、実効的に(単純な文字列操作——クリーネの s-m-n 定理により)新しいプログラム $e'$ を構成する。$e'$ は任意の入力 $y$ について:まずプログラム $e$ を入力 $x$ で実行するシミュレーションを行い、そのシミュレーションが停止したら、次にプログラム $e_0$ を入力 $y$ でシミュレーションしてその出力を出力する。

2つの場合を調べる。$e$ が $x$ で停止する場合:$e$ を $x$ で実行するシミュレーションは終了するので、$e'$ はその後すべての入力で $e_0$ とまったく同じように振る舞う、すなわち $\varphi_{e'}=\varphi_{e_0}$——これは性質 $P$ を持つ($P$ は意味論的なので計算される関数のみに依存し、$\varphi_{e_0}$ は $P$ を持つ)。$e$ が $x$ で停止しない場合:$e$ を $x$ で実行するシミュレーションは決して終わらないので、$e'$ はいかなる入力 $y$ についても $e_0$ のシミュレーション段階に決して到達しない。したがって $\varphi_{e'}$ は至る所未定義の関数 $\emptyset$ であり、仮定によりこれは性質 $P$ を持たない。

よって:$e$ が $x$ で停止する $\iff$ $\varphi_{e'}$ が性質 $P$ を持つ $\iff$ $D(e')$ が「はい」と答える。$(e,x)\mapsto e'$ は計算可能なので、「$(e,x)$ から $e'$ を計算し、$D(e')$ を実行する」というアルゴリズムは停止問題を決定してしまう——定理1と矛盾する。したがってそのような $D$ は存在しない:$P$ は決定不可能である。$\blacksquare$