[FOM] predicative foundations

[Harvey Friedman]

On 2/14/06 9:25 PM, "Robert M. Solovay" <solovay at math.berkeley.edu> wrote:

> Surely the current proof of Wiles-Taylor is not routinely
> formalizable in PA [with its appeal, for example to the Langlands-Tunnel
> theorem].
> 
> I am aware that you have *conjectured* that FLT should be provable
> in EFA.
> 

I was wondering if you could give some sort of indication of some of the
difficulties involved, and work needed, to show that FLT is provable in PA
or even in EFA? 

For example, you might tell us something about

1. Some of the results used that themselves may not be provable in PA, or
even properly statable in PA.

2. A guess at the most basic thing involved in FLT that needs to be analyzed
with some care to see that it can be properly interpreted in and/or proved
in PA or EFA.

3. Your opinion about the truth of my conjecture.

Harvey Friedman