[FOM] EFA/PA correspondence as to FLT
colin.mclarty at case.edu
Thu Sep 30 14:59:36 EDT 2010
Richard Borcherds's remarks on my paper just now published in the
September BSL but on my website before that
>> This is quite interesting, but also somewhat misleading in places.
>> The author seems to imply at various points that etale cohomology or
>> coherent cohomology or even group cohomology require large set-theoretic
>> constructions. It is obvious to anyone who understands these theories that
>> they do not require large amounts of set theory: this is just a minor
>> convenience in describing them.
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
Everyone agrees it is a convenience. I give quotations to show it is
a widely used convenience, and to explain some of the reasons why.
My article also says much of the large apparatus of Wiles's proof will
one day be by-passed in favor of more direct use of PA. While the
article was being refereed Mark Kisin published a large step in this
direction -- qnd this logical issue is not at all the point of Kisin's
accomplishment. He made a real mathematical advance with a much
simpler and at the same time much more general proof of the Modularity
Thesis. Logicians will note his proof avoids duality and so refers to
no prior results using universes (M. Kisin, Moduli of finite flat
group schemes and modularity, Ann. of Math. Sept. 2009).
To be quite explicit: universes are not "where the action is" in
Wiles's proof, but they are in fact used for the published proofs of
results he needs in his proof. They are not used even in that way in
Kisin's proof. They remain in many other proofs, where every
practitioner knows they could be eliminated but apparently no one
thinks it is worth doing in print.
More information about the FOM