コンビネータ論理
もし2つのNA=TとNB=Fを満たすような2つの引数A,Bが存在するとき、その述語Nは非自明であるという。また、NMがいかなる引数Mについても正規形をしているとき、そしてその時に限り述語Nが完全であるという。ライスの定理の例は、全ての完全な述語は自明であると述べている。この定理の証明はかなり単純である。
証明:背理法による。完全で非自明な述語の存在を仮定し、N と呼ぶことにする。
Nは非自明であるから以下を満たすコンビネータA,Bが存在する。
(N A) = T (N B) = F
Define NEGATION ≡ λx.(if (N x) then B else A) ≡ λx.((N x) B A) Define ABSURDUM ≡ (Y NEGATION)
不動点定理により、 ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM) を満たすABSURDUM = (NEGATION ABSURDUM)が与えられる。
Nは完全であるから以下の2つのうちどちらかを満たす。
(N ABSURDUM) = F
(N ABSURDUM) = T
場合1: F = F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T これは矛盾である。
場合2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F これもまた矛盾である。
故に、 (N ABSURDUM) は真であっても偽であってもNが完全で非自明な述語であることに反する。QED。