This posting is a follow up of this
Language multi-sorted FOL, with sorts (types) indexed by the naturals, equality symbol restricted to same type, while membership symbol restricted from lower to higher types, i.e. $x^n_i=x^m_j$ is well formed formula only when $n=m$, and $x^n_i \in x^m_j$ is well formed only when $n<m$
A type-graph on formula $\phi$ is a graph on the type indices used in $\phi$, this is precisely defined (meta-theoretically) here as a set of singletons and unordered pairs where each pair in it is the Boolean union of two distinct singletons in it, the nodes are singletons of types, the edges are pairs of types. An acyclic graph here can be defined as a graph having no subgraph of it having as many edges as nodes. A linear graph is an acyclic graph in which no node has more than two edges springing from it, i.e. no singleton in it is a proper subset of more than two distinct pairs in it!
Axioms: Multi-sorted ID axioms +
Extensionality: $i=1,2,3,\dotsc; j=0,1,2,\dotsc, j<i \\ \forall x^i \forall y^i: \forall z^j (z^j \in x^i \iff z^j \in y^i) \to x^i=y^i$
Comprehension: $i=1,2,3,\dotsc; j=0,1,2,\dotsc, j< i \\ \exists x^i \forall y^j ( y^j \in x^i \iff \phi ) $
Where $\phi$ is a well formed formula with acyclic type-graph.
Now $\sf TTT$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the construction of $\omega$-models of predicative NF (and more), p:4-5]) seems to be equivalent to restricting $\phi$ in comprehension to well formed formulas having linear type-graphs, which is a special case of comprehension here, so this theory is an extension of $\sf TTT$. On the other hand, it is known that if we allow $\phi$ to be any well formed formula in this language then this leads to inconsistency.
Is there a clear inconsistency with this theory?
