Recall the criterion of acyclic comprehension. This is shown to be equivalent to stratified comprehension for language $\sf FOL(=, \in)$, given minimal assumptions. [See here, and here].
Let Acyclic ZF be the theory axiomatized by axioms of ZF but with Separation and Replacement restricted to using acyclic formulas.
Now, if we extend Acyclic ZF by an automorphism that can shift an ordinal downwardly, then would such extension be consistent? If so, would this increase the consistency level of Acyclic ZF? And would that increment be huge?
Formally, the extension can done by adding a total unary function symbol $j$ to the signature of Acyclic ZF, and axiomatize:
Automorphism: $\forall x: j(x)=j[x] \\ \forall y \exists x: j(x)=y$
Movement: $\exists \operatorname {ordinal} \alpha: j(\alpha) < \alpha$
To spell out the conditions for acyclicity around $j$, we'd stipulate that there is an edge from the term symbol "$j(x)$" to "$x$" for each occurrence of "$j(x)$".
Of course this is known to be consistent if $j$ is external, i.e. not allowed in instances of Separation and Replacement. But, here the question is about when $j$ is allowed to be used in Separation and Replacement of Acyclic ZF.
