What is the consistency status of this theory?

Question

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

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$

   $\mathcal{Define:} \ set(x) \iff \exists y (x \in y)$

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

3. Sub-world: $W \in V$

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

5. 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)]$$

6. 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:

1. Is there a clear inconsistency with this theory?
2. If not, then what is the consistency strength of it?
3. 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:

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

Answer 1

This doesn't add any strength, because you only asserted first order elementarity. If $(M,E,W)\vDash K_2(W)$, then $(2^M,E,W)\vDash K_2^+(W)$. This can be verified one axiom at a time, because comprehension doesn't effect any other axiom. Additionally, if you added $W\prec_1 V$, you would get inconsistency, because transitivity is a $\Delta_1^1$ property of a set.