MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Main Question: Does anyone know of a reference that can tell me which axioms of ZFC Quine's New Foundations prove, disprove, and leave undecided?

Secondary Question: I've read that diagonal arguments don't go through in NF and thus can't be used to prove that the reals are uncountable. Does NF manage to prove the uncountability of the reals by some other means or does that fact (normally rendered as "$P _1(\mathbb{N}) < P(\mathbb{N})$" in order to make sense in NF) turn out to be undecidable in NF?

share|cite|improve this question
up vote 18 down vote accepted

Hi Amit,

Pairing (true in NF), Choice (false) and Infinity (true) are well documented. I would expect that Thomas Forster's book addresses if not outright answers most of your question; I suppose one would need to restate things like replacement appropriately to even make the question meaningful for some formulas. The book is "Set Theory with a Universal Set: Exploring an Untyped Universe" (Oxford Logic Guides), 1995, and you may enjoy reading it anyway.

Thomas is also interested in ZF, so even if the book doesn't completely answer your question, he may help guide you through the relevant literature if you email him directly.

As for the secondary question, quite a few basic ZF facts go through for NF when reformulated as you suggest (this is part of the reason why Forster, Randall Holmes, and other NF researchers, are interested in ZF, and why set theorists like Jensen and Solovay have thought about NF). One of these facts is Cantor's result. You may also be interested in Greg Kirmayer, "A refinement of Cantor’s theorem", Proceedings of the AMS 83 (4) (Dec., 1981), 774.

(Email me in a few days if this doesn't work out, and I'll go across the hall and ask Randall.)

share|cite|improve this answer
New Foundations also proves the Power Set Axiom. The proof is in Halperin(1944). – Carlo Von Schnitzel Nov 26 '10 at 3:12
Yes, Pairing, power-set, union follow from stratified comprehension. Extensionality is an axiom. That choice is false is due to Specker: "The axiom of choice in Quine's new foundations for mathematical logic." Proceedings of the National Academy of Sciences of the USA 39, (1953) pp. 972-975. As a corollary, Infinity holds (suitably formulated, NF does not deal with Von Neumann ordinals; in NF, ordinals and cardinals are equivalence classes). Specker mentions in his paper another (silly) corollary, namely that GCH fails (as the proof that GCH implies choice can be formalized in NF). – Andrés E. Caicedo Nov 26 '10 at 6:14
New Foundations is just so weird. Just weaken extensionality to allow urelemente and it no longer proves infinity or the falsity of choice. It becomes consistent with choice and relatively consistent to ZFC. What is so special about atoms with NF that makes the theory so different? The other thing that always amazed me about stratification is that it succeeds in taking care of a whole bunch of paradoxes in the same way, namely by asserting that the universe is untyped. – Carlo Von Schnitzel Nov 26 '10 at 9:52

One twist one can give to the question is to reformulate it as: which axioms of ZF(C) does NF prove to hold in the wellfounded sets?
We know the following: extensionality, pairing, sumset, power set, stratified $\Delta_0$ separation. We *don*t know if infinity can be proved to hold in the wellfounded sets and we *don*t know if every wellfounded set has a wellfounded transitive superset.

share|cite|improve this answer

NF does prove Cantor's theorem in the sense you indicate, $|\mathscr{P}_1(X)|<|\mathscr{P}(X)|$ for any set $X$. The usual ZF proof goes through, because definitions in that proof which need to be stratified for it to work in NF, in fact are. But if you try to prove $|X|<|\mathscr{P}(X)|$, you no longer have the right stratification, so Cantor's theorem fails in NF in this sense (which is good, as the universal set $V$ can't have a lesser cardinality than any other set).

Generally speaking, in NF one cannot prove $|X|=|\mathscr{P}_1(X)|$ because the obvious bijection $x\mapsto \{x\}$ does not have a stratified definition. One way of increasing strength of NF-style theories is to assert that more and more sets are "Cantorian" in the sense that $|X|=|\mathscr{P}_1(X)|$ (or "strongly Cantorian" in the sense that the particular bijection $x\mapsto \{x\}$ exists). This idea goes back at least to some papers of Orey (if I recall correctly), and Holmes has had a lot to say about that. Solovay proved some interesting results that link up the consistency strength of such additional axioms (on top of NFU) with large cardinal axioms for ZF. See, e.g., the paper on NFUB here.

share|cite|improve this answer

I didn't see anyone specifically address the secondary question, so I thought I'd pipe in. In NF the natural numbers are provably Cantorian (see above for definition). Rosser's "Logic for Mathematicians" (available from Dover and a pretty nice resource) has a detailed proof on p.437. Basically, if $a \in n$ and $b \in m$ and $|a| = |\mathscr{P}_1(b)|$ then the relation pairing $n$ and $\{m\}$ turns out to be stratified and is a bijection between $\mathbb{N}$ and $\mathscr{P}_1(\mathbb{N})$. When you have such a bijection, Cantor's proof goes through in the usual fashion.

share|cite|improve this answer
Very sorry for the re-edit, but it did change the meaning of my answer. – Malice Vidrine Aug 13 '13 at 5:52

While I second (with highly biased motivation) the recommendation of Forster’s book, for questions like this an easier starting point than Forster’s book or Holmes’ articles might be Holmes’ book Elementary Set Theory with a Universal Set, originally volume 10 of the Cahiers du Centre de logique, with a corrected online version at

(This should perhaps have been a comment to the original answer, but I don’t have enough reputation points yet to post comments.)

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.