linguistic:translation, quality:correction
Tangled Type Theory

Tangled Type Theory (TTT) is an extension of TST where each variable is typed by an ordinal rather than a natural number. The well-formed atomic formulas are x n = y n {\displaystyle x^{n}=y^{n}} and x m ∈ y n {\displaystyle x^{m}\in y^{n}} where m < n {\displaystyle m<n}. The axioms of TTT are those of TST where each variable of type i {\displaystyle i} is mapped to a variable s (i) {\displaystyle s(i)} where s {\displaystyle s} is an increasing function.

TTT is considered a "weird" theory because each type is related to each lower type in the same way. For example, type 2 sets have both type 1 members and type 0 members, and extensionality axioms assert that a type 2 set is determined uniquely by either its type 1 members or its type 0 members. Whereas TST has natural models where each type i + 1 {\displaystyle i+1} is the power set of type i {\displaystyle i}, in TTT each type is being interpreted as the power set of each lower type simultaneously. Regardless, a model of NF can be easily converted to a model of TTT, because in NF all the types are already one and the same. Conversely, with a more complicated argument, it can also be shown that the consistency of TTT implies the consistency of NF.