This question is related to but different from a previous question of mine.
I have been looking for an axiomatic set theory that handles classes elegantly from a mathematical perspective. The best I have found in common usage is KM (Kelley-Morse) but it also falls short in some basic respects. Ackermann's class theory as adjusted by Muller gets even closer but seems to fail at the last hurdle (Muller Section 4.4), see Wikipedia for some very basic background.
So can anyone provide or point me to an axiomatisation with the following basic world-view
1) The ontology is classes (extension of a property).
2) Sets are a special type of class (definite collections of definite things).
3) Comprehension has the form $z\in\left\{ x\mid\phi\right\}$ iff $Safe\left[z\right]$ and $\phi$. This avoids Russellian paradoxes which reduce to $\neg Safe\left[R\right]$. The choice of predicate $Safe$ is critical, in KM and NGB it is $\exists u\left(x\in u\right)$, but this won't work here. For example it makes $\left\{ x\right\} =\varnothing$ whenever $\neg Safe\left[x\right]$, but we want to be able to form $\left\{ x\right\}$ and have it mean what a mathematician thinks it means.
4) I believe we must have $V$ the class of all sets as a primitive constant, otherwise we are constrained to defining $Safe$ in terms of $\in$. I think $V$ is part of the mental furniture of mathematicians anyway, and contains the sets of “ordinary” mathematics like real numbers and concrete Hilbert spaces.
5) We need comprehension to work on safe classes and sets to produce safe classes. Hence $x\in V$ implies $Safe\left[x\right]$.
6) Other axioms include extension, foundation, doubletons, unions, powers, substitution (not replacement), infinity and choice all in appropriate forms. For example the doubletons axiom would take the form “if $x,y$ are safe then so is $\left\{ x,y\right\}$ , and if they are sets so is the doubleton”. Choice may take the form of global choice since anything else is splitting hairs once you have $V$.
7) Maybe even GCH could be added, from a mathematicians perspective, maybe?
8) THE HARD BIT – It must be legitimate to finitely iterate the constructors provided by the axioms on all safe classes and sets. This is where Muller comes unstuck, his theory only works within $\wp^{n}V$ one level at a time.
9) It would be nice but not essential if we could form the collection of all safe classes so the category of categories could be formed as an object, although in fact the entire universe of discourse would "be" this category anyway.
There is no possibility of introducing new contradictions here if you believe ZFC is consistent, all we have above is a model $V$ of ZFC combined with a model $F$ of hereditarily finite sets that takes $V$ as its starting elements (instead of $\varnothing$) optionally combined with $\left\{ F\right\}$ itself. Another model may be $V_{\kappa+\omega+1}$ where $\kappa$ is inaccessible in ZFC.
I know ZFC plus a vast infintude of possible large cardinals is very interesting for many reasons, and casts light on the system I describe above. But thinking from a selfish mathematical perspective it leads into an endless hierarchy that serves no purpose except adding complexity, whereas I think if we could directly axiomatise the above system it gives us “ordinary” mathematics plus the machinery to deal elegantly with non-sets when we need them for mathematical objects on the boundary of the ordinary. This includes categories, surreal number structures, and similar.
I also know that ZFC plus the first two smallest inaccessibles may do the trick, but that is not in the spirit of axiomatising the above world view, I am after an axiom system.