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