Conversations over the summer led to sharp improvements on my February
ArXiv article on weak foundations for Grothendieck's number theory.

I now formalize the entire Grothendieck tool kit at the strength of
finite order arithmetic.  In other words at the strength of ETCS (with
NNO) or simple type theory with infinity.  This includes even the
largest scale structures: derived categories for duality, and the
2-category of geometric morphisms between toposes.

This does not get as low as n-th order arithmetic for some fixed
finite n, but is reasonably weak and yet quite general.  This
foundation is natural for the Grothendieck toolkit as a whole, while
of course no single application uses the whole.

Besides that the argument is now simpler, the key advances since my
talks in July are:

1) a proof using only bounded separation that every sheaf of modules
over any Grothedieck site has an infinite-length injective resolution.
  Of course the resolution can be 0 from some point on in some cases,
but in general it cannot.

2) a conservative extension of Mac~Lane set theory with proper classes
and collections of them, modelled on Takeuti's conservative higher
order extension of PA.

My ArXiv article has been revised.  The new version re-titled "A
finite order arithmetic foundation for cohomology," is on my web page
at

http://www.cwru.edu/artsci/phil/Derived_functor.pdf

and is on the math arXiv as

http://arxiv.org/abs/1102.1773

It is substantially shorter than the February version, while proving a
stronger result.   I take this as a case where it is easier to prove
the right theorem than the wrong one.

best, Colin


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]