[FOM] Proving FLT in ZF (was in PA)
friedman at math.ohio-state.edu
Wed Mar 1 01:11:28 EST 2006
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
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?
More information about the FOM