FOM: epsilon terms and choice
Matt Insall
montez at rollanet.org
Mon Sep 18 17:08:33 EDT 2000
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
More information about the FOM
mailing list