A proof of Rice's theorem

We start with a particular language for expressing programs, and a particular alphabet in which programs and other strings are written. They are fixed.

Definition. Programs p and q are equivalent if they compute the same partial function.

Definition. A set of strings S is nontrivial if S is not the empty set and S does not contain all strings.

Definition. A set of programs S respects equivalence if, whenever programs p and q are equivalent, either both p and q are members of S or both p and q are nonmembers of S.

Rice's Theorem. Every nontrivial set of programs that respects equivalence is undecidable.

Proof.

Let S be a nontrivial set of programs that respects equivalence. We prove that S is undecidable. The reasoning is by contradiction. Presume that S is decidable. Then there must be a program called DECIDE that decides membership in S. Do decide has two properties.

1. phi_DECIDE(p) = yes whenever p is a member of S.
2. phi_DECIDE(p) = no whenever p is not a member of S.

Write a program called LOOP that loops forever on all inputs. It is either in S or not. We can presume without loss of generality that LOOP is not in S. If LOOP is in S, then just look at the complement of S instead. The complement of S is decidable if and only if S is decidable.

S is nontrivial, so it must have a member. Choose any member of S, and call it GEORGE. Now we have one member of S (GEORGE) and one nonmember of S (LOOP).

In order to show that DECIDE does not work, we need to write two programs. The first has another program r built into it. For any r, you can build program Q_r. It goes like this.

Program Q_r(x)

1. Run the interpreter on input (r,r). This is equivalent to running program r on itself.

2. Run program GEORGE on input x, and produce the same result that GEORGE does.

Observation Q1.  For every r:

phi_r(r) terminates
   => Q_r is equivalent to GEORGE
   => Q_r is a member of S

Observation Q2.  For every r:

phi_r(r) does not terminated
   => Q_r is equivalent to LOOP
   => Q_r is not a member of S

Now write a second program called FOOL as follows.

FOOL(r)

1. Build program Q_r by building parameter r into Q.

2. Run DECIDE on input Q_r, and call its answer y. (We are asking DECIDE whether Q_r is in S.)

3. If y = "yes" then loop forever, else stop.

Now we are ready to prove that DECIDE does not get the correct answer on every input. That is the contradiction that we are looking for (since we presumed that DECIDE got the right answer on every input.) Once the following claim is proved, we are done.

Claim. DECIDE gets the wrong answer on input Q_FOOL.

Proof of the claim. Imagine running FOOL on input FOOL. The following are evident.

phi_DECIDE(Q_FOOL) = "yes"
   => phi_FOOL(FOOL) does not terminate  [by inspecting the definition of FOOL]
   => Q_FOOL is not a member of S  [by observation Q2]

So if DECIDE answers yes on input Q_FOOL, it got the wrong answer. (The correct answer is no, since Q_FOOL is not a member of S.)

phi_DECIDE(Q_FOOL) = "no"
   => phi_FOOL(FOOL) terminates  [by inspecting the definition of FOOL]
   => Q_FOOL is a member of S  [by observation Q1]

So if DECIDE answers no on input Q_FOOL, it got the wrong answer. (The correct answer is yes, since Q_FOOL is a member of S.)

Regardless of what answer DECIDE gives on input Q_FOOL, the answer is wrong.

END OF PROOF

Remark. Program Q_r needs to be constructed by program FOOL. One mechanism for doing that is to use parameter fixing. Write Q as a program with two parameters, rr and x. Then what FOOL needs to do is fix the parameter rr to the value of FOOL's parameter r. That can be done by the computable function that fixes a parameter of a program to some particular value. That is, we use function PARAM where phi_PARAM(Q,r) = T where phi_T(x) = Q(r,x). That is, PARAM has fixed the first parameter of Q to a given value, r, yielding new program T.