[FOM] Re: Godel: the proof from The Book??

[Timothy Y. Chow]

Peter Smith <ps218 at cam.ac.uk> wrote:
> Leaving Godel's own original effort out of it, what proof of the first 
> incompleteness theorem would you suggest as a candidate for The Book?

Mitch Harris raised a similar question in sci.math last November.
Herman Rubin rather liked Mostowski's account (in "Sentences Undecidable
in Formalized Arithmetic" I think).

The concept of The Book applies very nicely to "self-contained" theorems,
but I think it starts to break down as soon as enough general theory gets
built up so that a broader pattern starts to emerge.  An area of math that
is mature enough to have lots of pretty theorems that are symptomatic of a
deeper underlying structure is probably best presented (and I do mean 
"best" from an aesthetic and not just a pedagogical point of view) in a
way that makes clear the big picture.  And in this big picture, many nice
theorems might fall out as corollaries.  Is The Book going to contain the
"locally optimal" proofs of the individual theorems or the "globally 
optimal" treatment of the entire subject area?

I think the first incompleteness theorem teeters on the brink of this sort 
of situation.  My feeling is that The Book contains a development of a
slightly broader area than just the incompleteness theorem itself.  For 
example, I'd guess that as far as representing recursive functions in the 
first-order language of arithmetic goes, a locally optimal proof would 
contain just the bare minimum needed to push Goedel's 1st theorem through.
But I personally wouldn't find such a minimalistic approach very pleasing.

Since this is FOM, allow me to speculate that if these kinds of aesthetic
considerations can be formalized even partially, so that (for example)
computers can be programmed to find Book proofs, then that would likely
attract the attention of mainstream mathematicians and maybe get them
more interested in f.o.m.

Tim