I want to coin the notion of heaviness of a class as a function from classes to ordinals such that $$heaviness(x)=|TC(x)|$$, i.e. the heaviness of a class is the cardinality of its transitive closure.

Now I want to introduce a new unary predicate symbol to the language of set theory, that is the predicate "Heavy"; so we'll be working in mono-sorted first order predicate logic with primitives of equality $``="$, class membership $``\in "$, and the one place predicate symbol $``Hv"$ standing for is heavy.

The idea is to define a class theory that would interpret Ackermann set theory by a quazi-size criterion in a theory that has proper classes as top ranked classes.

Ontology: every object is a class.

$$\text{Define: } Set(x) \iff \exists y \ (x \in y)$$

Axioms are those of first order identity theory +

1. Extensionality: Two classes are equal iff they have the same members.

2. Class comprehension scheme: if $\varphi$ is a formula, then there exists a class of all sets for which $\varphi$ holds.

3. Dichotomy: $Hv(x) \wedge heaviness(y) \geq heaviness(x) \to Hv(y)$

In English: objects heavier than a heavy object are heavy.

$$\text{Define: } light(x) \iff \neg Hv(x)$$

4. Maximality: $light(x) \to Set(x)$

Let $V^l$ denote the class of all light sets.

5. Reflection: if $\varphi$ is a formula that doesn't use the symbol $``Hv"$, then: $$ \forall \bar{p} \in V^l \ [\varphi(V^l,\bar{p}) \to \exists x \in V^l \varphi(x,\bar{p})] $$, is an axiom.

6. Foundation over all classes.

7. Choice over all classes.

/Theory definition finished.

The thing with this theory is that if it works (i.e. if its consistent) then it would be providing some natural explanation for Ackermann set theory, since clearly the predicate $light$ would work as Ackermann's predicate $M$ which stands for "is a set" in Ackermann's system. However this system defines set-hood in exactly the same manner $MK$ defines it, but light classes seem to play the role of Ackermann's sets. Now Ackermann's proper classes are the heavy sets here. Additionally this theory captures the proper classes of $MK$ as well. This theory simply impart that Ackermann set theory can be interpreted in a try to maximally comprehend over light classes. This theory can easily capture the class separation axiom of Muller, and therefore it can easily interpret Muller's $ARC$ class theory, and thus would be adequate to work as a foundation for Category Theory, here large categories would be founded in heavy objects of this theory .

The question to be raised is:

Is there an obvious inconsistency with this theory?

The reason why I'm asking this, is because the way $MK$ works is fundamentally different from Ackermann's, so a clash would be expected if we try to define a theory that combine merits form both approaches.