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

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

I don't understand what you mean here.

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.

No, the Tangled NF you suggest would be inconsistent.

I have the same objection when people talk about defining set theories in such a way as to avoid the paradoxes. We don't avoid or work around the paradoxes: they are mistakes. We simply do things correctly, we do what we can do.

You don't work around what is impossible. A consistency proof for a theory T is usually a construction of a model of that theory in some context we have confidence in. Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality. And there are strong systems we have confidence in.

we are both in that conversation :-)

and we really don't use a large cardinal assumption...the existence of beth_omega_1 is really small potatoes. But, it is stronger than NF.

It's not really a workaround. Whenever we are proving the consistency of a theory T, we are implicitly working in a stronger system. That is just how consistency proofs are done. The incompleteness theorems do not say that we cannot prove the consistency of theories, or build models of theories...in a generally accepted theory such as ZFC. They do say that if we want to prove the consistency of ZFC itself we would need to work in an even stronger system.

It is no part of my agenda to promote the use of NF as an independent foundational system. It is a very odd one. But if someone wants to promote this, the consistency result says, it will work, at least in the sense that you are in no more danger of arriving at a contradiction than you are in ZFC.

I tried using it, and I could edit, but the update button did nothing; the edit never got posted. So I'll stick with little multiple replies for now.

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

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

The Quine pair works in ordinary set theory (Zermelo or ZFC); it has a mildly baroque definition but there is no problem with it. Look at the machinery and you will see why a pair (as opposed to a general set) doesnt strictly speaking need to be of higher type than its components.