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)$](https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TalkAxiomSetThy-ts05xn.pdf) (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.



What is the consistency status of this theory?
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.


