[FOM] Grothendieck fdns, query on weak set theories
friedman at math.ohio-state.edu
Tue Dec 7 19:00:51 EST 2010
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
On Dec 7, 2010, at 5:43 PM, Robert Solovay wrote:
> 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
More information about the FOM