[FOM] Proving FLT in PA

[Ben Crowell]

Soe Shipman wrote:

>The essential difference is that in the case of a proof using
>infinitesimals, WE HAVE A METATHEOREM so the mathematician doesn't need
>to do any additional work. BEFORE the work of Abraham Robinson, there
>was no metatheorem, and journal editors would have insisted on the
>proof being reworked using limits.

I see your point, but I think there's a weakness in your extension
to my analogy. In, say, 1930, most mathematicians were convinced that
Leibniz-style infinitesimals inevitably led to contradictions, and
they didn't realize that the contradictions could be eliminated by
approaching infinitesimals in the right logical framework. However,
nobody has shown that a contradiction can be reached by assuming
the kinds of things Grothendieck assumed.

It would, on the other hand, be spectacular if FLT
turned to be logically independent of ZFC. There have already
been enough twists and turns in the FLT soap opera that it would
probably be hard even for the experts to rule out such a possibility.
If that happened, then for the first time in a hundred years,
the majority of mathematicians would probably agree that it was
time to make changes in the foundations of mathematics.