The following is a first order MONOSORTED class theory, that is primarily motivated by an abstract hierarchy principle. It extends first order logic
with equality, its language has only two extra-logical primitives those of equality $``="$ and class membership $``\in"$. A class function $F$ is said to be *hierarchical* if and only if it sends ordinals to sets in such a manner that $F(A) \subsetneq F(B) \leftrightarrow A < B$. Now this theory stipulates that every hierarchical function if the class of all limit ordinals that are members of elements of its domain is equal in cardinality to some set, then the range of that function is a set. So this theory combines an accessibility principle with an abstract hierarchy principle. I tend to think that the result is equi-interpretable with $MK$ , however I'm not sure. Here is the formal exposition of it:

*Define:* $Set(X) \iff \exists Y (X \in Y)$

**Axioms:**

**Extensionality:** $\forall A,B [\forall X(X \in A \leftrightarrow X \in B) \to A=B]$

**Foundation:** $\exists Y (Y \in X) \to \exists Y \in X (\not \exists C \in Y (C \in X))$

**Comprehension**: if $\varphi(Y,W_1,..,W_n)$ is a formula in which only symbols $``Y,W_1,..,W_n"$ occur free (and only free), and in which the symbol $``X"$ doesn't occur, then : $$\forall W_1,..,W_n \exists X \forall Y [Y \in X \leftrightarrow Set(Y) \wedge \varphi(Y,W_1,..,W_n)]$$ is an axiom

*Define:* $X= \{Y|\varphi(Y,W_1,..,W_n)\} \iff \forall Y [Y \in X \leftrightarrow Set(Y) \wedge \varphi(Y,W_1,..,W_n)] $

**Set existence:** $\exists X (Set(X))$

**Pairing:** $\forall A,B,X [Set(A) \wedge Set(B) \wedge X=\{A,B\} \to Set(X)]$

**Union:** $\forall A,X [Set(A) \wedge X=\{Y|\exists Z \in A (Y \in Z)\} \to Set(X)]$

**Power:**$\forall A,X [Set(A) \wedge X=\{Y|\forall Z \in Y (Z \in A)\} \to Set(X)]$

**Subsets:** $\forall X,Y [ Set(X) \wedge Y \subset X \to Set(Y)] $

**Hierarchy:** $ \forall F \big{[} \forall M \in F \ \exists A,B (A \in ORD \wedge M= \langle A,B \rangle) \wedge \\ \forall A,B,X,Y ( \langle A,X \rangle \in F \wedge \langle B, Y \rangle \in F \to [A < B \leftrightarrow X \subsetneq Y] \wedge [A=B \leftrightarrow X=Y]) \wedge \\ \exists S (Set(S) \wedge |S|= | \{L | \exists A,B (\langle A,B \rangle \in F \wedge L \in A) \wedge \not \exists K (L=K \cup \{K\}) \}|) \\ \to \\ Set(range(F)) \big{]} $

Where $ORD$ is the class of all Von Neumann ordinals that are sets.

Question: Is this theory equi-interpretable with $MK$?