Roger Penrose is a smart guy. On pages 72 -75 of �Shadows of the Mind� 
you will find the clearest and simplest presentation of the Halting 
Theorem ever. What follows is loosely based on that.

Suppose there is a program A(n,m) that halts if program C_n does NOT 
halt on input m.  Suppose further that A(n,m) makes the correct decision 
except in the cases where this assumption results in a contradiction.

There is an associated predicate �C_n does not halt on m�. We can 
formalize it as  ~Halts(n, m). It is true iff A(n, m) halts.

We can write a program that investigates if a given program halts on itself:

C_k(n) {
     A(n, n)
     halt
}

C_k(n) above halts on n when C_n does not halt on n. If we pass k as a 
parameter to itself we have

C_k(k) {
     A(k, k)
     halt
}

That is if C_k halts on k then C_k does not halt on k. Duh?? After 
staring at this result in bewilderment for several minutes we realize 
that we have a contradiction on our hands. But above, we are passing a 
program as an argument to itself, so we can write:

C_s( void ) {
     A(k, k)
     halt
}

C_s() is attempting to say that it itself does not halt. It will not 
succeed because the assumption is that A() never obtains a falsehood or 
a contradiction.

It might seem we have to conclude that C_s(), C_k(k),  A(k,k) do not 
halt. Penrose says: �Thus our procedure A is incapable of ascertaining 
that this particular computation C_k(k) does not stop even though it 
does not.� . . . This is monumental nonsense.

Again, there is a predicate ~Halts(n, m) associated with A(n, m). Its 
semantics is defined as follows: ~Halts(n, m) is true iff A(n, m) 
determines that C_n does not halt on m. That is, ~Halts(n, m) is true 
iff A(n, m) halts:

A(n, m) halts    <==>    T(C_n(m) does not halt)
A(n, m) halts    <==>    T(~Halts(n, m))
The predicate associated with C_s() can be paraphrased as ~Halts(THIS, 
DONT_CARE) or �This does not halt�. It is true iff A() determines that 
C_k does not halt on k. But A() is unable to determine that. Therefore 
�This does not halt� is not true. And we obtain the following hierarchy:

This does not halt                                     ~T
�This does not halt� does not halt                      F
� �This does not halt� does not halt � does not halt    T

Therefore if a program A() as specified above does exist we will have 
the following results:

C_s()                        - not true that it halts
C_k(s)                       - does not halt
A(k, s)                      - halts


Since C_k halts on s is equivalent to T(C_s does NOT halt) then C_k does 
not halt on s is equivalent to ~T(C_s does not halt):

   C_k halts on s     <==>    T(C_s does not halt)
~(C_k halts on s)    <==>   ~T(C_s does not halt)

Turing�s paradoxical construction shows that A() is UNABLE TO DETERMINE 
the truth value of �C_k(k) does not halt�. And since its truth value is 
defined by what A() can determine, there is no truth value � and A() is 
able to determine that much.


-- 
X.Y. Newberry

If Jack says �What I am saying at this very moment is not true�, we can 
successfully and truly assert that he did not utter a truth: �What Jack 
said is not true�. But it is hardly conceivable that Jack�s utterance is 
true by virtue of its success in attributing non-truth to itself.

Haim Gaifman