FOM: epsilon terms and choice

[V. Yu. Shavrukov]

Dear Professor Kanovei,


thank you very much for the information you provided.


>ZFC + the epsilon-term seems to be the same as ZFC + Global Choice,
>or ZFGC.
>It is known (they refer to Felgner, 1971) that ZFGC is
>a conservative extension of ZFC, that is, any theorem of
>ZFGC in pure membership-language is a theorem of ZFC.

I am not quite sure what you mean by `ZFC + Global Choice'
in the first sentence.  Is it  GB + GC, or
ZFC + schema: definable classes exist + GC
(+ extensionality for classes),  or something else?

I can see that either of these theories is 'the same'
as  ZF(C) with epsilon terms in the sense that
they have the same 1st order theorems.

Is it the case that one of the above 2nd order theories
is 'the same as ZFepsilon' in a stronger sense than that?


Incidently, the way to model epsilon-terms by classes under GC
that I am aware of does not work without Foundation.

Do you know if the situation continues to be the same in
theories without Foundation?

A related question:

Consider the statement

Let F be a class. Suppose the class E is an equivalence relation
on F.   Then there exists a class function C : F -> F  s.t.
for all x in F,  x E Cx;
for all x,y in F,  x E y  imples  Cx = Cy.

Do you know if this follows from GC without Foundation?


sincerely,
V.Shavrukov