FOM: epsilon terms and choice

[Kanovei]

> Date: Sun, 24 Sep 2000 23:59:52 +0100
> From: "V. Yu. Shavrukov" <vys1 at mcs.le.ac.uk>
 
> Still, to model epsilon terms with  G,  I seem to need
> Foundation:  G  chooses from all sets, whereas  epsilon
> terms choose from possibly class-sized collections, so
> under Foundation you just restrict to elements of minimal
> rank and get sets.  Is there a way to do it differently? 

I don't know. The question can be interesting even for 
well-defined theories without Regularity like IST.

> I seem to remember somebody commenting that
> epsilon terms are easily explained away in terms of
> less exotic things in a fairly general setup.
> The explaining away that depends on Foundation does
> not appear too general to me.

Here there is hardly anything to "explain": 
indeed, both \epsilon-terms and 
global choice do not exist in the ordinary mathematical 
universe, hence, the mathematical side of the problem is 
to verify if the apparently stronger assumption in fact follows 
formally from the ther one. This can be just true or false, 
without any foundational application. 

> Mathias, in his recent paper
> (Bulletin London M.S., this year, number 5) tacitly
> equates "Bourbachisme" with  ZC.
> 
> I am not however sure that this should be interpreted
> as him saying that  Z+epsilon  is conservative over
> ZC,  but this would be my natural reaction.
> Any comment?

To verify that ZFGC is conservative over ZFC they extend the 
universe V of all sets by a generic global choice function 
such that no new sets are added. A straightforward implementation 
of this argument w.r.t. ZC does not work: to prove that no new 
sets are added one has to apply Replacement, not only Separation, 
in the ground universe. This is what I had in mind. 
Perhaps, a modification, which Mathias is aware of, solves 
the difficulty, or the conservativity of ZGC over ZC can be obtained 
by a totally different argument. 

V.Kanovei