[FOM] EFA/PA correspondence as to FLT (fwd)

[Timothy Y. Chow]

Colin McLarty wrote:

>Well I hope it is not misleading.  Far from saying large sets are
>required, I say certainly much less than ZFC is used in principle,
>probably nothing beyond PA, and perhaps much less than that.
>
>And I quote passages from Wiles and other works showing how both the
>proof as published, and its background in textbooks, is given using
>large sets.

As you may already be aware, Brian Conrad insists that your paper is 
wrong:

http://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof

I think that part of what's in question here is, what does it mean to cite 
a reference?  FOMers may have a mental picture of reference citations that 
resembles our mental picture of computerized proof assistants: If you cite 
something, then you automatically load the entirety of the cited work 
verbatim, along with verbatim copies of everything *that* work cites, and 
so on down the line.  If you want to avoid the default auto-loading 
behavior, then you have to write some new code.

However, human mathematics is a lot more fluid than that.  If I cite the 
Hahn-Banach theorem in a paper in functional analysis, am I explicitly 
using the axiom of choice?  That's how it's proved in all the textbooks, 
but it is also well known how to avoid full-fledged AC in the vast 
majority of actual applications of Hahn-Banach.  For an even more mundane 
example, suppose somewhere in a paper there appears the sentence, "So V is 
a vector space; let B be any basis of V."  Does this paper use AC, if V 
happens to be a very concrete vector space for which one could easily 
exhibit a specific basis with AC if one cared to?  I think one would have 
to be very pedantic to insist that AC is being used here.

The same sort of thing is going on with Grothendieck-Dieudonne.  As you 
say in the article, "All the authors including Grothendieck and Dieudonne 
know that fragments of these theorems adequate to any given application in 
arithmetic can be stated inside ZFC by abandoning the system in favor of 
technicalities and circumlocutions suited to that application."  Given 
this, it is at the least highly debatable whether citing their work 
automatically constitutes "using universes in fact," or constitutes a 
"specific, central use of universes in Wiles's proof."  This is what I 
believe Borcherds considers misleading and Conrad considers outright 
wrong.

Tim