[FOM] Grothendieck fdns, query on weak set theories

[Robert Solovay]

Harvey,

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.

--Bob Solovay

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
> http://www.cs.nyu.edu/mailman/listinfo/fom
>