randallholmes
No user record in our sample, but randallholmes has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but randallholmes has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
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…
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…
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…
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…
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…
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…
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…
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…
It does, but I rather like "twisted type theory" :-)
Both are very important.
I have shown the consistency of New Foundations. My aim is not actually to promote it as a working set theory. NFU, which admits Choice, is probably better for that. But if there are people who want to use NF as the…
Jensen's consistency proof for NFU can be read as relying on the consistency of TTTU, which is actually very easy to show.
It certainly isnt a proof of equiconsistency between NF and the Lean kernel. The theory implemented in the Lean kernel is considerably stronger than NF.
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.
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…
It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
and it very much IS an essential part of my confidence in this proof that conversations between me and Sky Wilshaw reveal that she understands my argument [and was able to point out errors and omissions in paper…
The problem I express relates to the issues people mention about libraries: if a defined concept is used, one has to be sure the definition is correct (i.e., that the right thing has been proved). Wilshaw's…