[FOM] Proving FLT in ZF (was in PA)

[Harvey Friedman]

On 2/27/06 1:51 PM, "Colin McLarty" <colin.mclarty at case.edu> wrote:

> Harvey Friedman wrote, quite rightly, on the use of universes in
> proving FLT:
> 
> Only I would add that they feel the work is routine.  I do not think
> it is any intransigeant disregard for formalization.

In other words, the relevant experts feel that formalizing the proof of FLT
within ZF (or ZFC?) is routine?
> 
> I am pretty sure this is the best prospect for a principled proof in
> ZF that stays close to Grothendick's strategy:

Can we avoid choice and keep it close to Grothendieck?

>The arguments of the
> SGA (which are cited by Wiles) do use universes in universes.  But
> with one exception they do not use replacement in any universe.
> 
> So for all but this one theorem you could weaken the definition
> of "universe" to any transitive set that models Z.  ZF already gives
> proper-class many of these.  (They are just V at each limit cardinal,
> aren't they?) 

The V(lambda), lambda a limit ordinal greater than omega, are models of ZC.
Not every transitive model of ZC is of that form, thoough. But that should
not be a problem.  
> 
> So I believe the whole thing can be done in nearly Grothendieck's way,
> for any one set of Grothendieck topologies, using "weak universes" in
> the sense of sets that model Z and have sufficient, but cardinally
> bounded, replacement.

For example, would it be sufficient to have the following, and maybe this is
overkill?

Limit ordinals greater than omega, or even limit cardinals, lambda_1 <
lambda_2 < ... < kappa, where (second order) replacement holds in V(kappa)
with respect to lengths that are less than some lambda_n? This would
certainly be well within ZFC.

At least then we will be on our way to a proof of FLT within ZFC?

I still like my conjecture that FLT can be proved in EFA = exponential
function arithmetic, weak fragment of PA. Would that require at least a very
radical reworking that might require serious new ideas?

Harvey Friedman