From: centaur@terminus.gatech.edu (Anthony G. Francis)
Newsgroups: comp.ai.philosophy
Subject: Re: goedel and ai - correct version!!
Keywords: ai,goedel
Date: 6 Apr 92 22:12:17 GMT
Organization: Georgia Tech College of Computing

atten@phil.ruu.nl (Mark van Atten) writes:
>There is an ongoing discussion right now on mathematical realism in the ai
>group. Some people question the relevance of this to ai. In this article,
>I want to discuss
>1 The objective existence of mathematical objects
>2 The significance of this for ai

>II THE SIGNIFICANCE OF GOEDEL'S THEOREM FOR AI
>II.2 Penrose's argument
>Let F be a formal system, and G(F) an undecidable formula in F. (e.g., Con(F))
>Then Penrose's argument is this:
>The ***deduction*** of G(F) from F is true and valid, 
>we can ***see*** that. The important thing is that it is 
>the deduction is seen to be valid, while it is
>not formalizable (is that correct English?).
>Perhaps mathematical intuition cannot see ALL of true math. (Goedel thinks it
>can, however), but that doesn't matter for this argument: there is at least
>one math. truth that can not be formalized and hence, is not algorithmic.
>It must be borne in mind that this is a question of principle. Probably no one
>will ever be able to compute the 10^10^10^10 digit 
>of pi, but in ***principle***, it is possible.
>Again: it is the fact that we see the validity of 
>Goedel's proof, not the truth
>of G(f); that is the difference with Lucas.

The deduction of G(F) is not formalizable from _within_ F, but that
does not mean that it is not formalizable at all. It is possible to 
devise a new formal system F', in which it is possible to prove truths 
_about_ F. From within F', it is possible to derive that G(F) is an 
undecideable formula within F, and that G(F) is true and valid. That is,
the validity of the deduction of G(F) from F can be determined in a 
formalizable way, even though this cannot be determined from within F.

Because of Godel's theorem, this new formal system F' will have limitations
of its own, namely, that there are statements in F' which are true and valid
but undecideable. This corresponds _precisely_ to your caveat about
mathematical intuition; if mathematical intuition cannot see ALL of true
math, it is exhibiting precisely the behavior we would expect it to _if_
the cognitive system of the mathematician is specifiable as a program.

Lest the sharp-witted tear into this conclusion with abandon, let me
clarify. If the Strong AI thesis is true, then the mathematician (and
consequently his mathematical intuition) can be specified by (formalized as)
a computer program, and therefore is vulnerable to Godel's result, i.e.,
there are propositions which are undecidable yet true within the 
mathematician's formal system, including truths about mathematics; the
centuries of difficulty with Fermat's Last Theorem leap to mind.

However, the converse does not necessarily hold; merely because some
process of mathematical intuition fails to capture the entirety of
mathematical truth, it does not follow that the set of truths that it
captures can be produced by a formal system. However, the machinations
which you might need to go through to produce such a set make it unlikely
that such a set would correspond in any real way to our conventional
notions of mathematical intuition.

Of course, an AI supporter (for example, me) might claim that, since the
number of mathematical truths produced by a mathematician is finite
(limited by the mathematician's lifetime) that a formal system can 
always be constructed to account for his behavior; this is, indeed, true.
However, that is _not_ a demonstration that all mathematical behavior
_is produced by_ a formalizable system, only that all finite-sized truth
sets can be captured by a formal system (i.e., by including them as
axioms, a procedure which is often referred to as _ad hoc_ or _post hoc_,
depending on your school of thought and the method in which it is done).

Determining whether mathematical intuition is such that it can be
captured by a formal system is an entirely empirical question and cannot
be answered as a matter of principle. This is the source of the pro-AI
requests for a specification of what programs lack that humans possess;
once a "lacking" item has been identified, it must be empirically
verified to exist within humans before the argument becomes damning.

-Anthony Francis
--
Anthony G. Francis, Jr.  - Georgia Tech {Atl.,GA 30332}
Internet Mail Address: 	 - centaur@cc.gatech.edu
UUCP Address:		 - ...!{allegra,amd,hplabs,ut-ngp}!gatech!prism!gt4864b
-------------------------------Quote of the post------------------------------ 
"Cerebus doesn't love you ... Cerebus just wants all your money" 
		- Cerebus the Aardvark, from a _Church and State_ T-shirt
------------------------------------------------------------------------------