[FOM] EFA/PA correspondence as to FLT

[Colin McLarty]

I am happy with Harvey's summary:

> 1. Wiles' proof of FLT is not given outright within ZFC, in the usual sense.
>
> 2. No new ideas are needed to cast Wiles' proof in ZFC. However, there is still a perceived need for documenting a form of Wiles' proof in ZFC.
>
> 3. Kisin's new proof of FLT is given outright within ZFC, in the usual sense.

Well, a lot of mathematicians perceive no need to document a form in
ZFC.  Some have no interest in logic, and others have a well grounded
but imprecisely formulated belief that "this kind of thing" can always
be done in ZFC.  And on the other hand some set theorists say they are
so happy with large cardinals that a mere strong inaccessible is no
issue to them.  I have no quarrel with those viewpoints

But logicians ought to give precise formulations, and turn well
grounded beliefs into proofs, and should be at least piqued by such
profligate assumptions.

I can answer this question:

> 4. Are new ideas needed to cast Wiles' proof in ZC?

No.  I have not tried to check every detail, but the only part of the
Grothendieck apparatus that seems to use serious transfinite
induction is proving certain categories have "enough injectives" (I do
not know how much induction is necessary there either, but
the usually cited proof in Grothendieck's 1957 Tohoku paper uses
arbitrarily long inductions).  In effect that apparatus depends on
showing every sheaf of modules embeds into an injective sheaf of modules.

Because Wiles does not need cohomology groups above dimension 3, and
then only for certain specific sheaves of modules, the standard
inductions can be bounded at bounds that ZC proves exist.

I have not even thought about any role of Choice.  I have no opinion
on that, let alone information.


>  In Z_8?

It seems to me that most of the proof is pretty overtly in Z_8 or so.

>  In Z_3? In Z_2?

I have no well-informed view on this.  Angus Mcintyre seems to have
looked most closely at this so far.

> In Pi11-CA_0? In ATR_0? In PA? In EFA?

I expect this would need new ideas.  I do not claim I can demonstrate
that (let alone provide the new ideas).

> 5. Are new ideas needed to cast Kisin's new proof in ZC? In Z_8? In Z_3? In Z_2? In Pi11-CA_0? In ATR_0? In PA? In EFA?

I have not looked at this the way I have Wiles's.  My feeling is it is
overtly in ZC or even Z_8, but the weaker arithmetics would need new
ideas.

> I would also like to raise the same questions with regard to Falting's and other proofs of the Mordell Conjecture.
>
> Harvey Friedman

Yes.  I second that.  Falting's proof has been greatly simplified
since he gave it.

And I would also like to know how weak a foundation will work for the
general Grothendieck apparatus (say SGA 4) as applied just to
arithmetic.  This is somewhat vague, depending on what is meant by
"just arithmetic."  But I believe there are real insights to gain from
eliminating the visibly excessive strength of universes while
preserving the natural conceptual order that Grothendieck set up.

Colin