Can Ackermann set theory find a natural interpretation in light\heavy class dichotomy?

Question

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 quasi-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.

   Let $V$ denote the class of all sets.

3. Pairing: $\forall a,b \in V \exists x \in V \forall y (y \in x \leftrightarrow y=a \lor y=b)$

4. 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)$$

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

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

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

7. Foundation over all classes.

8. 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 an endeavor 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 classes 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 from both approaches.

Answer 1

This question is more subtle than I originally thought. The answer is that the theory is consistent assuming some large cardinal hypothesis, the existence of $0^\sharp$.

If $0^\sharp$ exists, then there is a club class $C$ of ordinals which are order-indiscernible for $L$. For every limit ordinal $\alpha \in C$, $Hull(C\cap \alpha) = L_\alpha$. Every $\alpha \in C$ is inaccessible in $L$.

Let $\lambda$ be the $\omega^{th}$ indiscernible, and let $\kappa$ be the next indiscernible above. Consider the model $V_{\kappa+1}^L$, which satisfies MK. $Set$ is interpreted as members of $L_\kappa$, and $Hv$ is interpreted as sets of rank $\geq \lambda$.

Let us verify the Refleciton Axiom (6). Suppose $p \in V^l$. Then there are indiscernibles $\alpha_0<\dots<\alpha_n <\lambda$ and a definable Skolem function $f$ (in the language of ZF) such that $p = f(\alpha_0,\dots,\alpha_n)$. Let $\varphi(x,y)$ be a formula, and suppose $V^L_{\kappa+1} \models \varphi(L_\lambda,f(\alpha_0,\dots,\alpha_n))$. Let $\beta$ be an indiscernible, $\alpha_n < \beta < \lambda$. Then by indiscernibility, $V_{\kappa+1}^L \models \varphi(L_\beta,f(\alpha_0,\dots,\alpha_n))$. This verifies the axiom.