# Can we alter MK axioms to allow “safe” operations on proper classes

I like $MK$ class theory, and occasionally read maths where authors say they are using MK and then write things like $\langle No,b\rangle$ or $\langle O,A,\circ\rangle$ where $No$ and $O,A$ are proper classes.

My understanding is that MK is set up so anything containing a proper class is empty, in particular $\{A\}=\varnothing$ and $\{A,B\}=\varnothing$ and $\langle A,B\rangle=\varnothing$ when $A,B$ are proper classes. MK defines a proper class as a class that is not a member of any class, so certainly $A\notin\{A\}$ in this case.

Obviously ZFC doesn't handle classes at all, there simply is no such thing, although we get around it by pretending first order statements are proxy classes. Yet we see $V=\bigcup_{\alpha\in On} V_\alpha$ written many places.

So my question, it would be nice to have a class theory that acts like MK on classes $X$ with $X\in V$ and $X\subseteq V$, and from there on allows finite iteration of "safe" operations like $\{\cdot,\cdot\}$, $\bigcup$ and $\wp$, so we could form $\langle V, \in\rangle$ for example. Has anyone come up with an axiomatisation that achieves this?

I know a Tarski-Grothendieck approach could be used, that is how the problem is dealt with in Category Theory, but to me that is pretty ugly. A never ending hierarchy of universes, and consequently inaccessible cardinals. Having to start by chosing a "favourite" universe, blah.

I have spent quite a lot of time trying to find an axiomatisation, the main problem seems to stem from the definition of set as $\exists y(x\in y)$ and comprehension. It is remarkable how intricately tied together all the MK axioms are and the slightest change seems to bring everything unstuck! One of the things I tried was a first order signature of $\langle\in, V\rangle$ so the universe is taken as primitive and can be used in comprehension $x\in y \iff x\in V \wedge \varphi$.

So I am curious if there is an axiomatisation for MK plus safe operations on proper classes. I think such a theory should have just one inaccessible cardinal $\kappa$ and be modelled by $V_{\kappa +\omega}$ .

• As an aside, the category theorists actually use the hierarchy. I.e. when interested in a universe $U$, they are interested in categories of $U$-small things, but these categories are $U$-proper classes, so if you want to do category theory with them you need to do that in a bigger universe. I think the modern perspective, though, is more along thinking of a universe as a parameter to category theory rather something you fix. – user14972 Nov 13 '17 at 4:24
• (also, I have the vague impression that BZC plus universes is enough for category theory, and ZFC already contains a model of that) – user14972 Nov 13 '17 at 4:27
• First order logic is not the best place to look for "type safe", or "type" for that matter. – Asaf Karagila Nov 13 '17 at 7:01