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.

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 foundation, it is now seen to be as secure as a rather small fragment of ZFC.

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

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 versions!]

human interaction helps create confidence. But the software is extremely reliable: a philosophical challenge based on bugs in theorem proving software just is not going to hold water.

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 vulnerable to this objection, though libraries were used. What is proved is that a certain defined concept satisfies a certain suite of formulas of first order logic. If there is a predicate satisfying that suite of formulas, NF is consistent.

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 read the conclusions carefully to make sure that the right thing is actually proved.

I read Wilshaw's final conclusions carefully, and she did indeed prove what needed to be proved.