FOM: On A.Wiles's proof of FLT

[Alexander Zenkin]

In his posting [Fri, 6 Feb 1998], Soren Riis writes:

> Wiles gave an informal proof, in which I assume there was
> no mentioning of any axioms in ZFC. Wiles proved FLT.
> I am not claiming
>Wiles proof is mistaken if it cannot be formalized in ZFC.

I would like to make a remark on his statement: " Wiles proved FLT."

In 1986, Kenneth Ribet proved that the Tanijama-Shimura conjection
(TSC) implies FLT, i.e. he proved that the implication TSC - > FLT is
true,
only. Some years after that, A.Wiles proved, strictly speaking,
not FLT, but he proved TSC (see "Update on Proof of Fermat's Last
theorem" by Allyn Jackson in Noties of AMS, March 1994, vo. 41,
no.3, pp. 185-186).

The FLT follows only from both these results by modus ponens:
TSC, TSC - > FLT |- FLT.
Of course, this does not make the Wile's achievement less outstanding,
but it is obvious, that without Kenneth Ribet's implication HTS - > FLT,

the Wiles result were an outstanding result but in the elliptic curve
theory
only.

I think, the fact, that FLT was obtaind not from Peano's axioms
directly,
but from the elliptic curve theory, makes the problem of the
ZFC-formalization of the FLT-proof still less easy.
For people who will engage in this task.

This small remark is important for understanding the logic nature of my
superinduction method (see my FOM-posting [     Fri, 06 Feb 1998 ])

Alexander Zenkin