[FOM] predicative foundations

[Robert M. Solovay]

On Tue, 14 Feb 2006, Harvey Friedman wrote:

> 2. Give me one example of a theorem aobut finite objects, in what you call
> "normal" or "core" mathematics (I make a distinction between the two), that
> is not handled in PA, or even EFA. Both PA and EFA are far less than
> predicativity - both mathematically and philosophically.

 	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.

 	--Bob Solovay