The following theory contains a comprehension axiom that is a naïve-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 $\operatorname{FOL}(=, \in^*)$.

Formal workup:

Language: the first order language of set theory.

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

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

$\DeclareMathOperator\TC{TC}\DeclareMathOperator\trs{trs}$* 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 a formula, then:

$$\forall y \in x \ (\phi(y)) \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?