[FOM] EFA/PA correspondence as to FLT (fwd)
Timothy Y. Chow
tchow at alum.mit.edu
Mon Oct 4 11:21:03 EDT 2010
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
More information about the FOM
mailing list