[FOM] Logical Status of FLT

[Harvey Friedman]

 From the recent FOM postings on the logical status of FLT, and from  
McLarty's http://www.cwru.edu/artsci/phil/Proving_FLT.pdf, I think we  
can draw a few conclusions.

1. Wiles' proof of FLT is not given outright within ZFC, in the usual  
sense.

2. No new ideas are needed to cast Wiles' proof in ZFC. However, there  
is still a perceived need for documenting a form of Wiles' proof in ZFC.

3. Kisin's new proof of FLT is given outright within ZFC, in the usual  
sense.

My questions are:

4. Are new ideas needed to cast Wiles' proof in ZC? In Z_8? In Z_3? In  
Z_2? In Pi11-CA_0? In ATR_0? In PA? In EFA?

5. Are new ideas needed to cast Kisin's new proof in ZC? In Z_8? In  
Z_3? In Z_2? In Pi11-CA_0? In ATR_0? In PA? In EFA?

I would also like to raise the same questions with regard to Falting's  
and other proofs of the Mordell Conjecture.

Harvey Friedman