Path: utzoo!attcan!uunet!bu.edu!dartvax!eleazar.dartmouth.edu!phil
From: phil@eleazar.dartmouth.edu (Phil Bogle)
Newsgroups: comp.ai
Subject: Re: Comments on "The Emperor's New Mind
Message-ID: <24793@dartvax.Dartmouth.EDU>
Date: 29 Sep 90 17:21:55 GMT
References: <47000003@uxa.cso.uiuc.edu> <47000004@uxa.cso.uiuc.edu>
Sender: news@dartvax.Dartmouth.EDU
Organization: Dartmouth College, Hanover, NH
Lines: 71

igl@ecs.soton.ac.uk (Ian Glendinning) writes:

>The Goedel argument actually runs something like:
>G: There is no proof of G in this system.

In article <47000004@uxa.cso.uiuc.edu> xhg0998@uxa.cso.uiuc.edu writes:
>
>What is G in Goedel's theorem's case? The very definition of G involves
>recursing reference to itself and is therefore not defined. If you plug
>anything specific into G, then the definition of G does not hold any more.

G is not so wickedly recursive as it seems. We actually could compute it and
write it down on a (very large) sheet of paper;  it would be a huge expression
involving lots of existential quantifiers and ANDs and ORs, but there would be
no recursive definitions and no free variables.

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!

    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.