[FOM] Grothendieck fdns, query on weak set theories

[Harvey Friedman]

Dear Bob:

You are right. That's more or less what I meant by "reasonable" in http://www.cs.nyu.edu/pipermail/fom/2010-December/015160.html

Harvey

On Dec 7, 2010, at 5:43 PM, Robert Solovay wrote:

> 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