🚀 go-pugleaf

In article <2362@sphinx.uchicago.edu>, hin9@sphinx.uchicago.edu (The Reverend w. No Name) writes:

> [from] What is the Name of This Book?, by Raymond Smullyan.
> 
>      'This Sentence is Unprovable in System S.'
> 
>      If it's false, it is provable in system S, which is impossible unless
> S is inconsistent.  Therefore, it is true.  Therefore, it is unprovable
> in system S.

This is the standard approach, as taken by Godel. I've always found
it a bit on the tricky side, though, and therefore harder to figure
out than the following approach (which must have been discovered by
people other than me too, though I don't know any references):

   1) Insert standard proof that no algorithm can determine whether
      a given algorithm terminates in all cases. (HALTING PROBLEM)

   2) Formal systems of logic, mathematics, etc. all come with an
      algorithm for determining whether a proof is valid. There is
      always a countably infinite number of proofs.

   3) For any formal system there is an algorithm that will terminate
      with "yes" if a given statement is a theorem. It just needs to
      check each possible proof in turn.

   4) Any interestingly comprehensive formal system of logic is
      capable of expressing such statements as "Algorithm X does
      not terminate".

   5) No interesting formal system is both correct and complete. If
      it were, you could solve the halting problem by just searching
      for proofs of "Algoritm X terminates" and "Algorithm X does not
      terminate" and announcing the result when you find one or
      the other.

This proof makes it much clearer than the standard one that the
"problem" applies to any system that could be considered "formal".
It also avoids the tricky self-reference stuff, though there's a
bit of that in the proof of the halting problem itself.

    Radford Neal
    The University of Calgary