[FOM] predicative foundations

[Robert M. Solovay]

On Tue, 14 Feb 2006, Harvey Friedman wrote:

>
> Within the last few months, I had some conversations with a Fields Medalist
> (core mathematician) - a different one than I have ever previously alluded
> to.
>
> I asked him if he ever used the axiom of choice in his main research.
>
> He surprised me, and said yes, a lot of the time, and in fact, the example
> he gave me surprised me on several counts.
>
> 1. He and his colleagues use it all the time, and things like it. It
> involves only countable structures, and is very natural - for them and for
> me.
> 2. He and his colleagues did not know (according to him) how to remove the
> axiom of choice.
> 3. In fact, they identify Zorn's Lemma as the method of proof.
> 4. The proof they have of it not only uses the axiom of choice, but is
> blatantly highly impredicative in other ways. Even beyond iterated inductive
> definitions.
>
> In fact, it is clear that they are indiscriminately working in a system like
> full second order arithmetic with lots of choice  - at least!
>
 	I find this quite intriguing. Can you say waht area of matheamtics 
this is. Has the Fields Medalist requested anonymity or can you talk 
explicitly about who he is, and what the theorems in question are.

 	--Bob Solovay