**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?



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


Pairing (true in NF), Choice (false) and Infinity (true) are well documented. I would expect that [Thomas Forster](http://www.dpmms.cam.ac.uk/~tf/)'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 reﬁnement 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.)


