I want to coin the notion of *heaviness* of a set 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][1], 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][2], 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.


  [1]: https://en.wikipedia.org/wiki/Ackermann_set_theory
  [2]: http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF