I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: [Holmes - NF is consistent, p:11](https://arxiv.org/abs/1503.01406), [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](https://randall-holmes.github.io/Papers/tangled.pdf)]) can be written completelly without any reference to sequences, i.e. written only in terms of types.



> 
> In particular does the following theory have exactly the same axioms of $\mathsf{TTT}$?
> 
> 
> 


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\_i^n = x\_j^m$ is well formed formula only when $ n=m$, and $x\_i^n \in x\_j^m$ is well formed only when $n < m$.


**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 in which $ x^i $ is not free.



Can we write Tangled Type Theory without reference to type sequences?
No it is not the same. The type sequences are absolutely needed, in some form.


--Randall Holmes (author of the theory in question)


The theory you describe is provably inconsistent.


The formula has to be the result of replacing the variables in an axiom of ordinary TST (indexed by type in the usual order) with variables of types determined using a strictly increasing sequence of TTT types. This is unavoidable. Finite sequences could be used in place of the infinite ones I use, but this is a complication, not a simplification.


