Editing New Foundations (section)

=== 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 <math>x^{n} = y^{n}</math> and <math>x^{m} \in y^{n}</math> where <math>m<n</math>. The axioms of TTT are those of TST where each variable of type <math>i</math> is mapped to a variable <math>s(i)</math> where <math>s</math> 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 <math>i + 1</math> is the power set of type <math>i</math>, 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.{{sfn|Holmes|Wilshaw|2024}}