The following theory contains a comprehension axiom that is a naive like schema. This theory definitely looks inconsistent at first glance. However, I tried to find this inconsistency, but to no avail. The main idea pivotes around an *acyclic* membership relation $\in^*$, so an acyclic member of a set is an element of a set that doesn't contain that set in its transitive closure. Now, this theory allows free construction of sets after all formulas in the language FOL(=, $\in^*$).


Formal workup: 

Language: the first order language of set theory.

**Extesnionality:** $\forall x \, (x \in A \leftrightarrow x \in B) \to A=B$

**Transitive Closures:** $\forall x \exists t: t=TC(x)$

***Define:*** $t=TC(x) \iff trs(t) \land x \subseteq t \land \forall k (trs(k) \land x \subseteq k \to t \subseteq k)$

Where "$trs$" stands for "is transitive", that is: closure under relation $\in$

**Induction:** if $\phi$ is formula, then: 

$$\forall y \in x \ (\phi) \land \forall k \,  (\phi(k) \to \forall l \in k  (\phi(l))) \to \\ \forall m \in TC(x)( \phi(m))$$

 





***Define:*** $y \in^* x \iff y \in x \land \neg \, x \in TC(y)$

 
**Comprehension:** $\exists x \forall y \, (y \in x \iff \phi^*)$

Where $\phi^*$ is a formula not using $``x"$, whose predicates are among $=, \in^*$ symbols.

 Questions:

> Is there a clear inconsistency with this theory?

> If not, then can this theory prove Infinity?