I'm currently working on some universal algebra using proper classes (in MK class theory), and I repeatedly run into situations where I want to collect together some proper classes as the members of a new algebraic structure. 


For example, the construction given [here](https://mathoverflow.net/questions/286791/name-for-this-algebraic-structure/286885#286885) yields a bunch of equivalence classes $\equiv/(m\_0,m\_1)$ for $(m\_0,m\_1)\in\mathbb{M}^2$, and if $\mathbb{M}$ is a proper class then each of these equivalence classes is a proper class. Despite this we would like to treat $\mathbb{M}^2/\equiv$ as a group, so to get around the problem we can technically collect together one representative from each equivalence class and be good to go with the class of representatives serving as the new group.


This feels clunky to me from a logical standpoint every time I have to do it, and it makes me wonder if there may be situations where we want to collect up some proper classes which do not admit representatives so simply. Consequently, I would like to add an axiom to MK which allows me to dictate one of two things:


1. I can collect together proper classes into 'hyper classes' under certain circumstances. This seems like the direct and obvious route at first; it is [suggested](https://mathoverflow.net/questions/273551/category-theory-from-mk-class-theory-perspective) by Andreas Blass under similar circumstances, however this would require an extension of the formal language of MK to include a relation symbol between proper classes and hyper classes that is not $\in$, and this bothers me. (this may bother me less as I learn more logic/model theory)
2. Classes which are definable as equivalence classes using the first order language of sets and a relation $\mathcal{R}$ on a class $\mathbb{B}$ (possibly a proper class) are sets.


The second one is more along the lines of what I want, but this form of it is inconsistent. For example, if we let $\mathfrak{G}(O\_n)$ be the Grothendieck ring of the ordinals as defined [here](https://mathoverflow.net/questions/287446/formalizations-of-the-matchstick-diagram-representation-of-ordinals/287451#287451) for $\omega\_1$ (just replace $\omega\_1$ with $O\_n$ in the construction), we technically need to take a quotient of $\mathfrak{G}(O\_n)$ by the equivalence relation $$\equiv=\{(\alpha-\beta,\gamma-\zeta):\alpha+\zeta=\gamma+\beta\}$$ to remove extra 'difference representations' of the same element in $\mathfrak{G}(O\_n)$. We now have that $\equiv/(\alpha-\beta)$ is a set for any choice of $\alpha,\beta$ under this new axiom, but $$\equiv/(0-0)=\{\alpha-\alpha:\alpha\in O\_n\}$$ is trivially in bijection with $O\_n$, a proper class. 




---


In summary, my question is:



> 
> What is a concise axiom that (when added to MK class theory) would allow us to collect together proper classes satisfying certain algebraic formulae as though they were sets? 
> 
> 
> 


If an extension of the language of sets with an additional relation for hyper classes seems the most concise option, I would be open to an argument in favor of that as well.


It also seems from the discussion [here](https://mathoverflow.net/questions/71765/are-proper-classes-objects) that I may want to simply consider collecting these objects together in the meta-theory, but I do not know what pitfalls await me if I try this apparently bold route.



An axiom for collecting proper classes
Really, what you want to have is a set-theoretic structure on top of the universe, with classes and meta-classes and hyper-classes and so on, in a set-theoretic realm continuing to build into ranks above the ordinals.


One can make this precise by talking about classes coding these meta-class structures. The process is referred to as *unrolling*, and goes back to Marek and Mostowski. 


The basic idea is to code these higher-order classes with well-founded class relations on the ordinals, in much the same way that one can code hereditarily countable objects by means of a well-founded relation on the natural numbers. One considers the family of such codes and then defines the corresponding natural element-of relation on the codes and the natural equivalence relation, which in the right theory is a congruence with respect to that element-of relation. 


If you start with a model of KMCC, which is Kelley-Morse set theory with the class-collection principle (this is strictly stronger than KM by a result of mine and Victoria Gitman's), then you can build a model of $\text{ZFC}^-\_I$, which is ZFC without the power set axiom, but with a largest cardinal, which is inaccessible. Basically, Ord itself turns into the largest cardinal of the higher realm, and you get $\text{ZFC}^-$ for the rest of the higher-order structure. 


Indeed, those two theories are bi-interpretable in a precise sense, and this is the answer to your question: if you have KMCC, then you can just jump into the unrolled universe, where the higher-order classes exist in a $\text{ZFC}^-$ context and the old Ord becomes an inaccessible cardinal and the largest cardinal. 


My student Kameryn Williams is writing a chapter in his dissertation about figuring out exactly what set-theoretic strength you need in order to have exactly which theories in the unrolled structure. For example, you basically need the principle of elementary transfinite recursion (ETR) in order for basic facts about the unrolling process to work out, and he has some level-by-level results about how the strength of second-order set theory in the base model is revealed by increased strength of set theory in the unrolled structure. I'll encourage him to post further information. 


