[Mathnerd314]

While you're around, I have a question: In TST, the restriction for x^m in y^n is that n = m+1, i.e. the level must increment by 1. In TTT, the restriction is instead that m < n, there is no requirement that it only be 1. Now, in NF, the restriction for set membership in stratified formulas is also +1. Is it possible to relax this to a "Tangled NF" where the set membership restriction is only that m < n? This would resolve issues such as how many levels it takes to construct an ordered pair.

[randallholmes]

No, the Tangled NF you suggest would be inconsistent.

[Mathnerd314]

Well, there is that proof that stratified comprehension works, https://randall-holmes.github.io/head.pdf#page=41, based on encoding x^(n-1) ∈ y^n as ({x}^n,y^n) ∈ [∈], where the existence of [∈] = { ({x}, y) | x ∈ y } (or its containing relation [⊆]) is an axiom. I don't see why you can't similarly encode x ∈ y as ({{x}},y) ∈ [∈2] where [∈2] = {({{x}},y) | x ∈ y }. From what I can tell, the existence of [∈2] is required by relative product, [∈2] = {(x'', y) | for some x', x'' [∈] x' and x' [∈] y }. Similarly [∈n] exist for all n>0. Then an occurrence of x ∈ y in which x has type n − k and y has type n can be replaced by ι^(N−(n-k))(x) [∈k]^ι^(N−n) ι^(N−n)(y) and the formula can be stratified. So it should just be equivalent to normal NF.

[randallholmes]

Work out the details. It won't produce what you describe above.

[randallholmes]

Jensen's consistency proof for NFU can be read as relying on the consistency of TTTU, which is actually very easy to show.