[randallholmes]

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.

[einpoklum]

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

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

[randallholmes]

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).

[randallholmes]

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 :-)

[sagebird]

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?

[randallholmes]

I don't understand what you mean here.

[klyrs]

> 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.

[randallholmes]

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 :-)