randallholmes

6 ms·

1.
by randallholmes 2y ago
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 fi
2.
by randallholmes 2y ago
Work out the details. It won't produce what you describe above.
3.
by randallholmes 2y ago
I don't understand what you mean here.
4.
by randallholmes 2y ago
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.
5.
by randallholmes 2y ago
No, the Tangled NF you suggest would be inconsistent.
6.
by randallholmes 2y ago
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.
7.
by randallholmes 2y ago
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 t
8.
by randallholmes 2y ago
we are both in that conversation :-)
9.
by randallholmes 2y ago
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.
10.
by randallholmes 2y ago
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
11.
by randallholmes 2y ago
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 mor
12.
by randallholmes 2y ago
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.
13.
by randallholmes 2y ago
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 disti
14.
by randallholmes 2y ago
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
15.
by randallholmes 2y ago
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
16.
by randallholmes 2y ago
It does, but I rather like "twisted type theory" :-)
17.
by randallholmes 2y ago
Both are very important.
18.
by randallholmes 2y ago
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 foundation, it is now
19.
by randallholmes 2y ago
Jensen's consistency proof for NFU can be read as relying on the consistency of TTTU, which is actually very easy to show.
20.
by randallholmes 2y ago
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.
21.
by randallholmes 2y ago
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.
22.
by randallholmes 2y ago
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 fro
23.
by randallholmes 2y ago
It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
24.
by randallholmes 2y ago
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 versions!] human interactio
25.
by randallholmes 2y ago
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 formalization is not vulner
26.
by randallholmes 2y ago
I would say that there is very little danger of a proof in Lean being incorrect. There is a serious danger, which has nothing to do with bugs in Lean, which is a known problem for software verification and also applies in math: one must re