to the original poster,

the universe is a boolean algebra in NF: sets have complements, there is a universe.

The number three is the set of all sets with three elements (this is not a circular definition; it is Frege's definition from way back); in general, a cardinal number is an equivalence class under equinumerousness, defined in the usual set theoretic way, and an ordinal number is an equivalence class of well-orderings under similarity.

When you look at objects which lead to paradox (the cardinality of the universe, the order type of the natural well-ordering on the ordinals) then you discover the violence inherent in the system. Very strange things happen, which are counterintuitive. None of this depends on my proof to work: these are all features of NFU (New Foundations with urelements) which has been known to be consistent since 1969, and one can explore what is happening by looking at its known models, which are far simpler than what I construct.

So, is the article/project concerned with "just NF", or "NF with urelements"?

Also, now I have to go learn about urelements too :-(

The project is concerned with NF itself; the status of NFU was settled by Jensen in 1969 (it can be shown to be consistent fairly easily). Showing consistency of NF is difficult.

There is nothing mysterious about urelements: an urelement is simply an object which is not a set. To allow urelements is to weaken extensionality to say, objects with the same elements which are sets are equal; objects which are not sets have no elements (but may be distinct from each other and the empty set).

urelements aren't mysterious at all. They are simply things which are not sets. If you allow urelements, you weaken extensionality, to say that sets with the same elements are equal, while non-sets have no elements, and may be distinct from each other and the empty set.

Allowing urelements can be viewed as a return to common sense :-)

If urelements may be distinct from each other, or the same, it seems like you could place the universe under a type and name it urelement, without creating a new axiom -- Except for, a urelement defined in this way could never be equal to the empty set - hence the new axiom? Am I understanding this correctly?

I don't understand what you mean here.

> The number three is the set of all sets with three elements

I can't make up my mind if this is extremely elegant, or mindbogglingly horrendous; awesome or awful. I lean towards elegant, because the mindboggle caused by traditional set theory.

I think the Frege definition of the natural numbers is philosophically the correct one. This is a point in favor of foundations in NFU. I also think that Zermelo-style foundations are pragmatically better, so sadly I must let go of the first preference :-)

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.

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

No, the Tangled NF you suggest would be inconsistent.

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.

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

to clarify, when you look at objects that lead to paradox in naive set theory; they do not lead to paradox in NF or NFU; they exist but have unexpected properties.

at some objects. The Russell class cannot be a set in any set theory, that is logic. The cardinality of the universe and the order type of the ordinals do exist in NF(U) and have rather unexpected properties.