[FOM] Grothendieck foundations, fragment in second order arithmetic
colin.mclarty at case.edu
Sun Jul 1 12:07:28 EDT 2012
I have just posted an article to the math ArXiv, "Coherent, Cech, and
Zariski cohomology in second order arithmetic." It formalizes the
basic tools of cohomological number theory, short of etale cohomology,
at the proof theoretic strength of second order arithmetic. There is
no reason to doubt such an approach could work for etale cohomology
but i have not done it yet -- let alone crystalline cohomology etc.
The theorems are not limited to the countable case but of course the
foundation cannot prove any non-countable cases exist.
Specifically the article uses ZFG, Zermelo Fraenkel without
powerset, extended by a global choice principle. There is no serious
need for global choice. It only needs that each set can be
well-ordered (which of course does not follow from the usual axiom of
choice without using power sets). But the constructibility
interpretation in second order arithmetic naturally gives a global
As Harvey has suggested, the advantage to restricting power set in
ZF is to get the strength of second order arithmetic without
The article obviously checks a great many things, and the weaker a
foundation we use the more care we need. It remains as always the key
problem is to prove existence of enough injectives in each context we
The article should appear on the arXiv at 10pm EST Monday.
More information about the FOM