[FOM] Weak foundations for cohomological number theory

[Harvey Friedman]

On Jan 3, 2011, at 11:04 AM, Colin McLarty wrote:

> I can now show that the Grothendieck-Deligne proof of the Weil
> conjectures, and Wile's and Kisin's proofs of Fermat's Last Theorem,
> can be formalized in Bounded Zermelo Fraenkel set theory with choice.

I gather that "bounded Zermelo Fraenkel set theory with choice" is not  
what you meant to write, and you mean "bounded Zermelo set theory with  
choice" =  "bounded ZC".

A good next step would be to do this in full ZFC with Power Set  
weakened to

100 power sets of omega exists.

Then reduce 100 considerably, maybe down to 0.

It is well known that any arithmetic (and much more) sentence provable  
in this system - even with 100 replaced by any specific integer in  
base 10 notation - is provable in bounded ZC.

It is also well known that any arithmetic (and much more) sentence  
provable in any of these systems, including ZC, is provable in the  
same system without use of the axiom of choice.

Harvey Friedman