[FOM] Foundational Challenge

[Timothy Y. Chow]

Lawrence Paulson wrote:

> It might help if more mathematicians were familiar with some basic 
> principles of computer science. To a computer scientist, it's natural 
> that a say a graphics application might be built on top of certain data 
> structures or libraries for computer graphics, which in turn are built 
> on lower-level numerical libraries, and so on down until raw binary is 
> reached. For mathematics, ZFC typically serves as the equivalent of 
> binary, while category theory, et cetera, are the libraries.

I like this analogy!

> I think there is a big cultural difference here. I've read an account of 
> G?del's theorem that devoted much space to the concept of 
> G?del-numbering, when coding one thing in terms of another is as natural 
> as breathing to a computer scientist.

I partially agree with you.  I do remember being puzzled about this point 
when first learning the subject, and wondering why the account of Goedel 
numbering seemed so belabored.  I do think that for pedagogical purposes, 
the traditional account of Goedel's theorem should be modified if the 
audience has experience with computer programming.

On the other hand, I have come to realize that there are legitimate 
reasons for spending considerable time on Goedel numbering.

1. Historically, it can be instructive to see how Goedel, in effect, did 
some computer programming before there were computers.

2. For some applications, one wants to know that syntactice operations are 
not only computable, but primitive recursive, and to check this, one needs 
to pay attention to implementation details.

3. The third point is perhaps the most important, although it's not always 
explained clearly in textbooks.  Goedel numbering is a key step in the 
argument that *syntactic* operations are faithfully mimicked by 
*arithmetical* operations.  As is apparent from the discussions on FOM 
about Artemov's and Detlefsen's arguments about the provability (or 
unprovability) of consistency, this point continues to cause confusion to 
this day.  One not only wants Goedel's theorems to be proved; one also 
wants to draw metamathematical conclusions about the implications of 
Goedel's theorems for the unprovability of consistency, and for that, one 
needs to inspect the conversion from syntax to arithmetic and confirm that 
the encoding was "faithful" in an appropriate sense.

Tim