Let $K_2^+(W)$ be the following theory in the language $L(\in,W)$ with the constant symbol $W$.

**Extensionality:**$\forall x (x \in a \leftrightarrow x \in b) \to a=b$$\mathcal{Define:} \ set(x) \iff \exists y (x \in y)$

**Class comprehension:**if $\varphi$ is a formula in which $x$ is not free, then: $\exists x \forall y (y \in x \leftrightarrow set(y) \wedge \varphi)$Let $V$ be the class of all sets.

**Sub-world:**$W \in V$**Weak Sub-world Separation:**if $\varphi$ is a formula in which y is not free, then:

$$ x \in W \to \exists y \in W \ \forall z \in W \ (z \in y \leftrightarrow z \in x \wedge \varphi)$$

**Reducibility:**if $\varphi$ is a fromula in $L(\in)$ in which all and only symbols $x_1,..,x_n,y$ occur free, then: $$x_1,..,x_n \in W \to [\exists y \in V (\varphi) \to \exists y \in W (\varphi)]$$**Transitivity:**$\exists x \in W \ \forall y \subseteq W \ [transitive(y) \to y \subseteq x]$

If this theory is consistent, then I'd think it would interpret Friedman's $K_2(W)$ (page:7), which proves a standard model of ZFC + the existence of a measurable rank, and is consistent if the existence of an extendible cardinal is consistent with ZFC.

To quote Harvey Friedman on that:

We have proved that K2(W) proves the existence of a standard model of ZF + "there is a measurable rank." And ZF + "there is a nontrivial elementary embedding from some rank into some rank" proves the existence of a standard model of K2(W). Measurable ranks are an appropriate formalization of measurable cardinals in the ZF context with Choice. In ZFC, these are equivalent: i.e., V(a) is a measurable rank if and only if a is a measurable cardinal.

THEOREM 4.13. ZFC + “there is an extendible cardinal” proves the existence of a standard model of K2(W).

Now my Questions are:

- Is there a clear inconsistency with this theory?
- If not, then what is the consistency strength of it?
- which large cardinal axiom this theory can prove?

The idea is that $K_2^+(W)$ adds proper classes in $MK$ style, i.e. in impredicative manner. Would that addition result in increment in the consistency strength of this theory? I mean as far as proving large cardinal properties is concerned? do we need to go beyond extendible cardinals in order to prove its consistency? if so then how much far?

[*afternote*] I've noticed that there is a possible point of departure from Friedman's theory, that is the last axiom, here since we can construct classes, then we can define the class of all ordinals in $W$ which is something that Friedman's theory doesn't grant, perhaps the correct parallel of Friedman's theory is to re-write the last axiom as:

**Transitivity:**$\exists x \in W \ \forall y \subseteq W \ [transitive(y) \wedge y \in V \to y \subseteq x]$

However I'm still not really sure if the first axiom 6 of this theory is inconsistent, but it appears that the second axiom 6 is what really copies Friedman's theory.