I need to know if the following system is consistent, because I want to use it in presenting automorphisms over stratified versions of it. The system I'd label as "*Acyclic ZF*", which is $\small \sf ZF-Reg.+ acyclic \ AFA + Rank$, is obtained by adding a two place predicate symbol $\mathcal R$ symbolizing *is the rank of* to the language of $\small \sf ZF$, then replace Regularity by the following two acyclic AFA axioms: **Acyclicity:** $\forall x_1,..,x_n: \neg (x_1 \in x_2 \in x_3 \in ... \in x_n \land x_1=x_n)$ **Acyclic construction:** For every *acyclic* [accessible pointed graph][1] there exists a set whose membership graph is isomorphic to it, where the latter means the membership map on the transitive closure of that set. Now we define the unary predicate *ordinal*, symbolized by $\mathcal Ord$, as *transitive set of transitive sets*. To be emphasized here is that an ordinal can be a von Neumann or may not be so! If the ordinal is well founded on $\in$, then it is a von Neumann ordinal, if not then its to be called as a non-standard ordinal, or even more outrageously an *ill-founded ordinal*. We make axioms to the effect that the ranking relation $\mathcal R$ constitute a partial function from ordinals to sets such that the indexed sets would correspond to iterative powers similar to the buildup of the cumulative hierarchy. Formally this is: $\forall a,b,c,d: \mathcal R(a,b) \land \mathcal R(c,d) \longrightarrow [a=c \Leftrightarrow b=d]$ $\forall x: \exists y (\mathcal R (x,y)) \iff \mathcal Ord(x)$ $\forall \alpha \forall x \forall y: \mathcal R(\alpha, x) \land \mathcal R (\alpha+1, y) \longrightarrow y=\mathcal P(x)$ $\forall \alpha \forall x [(\not \exists \beta: \alpha=\beta+1) \land \mathcal R(\alpha,x) \longrightarrow x= \bigcup \{y: \exists \beta < \alpha ( \mathcal R(\beta,y)) \}]$ The last axiom is to restrict sets to those itrative stages, I'll consider it as a parallel to foundation, that is: **Para-foundation:** $\forall x \exists \alpha \exists v : \mathcal R(\alpha, v) \land x \in v$ > Now, is Acyclic ZF consistent? [1]: https://en.wikipedia.org/wiki/Rooted_graph#Set_theory