[FOM] Fwd: invitation to comment

[Timothy Y. Chow]

Andre Rodin wrote:

> [Kevin Watkins wrote:]
> > (I have no intuition for whether or not this is even possible in the
> > case of the Poincare conjecture... but for the sake of argument, one
> > might admit the possibility that *some* acceptedly "mathematical"
> > result *might* eventually be shown to imply Con(PA) over a weak base
> > theory.)
> 
> In order to establish such a result you need first of all to *formalize* 
> the Poicare-Perelman theorem PP (I can see no reason to call it 
> conjecture any longer), that is, replace PP by its formal counterpart 
> FPP.

No, this is not correct, even given your philosophical position.

It would be perfectly possible to produce a *mathematical* argument that 
deduces the consistency of first-order Peano arithmetic from some other 
mathematical statement such as the Poincare conjecture, using no 
philosophical premises about formal systems and their alleged 
relationship to actual mathematical practice.  In fact, this has already 
been done, not for the Poincare conjecture specifically but with other 
mathematical results in its stead.  (Joe Shipman pointed this out 
recently.)

Now, most people would then be comfortable mimicking such an argument to 
produce a *formal* proof of Con(PA) from FPP, and furthermore asserting 
that the resulting formal proof has "something to do" with the original 
mathematical argument establishing the consistency of first-order Peano 
arithmetic from the Poincare conjecture.  Given your philosophical 
postiion, it seems you would raise some objections here.  But that is 
irrelevant to Kevin Watkins's proposal.

Tim