Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site faron.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!bellcore!decvax!linus!faron!bs
From: bs@faron.UUCP (Robert D. Silverman)
Newsgroups: net.ai,net.philosophy
Subject: Re: A halting problem
Message-ID: <436@faron.UUCP>
Date: Thu, 16-Jan-86 23:43:45 EST
Article-I.D.: faron.436
Posted: Thu Jan 16 23:43:45 1986
Date-Received: Sat, 18-Jan-86 08:12:31 EST
References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA>
Distribution: net
Organization: The MITRE Coporation, Bedford, MA
Lines: 49
Xref: watmath net.ai:3183 net.philosophy:3807

> The question of whether or not people are capable of solving the
> Halting problem in general (which, as people have abundantly shown, is
> equivalent to solving your favorite outstanding mathematical problem)
> does not seem amenable to a rational answer. Sure there are hard
> problems, but cleverer people pop up over the centuries and solve some
> of the outstanding problems, but then the remaining problems are
> harder, etc.  I suspect that I at least am not capable of solving
> every problem (such humility).
> 
> The REAL question for me is whether the following is correct reasoning:
> 
> Premise 1: No Turing machine will solve the Halting problem for every
> input.
> 
> Premise 2:  The human "race" is equivalent (in problem solving power)
> to a Turing machine.
> 
> Consequent (?): There is some PARTICULAR input for which the human
> race can never solve the Halting problem.
> 
> If so, and one believes premise 2, can we construct such an unsolvable
> problem, in finite time, and then get on with life?
> 
> Currently we have an ineffective algorithm for finding the unsolvable
> problem, should it exist, namely: work on problems, and if no one ever
> solves one, then that one is unsolvable. But can we find out before
> forever?
> 
> -tom

Goedel's Theorem establishes that in ANY finite axiomatic system there are
problems which are undecidable. That is to say there exist formal theorems
that are true but cannot be proved. Thus there DO exist problems which we
can never solve. In fact the proof of Goedel's theorem uses the same exact
technique used to establish the halting problem. One interesting aspect of
the whole business is the fact that we can never know when in fact a problem
is undecidable. Similarly there does not even exist an algorithm which
scans a computer program and tells us whether another algorithm exists that 
would decide if it had an infinite loop.
 
Note further that any given, formally defined, computer language is 
isomorphic to a finite axiomatic system in that the number of 'theorems'
(programs) is at most countable. A theorem in a formal system is just
a finite string of symbols or axioms of that system. A computer program is
just a finite string of symbols from the programming language. They are
isomorphic.
 
 
Bob Silverman