[FOM] Grothendieck fdns, query on weak set theories

[Colin McLarty]

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.)

So I want to understand the relative strengths of the set theories involved.

First:   What difference does it make when one set theory T proves
another T' has a model of the form V-sub-alpha, versus merely proving
T' is consistent?  Of course the first kind of proof shows T proves
existence of the ordinal alpha and T' does not.  But how important is
that?  Does the first sort of proof show a greater difference in
consistency strength than the latter?

Second:  Does Zermelo set theory (including choice) prove consistency
of each of its finitely axiomatized subtheories?  I believe this
follow from the much more detailed Theorem 5 section 3 of Mathias's
vast, madly concise, and madly rich paper "The Strength of Mac Lane
Set Theory." But this is what he calls "the dangerous part of logic
where to blur distinctions between languages is to jeopardise meaning"
(p. 8) and I may be blurring some distinction.

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.

best, Colin