FOM: epsilon terms and choice

[Matt Insall]

Thank you, Professor Shavrukov, for your time.  I will respond on each point
in your reply.


Professor Shavrukov:
>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)}

both these axioms look very strange to me.
I wonder if they express what you meant to express.
It might have been better if you spelt them out in words.


Matt:
This is intended to be a first order theory of ``collections'' with no
urelements.  The first SET/CLASS axiom is intended to say
``Every member of a collection is a class.''

The second SET/CLASS axiom says
``Every member of a class is a set.''




Professor Shavrukov:
It would also help if you explained what the relation of
'classes' to the rest of the entities in T's universe is.
Is everything a class?

Matt:
That is not what I intended.  A ``class'' can be a member of a
``collection''.


Professor Shavrukov:
Is the universe partitioned into
classes and sets?

Matt:
An example of a collection which is neither a class nor a set is {A}, where
A is the class of abelian groups.



Professor Shavrukov:
Should one read 'class' as proper class?


Matt:
Not if I typed what I intended to type.  What I intend is for every ``set''
to be a ``class'', and every ``class'' to be a ``collection''.  I guess I
would call a ``collection'' that is not a ``class'' a ``proper collection''.
I would call a ``class'' that is not a ``set'' a ``proper class''.


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

any restrictions on phi?

Matt:
I think the formula phi should be a formula of the first order language L
obtained from the language of GNB, and I intend using it much the same way
that it is used in the text of Smullyan and Fitting entitled ``Set Theory
and the Continuum Problem''.    However, in my case, capital variables are
intended to represent ``collections'', whilst lower case variables are
intended to represent either ``classes'' or ``sets''.  With respect to
distinguishing ``classes'' from among ``collections'' and ``sets'' from
among ``classes'', I use a similar convention to Gödel's paper on the
Continuum Hypothesis, in which he uses a predicate to distinguish ``sets''
from among the ``classes'', where all his objects are ``classes''.  Thus,
phi is a formula whose ``collection variables'' are among X_1,...,X_n, and
these are free in phi, and the only ``class/set'' variable of phi is x, and
I see no reason to require that x be free, although it seems not to make
much difference.  (With regard to the ``collection variables'',
capitalization is, I think, unnecessary, but only serves to highlight the
fact that I want these variables to occur free in phi.)



Professor Shavrukov:
>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]}]}

This suggests to me that you are willing to allow some classes
to be elements of other classes.  Is this what really you want to do?


Matt:
This is what I want to do.  This may cost me conservativity, but I am not
sure why it would, for I intend my ``collections'' to be in a similar
relationship to ``classes'' as the GNB ``classes'' are in with ``sets''.  It
seems to me that in the theory T, one can prove that no ``proper class'' is
a member of any ``class'', because ``classes'' must have only ``sets'' as
members.  I am not terribly comfortable with the idea of not having the
axiom of foundation available, because I have not had much experience with
non-well-founded set theories.  But I will probably enjoy trying it out.





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