type n class theory?
Toby Bartels
Here is an idea of mine.
I know I'm not the first to think of it.
What I want to know is:
Is there any use to it? and
Under what name do I look it up to find out more about it?
Begin with the axioms of set theory.
These axioms form type 0 class theory.
A set is a class of type 0.
Now modify these axioms in the following way:
Replace every existential quantifier <for some x P(x)>
with <for some x (P(x) and for some y x is a member of y)>.
Replace every universal quantifier <for all x P(x)>
with <for all x (P(x) if for some y x is a member of y)>,
except the quantifiers in the axiom of extension.
Add the axiom schema, for each property P, <for some x for all y
(y is a member of x iff (P(y) and for some z y is a member of z))>.
Now you have axioms for type 1 class theory (or just class theory).
If you start with ZF set theory,
the above changes get you GB class theory.
(The usual GB axioms are simpler but equivalent.)
My idea is to iterate this process.
Given axioms for type n class theory,
make the above modifications to get axioms for type n+1 class theory.
The things described by type n+1 class theory are type n+1 classes.
The members of type n+1 classes may be interpreted as type n classes.
A proper type n+1 class is a type n+1 class that isn't a member
of any type n+1 class: a type n+1 class that isn't a type n class.
Here is a useless (AFAIK) application to category theory:
Since the objects of a category may be a class, not just a set,
there is a category of all sets (and the functions between them).
However, there is no category of all categories,
only a category of all small categories:
categories whose class of objects is also a set.
This is good; the category of all categories
leads to the same contradictions as the set of all sets.
However, just as there is nothing wrong with the category of all sets,
there is nothing wrong with the 2category of all categories.
Of course, there is no such thing, since there is no class of all
categories.
But there is a type 2 class of all categories.
In general, if you allow ncategories to have a type n class of objects,
then you can always form an (n+1)category of all ncategories
(and their covariant mfunctors), not just of all small ncategories.
It seems, intuitively, that type omega class theory might exist,
but I don't see how to write down axioms for it.
(Then omegacategories could be interpreted as type omega classes.)
Maybe there is such a thing as type alpha class theory
for arbitrary ordinals alpha. That would be neat.
-- Toby Bartels
to...@ugcs.caltech.edu
PS: Let a type n set be a type n-1 class.
Let the type 0 set be the empty set.
Then a proper set is the same thing as a nonempty set.
In set theories that include atoms,
let a type 0 set be any set whose members are all atoms.
(This is when type 0 sets have any point.)
With this sort of numbering, an nset has a type n set of objects,
where an nset is an (n-1)category, and the only 0set is the empty set.
By numbering ncategories as (n+1)sets,
you have an analogy with ngroups, nvector spaces, and the like.
But this is not important.
-------------------==== Posted via Deja News ====-----------------------
http://www.dejanews.com/ Search, Read, Post to Usenet
Richard G. Heck, Jr.
I could be seriously wrong, but I'm not sure why this doesn't amount to
a re-formulation of higher-order ZF, in the guise of a first-order
theory. Isn't that what GB is, in essence, anyway? What look like axioms
stating the existence of classes are in effect the comprehension axioms
of second order logic. And then the type-2 classes, or whatever, are
third-order things, and so on and so forth. If that's right, then
standard sorts of constructions of omega-order logics will get the
extension you want, and so on and so forth.
However, it would seem that there can't "really" be such a theory for
every ordinal. Won't there end up being more things at the relevant
ordinal level than there are ordinals? and so things? That's not very
well expressed, but maybe you see the worry.
Richard