FOM: epsilon terms and choice

[Matt Insall]

Professor Shavrukov,
You posed the following question to Professor Kanovei:

<<
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?
>>



I am wondering if the following works or helps:

1.  Let GNB denote the (usual) first-order theory of classes without the
axiom of foundation.

2.  Let L be the first-order language obtained from the language for GNB by
adding a unary predicate, ``class''.

3.  Let T be the theory of L with the following axioms:

EXT:
(forall x){[(x is in X)iff(x is in Y)] implies X=Y}

SEP(phi):
(forall X_1,...,X_n)(thereis Y)(forall x)[x is in Y iff phi(X_1,...,X_n,x)]

SET/CLASS
(forall x)(forall y)[(x is in y) iff (x is a class)]
(forall x)(forall y){[(x is in y)&(y is a class)] iff (x is a set)}

PAIR:
(forall x,y)(thereis z)(forall w)[{[w is in z] iff [(w=x) or (w=y)]}&{[z is
a set] iff [(x is a set)&(y is a set)]}]

UNION:
(forall x)(thereis y)(forall z)[{[z is in y] iff (thereis w)[(z is in w)&(w
is in x)]}&{(y is a set) iff (x is a set)}]

POWER:
(forall x)(thereis y)(forall z)[{[z is in y] iff (forall w)[(w is in z)
implies (w is in x)]}&{(y is a set) iff (x is a set)}]


INF:
(thereis x)(thereis y)(thereis z)(thereis w){[(forall t)(t is not in x)]&[x
is in y]&[y is in z]&[z is in w]&(forall p)[(p is in y) implies (thereis
q){(q is in y)&(forall r)[(r is in q) iff (r is in p) or (r=p)]}

SUBST:
(forall f)(forall x){[f is a function] implies [{(x is a class) implies
(f[x] is a class)}&{(x is a set) implies (f[x] is a set)}]}

GC:
(thereis f){[f is a function]&(forall x)[(x is a set) implies {(thereis y)[y
is in x] implies [f(x) is in x]}]}

NCC:
(forall f){[f is a function] implies (thereis x)[(x is a class) & {(thereis
y)[y is in x] & [f(x) is not in x]}]}


4.  Is T a conservative, relatively consistent extension of GNB?

5.  Let NEC be the statement that negates (in L) the one you asked about:
(there is x){(x is a class)&(thereis e)[e is an equivalence on x]&(forall
f)[(f is a function from x into x) implies {(forall p)[(p is in x) implies
((p,f(p)) is in e)] implies [(thereis y)(thereis z){(y is in x)&(z is in
x)&(not[f(y)=f(z)])}]}]

6.  Let EC be the statement (in L) that you asked about:  EC=not(NEC).

7.  Is NEC a theorem of T?

8.  Is EC a theorem of T?

9.  Does any subcollection of these questions constitute a reasonable
reduction of your question to a simpler problem?










Dr. Matt Insall
http://www.umr.edu/~insall