Hacker News Reader

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.

Reply on news.ycombinator.com