Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!iuvax!purdue!haven!mimsy!frabjous.cs.umd.edu!nau
From: nau@frabjous.cs.umd.edu (Dana Nau)
Newsgroups: comp.ai
Subject: Re: Comments on "The Emperor's New Mind
Message-ID: <26776@mimsy.umd.edu>
Date: 29 Sep 90 22:31:57 GMT
References: <47000003@uxa.cso.uiuc.edu> <47000004@uxa.cso.uiuc.edu> <24793@dartvax.Dartmouth.EDU>
Sender: news@mimsy.umd.edu
Reply-To: nau@frabjous.cs.umd.edu (Dana Nau)
Organization: U of Maryland, Dept. of Computer Science, Coll. Pk., MD 20742
Lines: 55

In article <24793@dartvax.Dartmouth.EDU> phil@eleazar.dartmouth.edu (Phil Bogle) writes:
<    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.

Let T be the first-order theory in which G is stated.  The "meaning"
and "truth" of G depend not on T alone, but also on the model we use
for T.  In fact, the truth of any statement in T is defined only by
reference to the model.  

Loosely speaking, a model for T is an assignment of meanings to the
formulas of T in such a way that every statement that is provable in T
is true in the model.  This is the reverse of the way the word "model"
is used in mathematical modeling: there, the model is a mathematical
theory that represents some real-world phenomena, but here, the model
is instead the set of real-world (or unreal-world!)  phenomena that
the theory represents.

When logicians define a first-order theory T, they will usually have
some particular model in mind for T---and in this case, the intended
meaning for G is "G is not provable".  But in general, there may be
infinitely many other models for T, and in many of these, G will have
other meanings entirely.  Any statement that is provable in T is true
in every model of T, and vice versa---so since neither G nor ~G is
provable in T, this means that there are some models of T in which G
is true, and some models of T in which G is false.  Of course, in
those models in which G is false, the meaning of G is something other
than "G is not provable."
--
	Dana S. Nau
	Computer Science Dept.		Internet:  nau@cs.umd.edu
	University of Maryland		UUCP:  uunet!mimsy!nau
	College Park, MD 20742		Telephone:  (301) 405-2684