[FOM] Grothendieck fdns, query on weak set theories
solovay at gmail.com
Tue Dec 7 17:43:50 EST 2010
I think you inadvertently dropped the requirement that the theory T
that contains full induction is also **sequential** (handles finite
sequences well). At least, I need that additional hypothesis for the
proof I know. (Perhaps you know a different proof?
The proof I know can be sketched as follows. Let T be the strong
theory (say Zermelo) and let S be the finitely axiomitizable theory we
want to prove consistent. Transform the proof of 0=1 from S, using
Herbrand's theorem (replacing quantifiers by epsilon terms) to get a
finite conjunction of Herbrand instances of S that is contradictory.
Now exploit partial truth definitions and our full induction to
step-by-step construct an interpretation of the epsilon terms that
shows the conjunction is in fact satisfiable. Contradiction.
The place where I need that the theory is sequential is to handle the
partial assignments of elements of our universe to epsilon terms.
On Sun, Dec 5, 2010 at 9:45 PM, Harvey Friedman
<friedman at math.ohio-state.edu> wrote:
> 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
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM