[FOM] Proving FLT in PA

[Timothy Y. Chow]

Joe Shipman wrote:
> I consider it an insult to the mathematical community that Wiles et al 
> don't even pay lip service to normal standards of rigor by at least 
> REMARKING that there is a logical issue here and that IN THE PARTICULAR 
> THEOREM BEING PROVED the extra assumptions can be eliminated.

An insult?  Of course you have the right to feel insulted if you want, but 
clearly the mathematical community as a whole doesn't feel insulted, so 
it's a bit odd that you would feel insulted on its behalf.

I believe Crowell's suggestion is on the mark.  Friedman equates Crowell's 
suggestion with explicit, premeditated contempt for foundational matters.  
That is probably true in a large minority of cases, but I suspect in the 
majority of cases, the right word is "apathy" (or possibly even 
"ignorance") and not "contempt."

Shipman refers to "normal standards of rigor."  Well, normal standards of 
rigor allow you to quote published results that are accepted by the 
mathematical community.  Wiles et al. have adhered to normal standards of 
rigor in this sense.  If "normal standards" is supposed to mean that the 
argument has to be shown to be formalizable in ZFC, then I would argue 
that this is "normal" only to those who have some knowledge of 
foundational matters.  Working mathematicians don't usually think about 
what system their proofs can be formalized in.  They "know a proof when 
they see it."  Formalizing it in this system or another is regarded as a 
specialized interest that doesn't have any relevance to whether the 
original proof is rigorous.  ZFC for them is less of a "gold standard" 
than a magic spell that they intone superstitiously to ward off evil 
spirits who might raise foundational issues.  This is a naive and ignorant 
viewpoint, of course, but it's a common one, and so it's a situation of 
"no offense/none taken" for the mathematical community at large.

Tim