FOM: shankar book, questions on g"odel's result + recursion

[vznuri@earthlink.net]

Ive been revisiting g"odel's thm recently
& coming back to a question Ive always had
on it.

I would like to recommend the book to everyone,
"metamathematics, machines and g"odel's proof"
by n.shankar, cambridge tracts in theoretical
computer science.

the author actually *constructs* the entire
g"odel sentence asserting its unprovability.
he pulled this feat off in lisp after 18
months of PhD work & many tens of thousands
of lines of code (I think he mentioned how 
many, but I couldnt find it again in the book
just now). he used the boyer-moore
thm prover. I think many here will find it
quite engaging. it also advances the idea
that mathematics is at the heart a kind of
computer programming.

* * * 

iiuc, g"odel's result applies to
a theory that allows recursive statements,
such as the recursive form of the fibonacci
sequences

f_n = f_(n-1) + f_(n-2)  f(0) = f(1) = 1

unfortunately in any such theory, you can
define functions, say g, such that they
involve an infinite recursion & are not defined.
for example if above I didnt define the base
cases for f_n, the function is undefined.
this is interesting in that correct definition
of the base cases (not the recursive part itself) 
moves it from undefined to defined.

the question: how do I know for sure g"odel's
proof has defined all his base cases? in particular,
for the sentence that asserts of itself that
it is not provable?

next question. has anyone done any work to
simplify the g"odel statement, i.e. crunch
at it with a theorem prover that might reduce
it to a simpler form... ? seems like an
interesting exercise & inquiry.  especially
now that shankar has actually constructed
it. (he writes in his book it is distributed
with the boyer-moore thm prover).

I wonder, could the g"odel sentence be
asserting something like, "this is an infinite
string of true statements"..?? such a statement
could be true, but not provable within
the system, fitting the bill. moreover, if the
statements actually utilize all the axioms
of the system, it would also require consistency
of the axioms to be true.

seen in this light, maybe g"odel's proof is
a case of turing's halting problem in a different
guise, instead of vice versa as is more commonly
the view.

another question. suppose we consider the theory
that allows recursive functions, but also
requires a proof that they are "defined" 
in the above sense (base cases given) before
one is allowed to manipulate them. 

would such a system be the same or different than what
g"odel considered? what would be its implications
for provability? could it be possible a g"odel-like 
unprovability result might not be derivable in such
a system? even more radical, given that,
could a systematic thm prover be devised in it?