Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.3 alpha 4/15/85; site kestrel.ARPA
Path: utzoo!watmath!clyde!burl!ulysses!mhuxr!mhuxt!houxm!vax135!cornell!uw-beaver!tektronix!hplabs!oliveb!glacier!kestrel!ladkin
From: ladkin@kestrel.ARPA
Newsgroups: net.ai,net.philosophy
Subject: Re: A halting problem
Message-ID: <4024@kestrel.ARPA>
Date: Fri, 17-Jan-86 17:11:35 EST
Article-I.D.: kestrel.4024
Posted: Fri Jan 17 17:11:35 1986
Date-Received: Mon, 20-Jan-86 04:57:25 EST
References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA> <436@faron.UUCP>
Distribution: net
Organization: Kestrel Institute, Palo Alto, CA
Lines: 68
Xref: watmath net.ai:3193 net.philosophy:3838

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. 

False. The theory of dense linear orders without endpoints is a 
counterexample. So is the theory of equality with the single axiom
(forall x and y)(x = y). Etc, etc.
Goedel's theorem talks about first-order theories that include
sufficiently much about arithmetic. For details, see the Handbook
of Mathematical Logic, or Tarski, Mostowski and Robinson's
*Undecidable Theories*

> One interesting aspect of
> the whole business is the fact that we can never know when in fact a problem
> is undecidable. 

False. There are many sets which are recursively enumerable but not
recursive. This means that membership in such a set is undecidable
in general. The set of all theorems of first-order logic is such a
set (provided there is at least one non-monadic predicate in the 
language).

>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.

No argument has been provided in this discussion for the undcidability
of the detection of infinite loops, as a special case of 
non-termination. It's only in finite state machines, or 
machines with finitely-bounded storage that you get pumping-lemma
type results. (It's a consequence of the pumping lemma for
finite-state machines that any non-terminating computation
necessariliy involves an infinite loop).

I would like to see such an argument. First step would be,
to define which class of machines one is talking about.

>  
> 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.
>  

Isomorphism is a notion applied to structures with operations on them,
and predicates.
What is the notion of isomorphism of languages being referred to?
What operations or predicates on strings are being referred to?
Notice that the semantics for a language of first-order logic,
and the semantics of a procedural language like Pascal are
incomparable. Others may not be. One probably needs to define
the class of languages being talked about.

A further reference - the discussion about minds being or not
being Turing machines has been going on for a very long time.
There is an old collection of papers published by Prentice-Hall
called *Minds and Machines*. There is a philosopher at Oxford,
Merton College, John ......? who has argued for a long time
that the mind is not a Turing Machine. Hubert Dreyfus has 
argued this, amongst other, stronger claims for many years,
in semi-public.

Peter Ladkin
ladkin@kestrel.arpa