[FOM] Proving FLT in PA

[Harvey Friedman]

On 2/21/06 7:00 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> Harvey Friedman wrote:
>> I was wondering if you could give some sort of indication of some of the
>> difficulties involved, and work needed, to show that FLT is provable in
>> PA or even in EFA?
> 
> Here's one issue I've seen raised.  The fundamental facts of etale
> cohomology are developed in SGA, specifically SGA4, and Grothendieck
> universes are (apparently---I've never studied SGA4) freely assumed
> whenever necessary.
> 
> The experts seem to feel that for a "concrete application" like FLT, it
> would be routine to eliminate any use of Grothendieck universes.  In
> particular, there's probably no interesting math involved in the
> elimination process.  However, unless someone actually goes to the trouble
> of doing the necessary bookkeeping, there remains a question mark.
> Unfortunately, because of the highly technical nature of the subject,
> doing the bookkeeping would seem to require an inordinate amount of
> effort.
> 

I knew about this issue, but I was assuming (perhaps wrongly) that this part
of the project would be reasonably straightforward, and there were other
parts that might be more problematic.

Incidentally, I have a question for Weaver: is FLT core mathematics? What do
we learn from this persistent use of Grothendieck universes by core
mathematicians?

If impredicativity turns out to be essential in proving FLT, then how does
this affect your (Weaver's) insistence that predicativity is a far better
fit for core mathematics than set theory? Quite the opposite would seem to
be the case. 

It is perhaps surprising that there has not been papers systematically
eliminating Grothendieck universes from core mathematics, especially FLT.
After all, Grothendieck universes are on the cusp of ZFC.

Even if Grothendieck universes are well known or well believed in the core
mathematical community to be eliminable here, they likely might prefer to
keep a fragment of them known as topoi. Topoi are around the level of
Zermelo set theory, still wildly impredicative.

Another question for Weaver: why are these core mathematicians so wedded to
working with this wild impredicative monsters?

If they are eliminable, why don't they take the perhaps small trouble of
eliminating them? After all, then, according to you, they could easily
attain a "clear philosophical basis" for their work. If they are not
eliminable, then are you prepared to change your views?

Harvey Friedman