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!cbosgd!ukma!psuvm.bitnet!psuvax1!burdvax!sdcrdcf!hplabs!oliveb!glacier!kestrel!ladkin
From: ladkin@kestrel.ARPA
Newsgroups: net.ai,net.philosophy
Subject: Re: A halting problem
Message-ID: <4101@kestrel.ARPA>
Date: Mon, 20-Jan-86 19:19:48 EST
Article-I.D.: kestrel.4101
Posted: Mon Jan 20 19:19:48 1986
Date-Received: Wed, 22-Jan-86 05:33:26 EST
References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA> <438@faron.UUCP>
Distribution: net
Organization: Kestrel Institute, Palo Alto, CA
Lines: 73
Xref: watmath net.ai:3199 net.philosophy:3870

(Silverman)
> > > 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.

(Ladkin)
> > False.

(Silverman)
> I should have said "any sufficiently rich axiomatic system".

I agree.

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

(Ladkin)
> > False.

Still false. Any comments on what is meant?

(Silverman)
> > >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.

(Ladkin)
> > No argument has been provided in this discussion for the undcidability
> > of the detection of infinite loops, as a special case of
> > non-termination.
> > [..........]
> > I would like to see such an argument. First step would be,
> > to define which class of machines one is talking about.

I would still like to see the argument. Most people in
this discussion have been proceeding as if it were obvious.
I don't think it is obvious.

(Silverman)
> An isomorphism defines a map from one structure to another that is
> into and onto.

Add: ... and of the same similarity type. Hence my statement:

(Ladkin)
> > What operations or predicates on strings are being referred to?

(Silverman)
> 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).

This is fundamentally confused. *Structure* is a term of which
the definition may be found in any text on mathematical logic,
and to which this suggestion doesn't correspond.
It would help to have a definition of the two structures, and the
precise map between them, that is being suggested.

I would guess, from the rest of the paragraph, which I won't
reproduce, that you may be confusing *countable* and *isomorphic*?
If not, my apologies. But it isn't clear without careful
definition.

Peter Ladkin
ladkin@kestrel