FOM: RE: Insall's set theory
Matt Insall
montez at rollanet.org
Sun Sep 24 19:28:59 EDT 2000
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
More information about the FOM
mailing list