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.
Mathnerd314|1 year ago
randallholmes|1 year ago