[FOM] Grothendieck foundations progress, and a posted error

[Harvey Friedman]

> On Sep 12, 2011, at 11:26 AM, Colin McLarty wrote:
>
> I have sent the math arXiv an updated version of the paper, adding
> this result about cohomology with just one powerset of the naturals:
>
> ZFC[1], which is ZFC without the power set axiom but positing that the
> naturals have a power set, proves every countable module on a
> countable ring has cohomology groups of all finite orders.  Added as
> Section 3.6.2.  The powerset serves to form function sets between
> countable (not finitely generated) Abelian groups--notably the
> underlying Abelian groups of polynomial rings.
>
> The result fits nicely in this context.  But it will get its full
> value when extended to cohomology of schemes, and I am still working
> to see the best low-order arithmetic approach to arithmetic schemes
> for cohomology.

Are there any interesting issues of "necessary uses of such strong  
systems" in your contexts?

> I am still in the market for a plain published proof of mutual
> interpretability of ZF[0] in second order arithmetic if one exists.
> Even if I work out the details for myself first it would be good to
> have a citation.

There is a reason why this is an elusive result. There is an old  
result I think of Azriel Levy that ZF without power set is NOT a  
conservative extension of second order arithmetic. I.e., ZF\P is NOT a  
conservative extension of Z_2. I.e., there is a sentence provable in ZF 
\P, which, when routinely translated into the language of Z_2, is not  
provable in Z_2.

However, the counterexample is pretty high up in complexity. We do  
have conservative extension for sentences of reasonable complexity.  
However, this uses quite a bit of old machinery - particularly,  
Goedel's L technology crafted for fragments of ZF.

And of course we have interpretability. In fact, we have  
interpretability preserving the integers, in the appropriate sense.  
But only using this old machinery.

Also ZFC\P is a conservative extension of Z_2 for sentences of  
reasonable complexity sentences.

Harvey Friedman