In several set theories, among which Quine's NF is one of the best known and most extensively investigated, the existence of a Universal set V can be proved. V is the set of all sets-indeed all "proper classes", including V itself, are elements of V. Although it might be considered "meaningless" to ask what the "cardinal number" of V is, there are some questions of this type which one could ask. As far as I know, the consistency of NF relative to ZF is still an open question. But have any of the well known "large cardinal axioms" (assuming that they can be expressed in NF) been proved to be inconsistent with NF? If so, this might throw some light on the question of how "large" V really is.
-
$\begingroup$ It should be remarked that while NF has a universal set, $U$ and its subsets are indeed elements of $U$; one still have a notion of proper classes in NF. For example the Russell class of all sets which do not contain themselves cannot be a set, and indeed in NF it is not. But it is still a collection and we can still say meaningful things about the members of this collection (as we do with every non-empty collection). $\endgroup$– Asaf Karagila ♦Commented Feb 22, 2013 at 23:09
3 Answers
I believe that not much is known about NF itself and large cardinals - keep in mind that NF disproves the axiom of choice (Specker, 1953), and many large cardinal notions are not robustly defined in the absence of choice, in the sense that definitions equivalent over ZFC become non-equivalent without AC.
The system NFU (=NF + urelements), however, is much better behaved. It is known to be consistent - in fact, consistent relative to PA - and NFU does not disprove choice. (Although, having urelements, a universal set, and choice leads to the interesting situation in which the powerset of the universe is strictly smaller than the universe itself.) Over NFU+AC, we can attempt to define at least the smaller large cardinals in much the usual way.
That said, I don't' know anything about large cardinals in NFU, but I'd look at work of Ali Enayat (for example, http://academic2.american.edu/~enayat/Slides%20of%20Talks/Cambridge%20Slides.pdf) for starters.
Concerning the consistency of NF, Peter Smith made the following post last November on Logic Matters:
Randall Holmes has now announced “I believe that I am in possession of a fairly accurate outline of a proof of the consistency of New Foundations.”
He goes on to say “NF has the same consistency strength as TST + Infinity, has the same kinds of extensions as NFU in the same ways, has no interesting consequences for the combinatorics of small sets, etc. No surprises, this is a rather boring outcome in my opinion …” Well, I don’t know about boring! If Randall has indeed cracked this long-standing problem, it’s a major achievement. He is still editing the document, so nothing is released yet. However, Thomas Forster is organizing a conference here in Cambridge in the spring and Randall says he will “certainly be discussing this.”
And Thomas confirms ”I am indeed organising an NF meeting in Cambridge in the spring, current intention is last week of March and first week of April. The idea is that before Randall arrives there will be a warm-up act wherein the background and some preparatory material is set out for people who are not already familiar with it. Thus when Randall arrives we will all be primed and ready to go. … I am not at this stage soliciting other offers of talks, tho’ that may change. If you have something you think I may find irresistible by all means try to twist my arm. And – of course – contact me if you want to come.”
I'm not sure whether there has been any further news about this since then.
-
$\begingroup$ Joel: As far as I know the "jury is still out" in connection with Holmes' recent announcement. $\endgroup$ Commented Feb 23, 2013 at 1:37
-
$\begingroup$ Thanks for the update, Ali; we can all hope it holds together. $\endgroup$ Commented Feb 23, 2013 at 1:49
-
$\begingroup$ What's TST? Google only suggests Technical School of Toronto, and I don't think that would be equiconsistent with NF. :-) $\endgroup$– Asaf Karagila ♦Commented Feb 23, 2013 at 2:04
-
$\begingroup$ @Asaf: TST = Theory of Simple Types. $\endgroup$ Commented Feb 23, 2013 at 2:07
-
1$\begingroup$ I would assume Cambridge, England, since this is where Thomas Forster has his position. $\endgroup$ Commented Feb 24, 2013 at 18:44
We can say with fair confidence that $\sf NF$ is consistent relative to $\sf ZF$! So this question is practically a closed question. About large cardinals, most of those are studied with $\sf NFU$ and there is no proof of limitation of any of the known large cardinal axioms. $\sf NF$ can be extended in the same way $\sf NFU$ does, so you can extend it with axioms of Counting, Cantorian sets, Small and Large ordinals axioms. I think it is known that $\sf NFU$ is consistent with extendible cardinals or even higher. $\sf NF$, contradicting choice, might even be possible for it to be consistent with choiceless large cardinals, there is no proof so far of $\sf NF$ being inconsistent with them.
-
$\begingroup$ Does "fair confidence" at the beginning of your answer mean that people have vouched for the correctness of Holmes's proof (or another proof)? I haven't heard any news about that. $\endgroup$ Commented Apr 20 at 17:47
-
1$\begingroup$ @AndreasBlass, It's about Holmes's proof. Not "people" though. Lean verified it. "Fair confidence" is Holmes's own words. $\endgroup$ Commented Apr 20 at 18:54
-
$\begingroup$ @ZuhairAl-Johar This is the first I have heard that the proof was Lean-verified, do you have a reference for that? $\endgroup$ Commented Apr 20 at 19:05
-
$\begingroup$ @NoahSchweber, randall-holmes.github.io. Also, Holmes himself affirmed that to me. $\endgroup$ Commented Apr 20 at 19:07
-
$\begingroup$ @AndreasBlass, NoahSchweber, see also: logicmatters.net/blog $\endgroup$ Commented Apr 22 at 20:23