[FOM] predicative foundations

[Robert M. Solovay]

On Tue, 21 Feb 2006, Harvey Friedman wrote:

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

 	I mentioned the Langlands-Tunnel theorem. See Chapter VI in 
"Modular Forms and Fermats Last Theorem". I think this meets both your 
requirements.

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

 	As the cited book shows the Wiles-Taylor proof is a truly 
enormous beast. The work naturally seems to be carried out in third order 
number theory, and to compress it into PA seems a heroic if not impossible 
task.


> 3. Your opinion about the truth of my conjecture.

 	I'm extremly sceptical that the current proof can be reformulated 
in PA. Of course, there might be some wholly different elementary proof. 
I don't have strong opinions on that issue.

 	I'm also sceptical that there will be a decisive refutation of 
your conjecture.. {Say a proof that FLT implies the consisteny of EFA or 
PA.}

 	I do think it makes a charming research programme. One thing that 
would be nice is to have proof assistants like Isabelle or Mizar that are 
adapted to some variant of the formal systems PA or EFA.

>