By stratified ZF -Reg., it is meant the theory ZF - Reg. with restricting Separation and Replacement to stratified instances of them. 

>Is Stratified ZF consistent with having an *internal* non-trivial automorphism  $j$ from $V$ to $V$? 

That is we add a new primitive one place function symbol $j$ to the language of ZF, and add the axioms of $j$ being an automorphism over the whole universe of discourse, that is:

**Bijectivity:** $\forall x \exists y : j(x)=y   \\\forall y \exists x: j(x)=y$

**Isomorphism:** if $\phi(x_1,..,x_n)$ is a formula with $x_1,..,x_n$ being all of its free variables, then $$\forall x_1,..,\forall x_n \ [ \phi(x_1,..,x_n) \iff \phi(j(x_1),..,j(x_n))]$$

**Critical point:** $\exists x:  x < j(x)$

Where: $x < j(x) \iff \mathcal Ord(x) \land x \in j(x)$

Where: $\mathcal Ord(x) \iff \forall y \in x (y \not \in y) \land trs(x) \land \forall y \in x(trs(y))$

Where: $trs(x)$ stands for $x$ is transitive, i.e. every element of $x$ is a subset of $x$.



Where $``j"$ is allowed to appear in instances of the stratified separation and replacement.

> If this is allowed what would be the consistency strength of such addition?