[FOM] Proving FLT in PA

[Harvey Friedman]

On 2/23/06 6:30 PM, "Colin McLarty" <colin.mclarty at case.edu> wrote:

> But the practical situation is as bad as Timothy says and worse.  Or,
> we could say it is "better" depending on how you like open problems.
> Etale cohomology relies heavily on SGA 1, and the published version of
> that already says it should all be re-written
> in terms of SGA 4.  It has not been yet.  The re-write would not be a
> routine job for some MA thesis but as Timothy notes it is likely not to
> get anyone much credit either.  SGA 3 should also be re-written using
> SGA 4, not to mention the volumes that actually prove the duality and
> related theorems, SGA 5--7.

So I gather from this that as it stands, the current proof of FLT is not
conducted even within ZFC, but instead within some fairly modest extension
of ZFC. Furthermore, that, in your opinion, this state of affairs is
unlikely to change in the near future because of a lack of incentive for the
relevant people to do the necessary work.

My question is this. What are the prospects for at least proving FLT in ZFC?

This could be done by proving FLT in NBG + AxC, even with global choice.
I.e., the class of all sets is well ordered.

Maybe it is relatively easy for some appropriate scholar to attest that one
can get away with defining sets and classes by separation and comprehension
WITHOUT quantifying over classes? This seems quite reasonable to me - that
they don't use quantification over classes to define sets and classes.
CAUTION: Inductions also must not use quantification over classes in the
induction hypothesis. Then we could convert this to a proof of FLT within,
at least, ZFC. I still stand by my conjecture that it can be proved in EFA
(exponential function arithmetic).

Failing this, what about the prospects for some appropriate scholar to
attest that one can do the proofs in MK + AxC? I.e., Morse-Kelly? Here we do
allow definitions of sets and classes using quantification over classes.
Induction could use quantification over classes for the induction
hypothesis. 

If they really use Grothendieck universes inside Grothendieck universes,
then the above plan cannot be carried out - without the kind of major
overhaul that appears to be unlikely in the near future because of a lack of
incentive. That would be even stronger than ZFC + "there exists a strongly
inaccessible cardinal".

It is somewhat surprising that algebraic geometers seem content to LEAVE
things in this state.

Here are two possible explanations. I have not even the slightest idea which
is closer to the truth, or even if there is an explanation that fits the
principal players (they may have very different reasons).

1. These mathematicians are truly entirely comfortable with the present
situation, in that they are true believers in quite strong forms of
Platonism. In particular, they see nothing at all problematic about
Grothendieck universes, strongly inaccessible cardinals, and the like. They
are no less problematic, for them, than the ring of integers.

2. They are trying to thumb their nose deliberately at the very idea that
mathematics need be formalized in any sense - or would even benefit from
being formalized in any sense. They believe that mathematics is a living
activity that defies any restrictions. Valid mathematics is in the doing,
and one cannot reasonably proscribe any limitations. Issues of inconsistency
do not arise because such issues can only be formulated in terms of
formalizations or formal systems, and such objects are wrongheaded and
entirely irrelevant and go entirely counter to the proper and effective
development of mathematics. F.o.m. is as silly as trying to make formal
systems putting restrictions on musical composition or painting. Things like
the FOM email list are a plague, populated by silly self indulgent navel
contemplating fools who cannot do real mathematics.

Harvey Friedman