[FOM] EFA/PA correspondence as to FLT

[Colin McLarty]

> ---------- Message transféré ----------
> From: "Timothy Y. Chow" <tchow at alum.mit.edu>

Writes to me

> 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

Yes, and I have had some correspondence with him about it since then.
I return to this below.

>  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?

If the paper (rather oddly) cites a proof of the claim that vector
spaces have bases, namely the one in Lang's ALGEBRA explicitly using
Zorn's Lemma, and says not a word about a simpler proof applying in
its case, then yes I will say that paper uses Zorn's lemma in fact.

But my claim in the present case is better than that.  We do not just
say it is "easy" to prove well-ordered vector spaces have bases
without using AC -- there are widely published proofs and most people
on the FOM for example can give such a proof of the top of their head.
  So far as I can find there are no published proofs of (suitably
restricted) Grothendieck duality not using universes, nor even much
published discussion of how to suitably restrict it for given cases.

> 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.

I think Conrad and I rather agree on this point:  Grothendieck and
Dieudonné deliberately use universes to avoid the whole issue of
describing adequate weak fragments of their theorems suited to any
given application.  Conrad very much prefers not to that, but others
notably including Grothendieck and Dieudonné do it in fact.

I call it a central use in Wiles proof because Wiles says how he
actually found two crucial invariants were equal:

"The turning point in this and indeed in the whole proof came when ..
I learned that it followed from Tate's account of Grothendieck duality
theory for complete intersections that these two invariants were
equal''~(p.~451).

The reference in the body of his proof goes back to Grothendieck and Dieudonné.

Conrad has called this "blackboxing."  You use very general geometric
arguments to avoid going into the specific algebra.  He dislikes it.
And to support his preference we can say the new Kisin proof is a
triumph of *not* blackboxing.

Kisin at once sharply generalizes and greatly simplifies Wiles proof
of the Modularity Thesis (the last step in proving FLT).  The key to
his improvement is deep insight into the algebra and arithmetic, not
any concern about logical foundations.  But logicians will note
Kisin's algebraic insight does cut out all appeals to larger apparatus
in Wiles proof.

The key point is that I entirely agree with the many mathematicians
who say that universes are only used as a convenience.  Precisely so.
They are used.  As a convenience.

Logicians might want to explore why they are convenient, and find ways
to give that same convenience without the vastly disproportionate
proof-theoretic strength of universes.

best, Colin