FOM: RE: Insall's set theory

[Matt Insall]

Professor Shavrukov said:
I presume that here  dom f = V, the class of all sets.

In this case, you have that  {V}  is a set by your Replacement (new version
of),
as seen from


Matt:
Good point.  The substitution axioms should be relativized so that when the
domain of the function is a collection of sets (i.e. a class) AND THE RANGE
IS A CLASS, the range must be a set.


Prof. Shavrukov:
Generally, I get the feeling that your system evolves towards non-standard
set theory.  If this is so, then it might make sense to look at pre-existing
formal system for such.


Matt:
You may be right, and I shall look at some such pre-existing formal systems
if I find a need to do so, but my ideas are inspired by a few lines from a
1972 book of Fraenkel, Bar-Hilel, and Levy.  (They may also be inspired
subconciously by the fact that I was briefly exposed to some internal set
theory in the late eighties and early nineties.)   In the Bar-Hilel, Levy
and Fraenkel book is the comment that various levels of ``hyperclasses'' can
be obtained formally, but the consistency of such systems depend upon
various inaccessible cardinal axioms.  These large cardinal axioms are
fairly heavily studied, and I was years ago encouraged NOT to try to publish
results that seem folkloric, so I have not spent much time writing up the
details.  I just thought one of these formal systems would help you.




Prof. Shavrukov:
You might like to look at some papers of V.G.Kanovei, who is a specialist
on, among other things, non-standard set theory.


Matt:
And I interrupted your conversation with him.  I apologize.  I shall try to
get some of those papers.  Thank you.


Prof. Shavrukov:
Abstracting from the peculiarities of any individual formal system, your

>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]}]}

denies 'global' choice for classes, whereas my version only asked for
'local' choice from class many classes.  I am not convinced these
are quite the same.



Matt:
You are right.  They are not the same.  Something closer to your question
might be

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


Prof. Shavrokov:
Incidently, my 'axiom' was rather ad hoc and not well-thought out one.
That was something (more than) I needed to model epsilon-terms
without foundation.

For all I know, the answer to my question may be very simple and
already known.  I would certainly be surprised if it required consideration
of formal systems of non-standard flavour.
Also, I do not have any a priori reasons to believe that such systems
may be helpful in addressing the question.


Matt:
I guess you are right.  I apologize for the intrusion.  But I will consider
your suggestion about Professor Kanovei's papers.



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