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!genrad!panda!talcott!harvard!bbnccv!bbncca!linus!faron!bs
From: bs@faron.UUCP (Robert D. Silverman)
Newsgroups: net.ai,net.philosophy
Subject: Re: A halting problem
Message-ID: <438@faron.UUCP>
Date: Sun, 19-Jan-86 14:04:43 EST
Article-I.D.: faron.438
Posted: Sun Jan 19 14:04:43 1986
Date-Received: Tue, 21-Jan-86 07:25:35 EST
References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA> <436@faron.UUCP> <4024@kestrel.ARPA>
Distribution: net
Organization: The MITRE Coporation, Bedford, MA
Lines: 88
Xref: watmath net.ai:3197 net.philosophy:3858

> 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 

I should have said "any sufficiently rich axiomatic system". As such the
			-----------------
statement is true. As for 'sufficiently much about arithmetic' Peano arithmetic
qualifies. Constructs in programming languages satisfy Peano arithmetic.
 
 
An isomorphism defines a map from one structure to another that is
into and onto. Thus both the map and its inverse are one-to-one. You
may label any countable set of theorems via Goedel numbering, i.e. 
assigning to each axiom a prime number and then using the fundamental
theorem of arithmetic to represent a formal proof as the product of
primes (axioms) in a unique way. One can number the formal grammatical
rules of a programming language in the same way. In this case the
abstract structures are the axioms (or primitive statements of the programming
language) and the operator is the composition of those axioms (statements)
into formal theorems (programs).  The fact that the semantics are not comparable
is irrelevent. The mapping exists.
 
Bob Silverman