Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site mmintl.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!bellcore!decvax!linus!philabs!pwa-b!mmintl!franka
From: franka@mmintl.UUCP (Frank Adams)
Newsgroups: net.ai,net.philosophy
Subject: Re: A halting problem
Message-ID: <1060@mmintl.UUCP>
Date: Tue, 21-Jan-86 02:04:28 EST
Article-I.D.: mmintl.1060
Posted: Tue Jan 21 02:04:28 1986
Date-Received: Fri, 24-Jan-86 21:26:52 EST
References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA> <436@faron.UUCP>
Reply-To: franka@mmintl.UUCP (Frank Adams)
Distribution: net
Organization: Multimate International, E. Hartford, CT
Lines: 22
Xref: watmath net.ai:3207 net.philosophy:3907

In article <436@faron.UUCP> bs@faron.UUCP (Robert D. Silverman) writes:
>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.

All right, I'll say it again.  This implication is not valid.  Insofar as
a problem is regarded as strictly a problem in a formal system, it can
(potentially) be solved by showing it is undecidable in that formal
system.  Insofar as the problem is regarded as really about integers or
real numbers or whatever, there are potential proof mechanisms which
cannot be constrained to any pre-selected formal system.

If one assumes Church's thesis, it then DOES follow that there problems
which we can never solve.  This result is more directly related to the
halting problem than to Goedel's Theorem (although these results are
indeed related).

Need I add that Church's thesis is quite controversial in some quarters?

Frank Adams                           ihpn4!philabs!pwa-b!mmintl!franka
Multimate International    52 Oakland Ave North    E. Hartford, CT 06108