Path: utzoo!attcan!utgpu!watserv1!maytag!watdragon!violet!cpshelley
From: cpshelley@violet.uwaterloo.ca (cameron shelley)
Newsgroups: comp.ai
Subject: Re: Comments on "The Emperor's New Mind
Message-ID: <1990Sep30.163813.13039@watdragon.waterloo.edu>
Date: 30 Sep 90 16:38:13 GMT
References: <47000003@uxa.cso.uiuc.edu> <47000004@uxa.cso.uiuc.edu> <24793@dartvax.Dartmouth.EDU>
Sender: daemon@watdragon.waterloo.edu (Owner of Many System Processes)
Organization: University of Waterloo
Lines: 71

[stuff deleted]

>Let me try something: I'm going to restate Douglas Hofstadters presentation in
>_Goedel, Escher, Bach_ but in the notation of Computer Science rather than
>Mathematics.
>
>***
>
>For each expression or list of expressions in a system, assume that we
>can find a unique number to represent that expression, called the Goedel Number
>or GN for that expression.  This gives the system a way to "talk about itself";
>a formula can talk about other formulas by referring to them by their Goedel
>number.
>
>   In particular, we can capture the notion of provability.   It's
>hardly surprising that the steps of a formal derivation can be formally
>checked; that's the whole point of such a system.  Given the Goedel
>number of a derivation, we can create an expression which arithmetically
>"parses" the derivation and checks that each step follows from the
>previous ones by the axioms of the system.
>
>      Let this expression be called PROVES, and let us write "d PROVES y" if
>this expression evaluates to true for a given derivation d and if y is the
>conclusion of that derivation.  (PROVES will be an enormous expression with
>two free variables to be filled in by d and y) This is the first
>important step, the system can now talk about the provability of
>sentences within itself.
>
>    Now, we need to have a way for G to talk about itself without being
>viciously recursive.  G will actually talk about another formula, which
>when slightly modified by the function below, will turn out to be G itself.
>
>    Let f be the GN of a function which has a single free variable x.
>(a free variable is like the parameter to a function; it is a place marker
>which will later be filled in with a definite value).
>
>    Define SelfSubstitution(f) = f with the GN for f substituted for each
>                                    occurance of x (the free variable)
>
> -- We'll now define "H", which is G's almost indentical twin.
>
>    Define H(x) = There does not exist a Derivation such that
>                     Derivation PROVES SelfSubstitution(x)
>
>    Let #H# be the GN for H.
>
>    Define G = There does not exist a Deriviation such that
>                   Derivation PROVES SelfSubstitution(#H#)
>
>But notice  ***G = SelfSubstitution(#H#)*** since is exactly the same as H
>with the GN for H substituted for the free variable x!

Sorry for excerpting so much of this posting, but I did not want to
destroy the substance of the arguement.  I just have one question:
does the G = SS(#H#) equation here look like the fixed point of a 
function to anyone?  It sure does to me...  If so, it seems like there
should be some other interesting parallels between the ideas of
provability and fixed points.

>    So what G is really saying is "There does not exist a Deriviation such that
>Deriveation proves G", or more concisely, "G is not provable".  If G can be
>proven, we have a contradiction, so G must not be provable.  So G is telling the
>truth--- G is true, but not provable.  Hence the system (or any other system)
>fails to capture all true statements.


--
      Cameron Shelley        | "Armor, n.  The kind of clothing worn by a man
cpshelley@violet.waterloo.edu|  whose tailor is a blacksmith."
    Davis Centre Rm 2136     |
 Phone (519) 885-1211 x3390  |				Ambrose Bierce