[FOM] Proving FLT in PA

[Ben Crowell]

Harvey Friedman wrote:

>Here are two possible explanations. [...]

>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.[...]

How about:

3. They're convinced that the proof could be reworked so that it would
only use ZFC, but they see it as a waste of time to carry out the
routine steps that would be necessary. This would be like publishing
a proof using infinitesimals, knowing that it could be rewritten
using limits, and not feeling that anything would be gained by
the rewrite.