[FOM] Grothendieck fdns, query on weak set theories

[Harvey Friedman]

On Dec 5, 2010, at 12:15 PM, Colin McLarty wrote:

> I am working to show Grothendieck cohomology theory can all be done,
> very little changed, in bounded Zermelo set theory with an axiom
> saying there is a corresponding universe -- a transitive set model of
> bounded Zermelo which interprets powersets the same way as the ambient
> world of sets does.  Those axioms further imply the universe models
> Zermelo with unbounded separation because the universe itself acts as
> a bound.  (Here Zermelo includes choice, needed for the proof that
> cohomology functors exist.)

A good way to state the theory that I think you mean might be

bounded Z + V(omega + omega) exists.

This is "much" stronger than theories like

bounded Z + "Z is consistent"

In particular, the former proves the latter is consistent.

> Third, if ZC does prove consistency of each of its finitely
> axiomatized subtheories, what is a good basic reference for that?
> Perhaps a modification of the proof will show that ZC plus an axiom of
> a universe also proves consistency of its finite subtheories.  Unless
> I am mistaken, this does not follow directly from the theorem about ZC
> -- I would love to be wrong about that though.

There is an old result that any reasonable theory that proves  
induction with respect to all formulas in its language, proves the  
consistency of all of its finite fragments.

Harvey Friedman