Định lý Rice

Không mất tổng quát giả sử hàm không xác định khắp nơi $\emptyset$ (tính bởi chương trình không bao giờ dừng ở đầu vào nào) không có tính chất $P$ — nếu không thì lập luận với tính chất bù $\lnot P$, tính chất này quyết định được đúng khi $P$ quyết định được. Vì $P$ không tầm thường, cố định một chương trình $e_0$ mà hàm $\varphi_{e_0}$ của nó có tính chất $P$.

Giả sử phản chứng $P$ quyết định được bởi thuật toán $D$ nào đó (cho một chỉ số chương trình, $D$ dừng và báo cáo đúng liệu hàm của chương trình đó có tính chất $P$ hay không). Ta quy về bài toán dừng bởi $P$, mâu thuẫn với Định lý 1.

Cho một cặp $(e,x)$ bất kỳ, xây dựng hiệu quả (bằng thao tác văn bản đơn giản — định lý s-m-n của Kleene) một chương trình mới $e'$ mà, với đầu vào $y$ bất kỳ: trước hết mô phỏng chương trình $e$ chạy trên đầu vào $x$; nếu mô phỏng đó dừng, thì $e'$ tiếp tục mô phỏng chương trình $e_0$ trên đầu vào $y$ và cho ra bất cứ gì nó cho ra.

Xét hai khả năng. Nếu $e$ dừng ở $x$: mô phỏng $e$ trên $x$ kết thúc, nên $e'$ sau đó hành xử y hệt $e_0$ ở mọi đầu vào, tức $\varphi_{e'}=\varphi_{e_0}$ — hàm này có tính chất $P$ (vì $P$ ngữ nghĩa, chỉ phụ thuộc hàm được tính, và $\varphi_{e_0}$ có $P$). Nếu $e$ không dừng ở $x$: mô phỏng $e$ trên $x$ không bao giờ kết thúc, nên $e'$ không bao giờ tới bước mô phỏng $e_0$ ở bất kỳ đầu vào $y$ nào; do đó $\varphi_{e'}$ là hàm không xác định khắp nơi $\emptyset$, theo giả định không có tính chất $P$.

Vậy: $e$ dừng ở $x$ $\iff$ $\varphi_{e'}$ có tính chất $P$ $\iff$ $D(e')$ trả lời "có". Vì $(e,x)\mapsto e'$ tính được, thuật toán "tính $e'$ từ $(e,x)$, rồi chạy $D(e')$" sẽ quyết định được bài toán dừng — mâu thuẫn Định lý 1. Vậy không tồn tại $D$ như thế: $P$ không quyết định được. $\blacksquare$