How much of ZFC does Quine's New Foundations prove?

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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 http://math.boisestate.edu/~holmes/holmes/head.ps.

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