# Advantage of ZF over other set theories such as New Foundation

What would be the advantage of adopting ZF over other set theories such as New Foundation?

I am very curious, since it seems that there is no reason just to stick with ZF.

Edit: What about set theories other than NF? And why is NF's finite axiomatization possbility not attractive?

• Have you had a look at en.wikipedia.org/wiki/New_Foundations? – Gerry Myerson Jun 2 '12 at 5:52
• Familiarity. And for most things that most mathematicians do, all one needs is something that works well and that one can basically forget about. And, by the way, NF is weird. – André Nicolas Jun 2 '12 at 5:53
• What @André said. Squared. – Brian M. Scott Jun 2 '12 at 6:02
• To add a bit to André's comment, NF also refutes Choice, which is something I feel that most mathematicians appreciate (even if they are not consciously aware of it). – user642796 Jun 2 '12 at 7:15
• What about other systems? I was just giving NF as example. And by the way, why wouldn't finite axiomatization possibility of NF be attractive? – user32600 Jun 2 '12 at 7:38

There are two very good reasons to stick with ZF:

1. Historical reasons which really amount to "if it ain't broken, don't fix it." sort of argument. We have a very adequate foundation with ZF[C] for most mathematics, and large cardinals axioms also "tame" the modern parts which require collections whose size is too big.

2. I was told by a prominent set theorist once during a break between lectures that a "good axiomatic system" is one that you don't feel you are using. That is, the axioms describe perfectly how you perceive the objects you axiomatize.

ZF has this property, and the only axiom in ZF which makes "no sense" at the beginning is the axiom of regularity, which if you think about it enough, you understand that it really is a reasonable axiom from a philosophical point of view.

Other set theories, especially set theories from the first half of the previous century, often "lose" to ZF over one of the following reasons:

1. Being weaker or equivalent to ZF (in consistency strength), which means that you either can find things provable from ZF; or that you could have used ZF from the start.
2. Having too many types of objects, whereas ZF is simple: we only have sets.
3. Unclear axioms, which require a lot of careful attention, which counter the second point: clarity of the axioms.
4. Bad timing. Perhaps if NF was the first set theory we would have found it more natural. It came later, and it was strange... ill-founded; no choice; no power sets; universal set... all those clash with how we perceive sets (the ZF way).
• The impression I get is that the oddities of NF come from the way that it flattens Russell's universe. The non-existence of a powerset is somewhat unsurprising then: after all, even in ZF, if you have a nested hierarchy of universes, the powerset may change when passing from one level to another... – Zhen Lin Jun 2 '12 at 11:35
• But even if the power set changes, every object which I perceive as a set has a power set. If the universe itself is a set, then it cannot have a power set. – Asaf Karagila Jun 2 '12 at 11:43
• Cantor's theorem is a little more subtle than that in NF, though. Apparently, the powerset of the universal set is itself, or something smaller. (This reveals perhaps the main weakness of NF: not enough functions!) – Zhen Lin Jun 2 '12 at 12:37

Here's another reason.

Non-logician mathematicians generally don't like to have to worry about the syntactical details of the logic they are using. In ZF, it is possible to do "naive" set theory in which you ignore the formal syntax of the logic. You can informally use separation to form any set as long as it is a subset of a set that you already have. Formally, of course, the axiom of separation is not that loose, but in practice ignoring the difference usually causes no trouble when people act reasonably. So it is possible to write an entire book for undergraduates on ZF set theory without every mentioning a definition of a formal language, and this book can go quite far, including cardinals and ordinals and such.

On the other hand, in NF the axiom of separation only applies to stratified formulas. Many times in NF, when you want to form a set you have to write down a formula that defines the set and verify that the formula is stratified. Practicing mathematicians are not fond of that; they want to be able to focus on the mathematics rather than on the logic used to formalize the mathematics. And it's not very easy to write a "logic free" undergraduate book about NF in the same way as ZF.

In my site http://settheory.net I provide explanations on the main issues and paradoxes at the foundations of mathematics, with the articulation between set theory and model theory. I explain in details the difference of meaning between sets and classes, and the relative degree of justifications of different axioms. These explanations clearly show in particular that there is no universal set in nature, so that axiom systems admitting one such as New Foundations, may be studied as logical curiosities but cannot be accepted as a "natural" foundation for mathematics.

I give a justification for the consistency of ZF (showing that the one doubtful axiom is the powerset axiom, which we need anyway as far as I know), and find it relevant as a basis for the work of professional set theorists studying relative consistency issues.

But I propose another formalization accepting functions as fundamental objects aside sets, and many symbols instead of one, that I consider more appropriate to start mathematics from scratch : to facilitate the understanding of basic mathematical concepts, make the first developments of set theory simpler and more intuitive, and better fit with the common practice of mathematics that uses many symbols. Indeed I see the usual construction of ordinary mathematical tools from the mere membership predicate as unnatural, overcomplicated and irrelevant for beginners.

• In his work on set theory von Neumann already regarded functions as primitive notions, whereas Bernays in his formulation took membership to be elementary. For most people the building of the majority of mathematics within ZFC is redundant, moreover if you do want a foundational theory it is better to have fewer symbols and less axioms. Foundations should be relatively simple. Adding more symbols may be useful or may confuse whoever works with the theory. – Asaf Karagila Jun 19 '12 at 15:30

If you want to see modern theory for mathematical logic, have a look at lambda calculus and type theory and especially Martin-Löf type theory, which is implemented in the proof assistant Coq. This is pure constructive logic, and in fact too constructive to do set theory.

You can also look at Voevodsky's univalent foundations a work-in-progress based on Coq which would be suitable for all maths, in a constructive way.

ZF is far from being perfect, but every set theory have more or less the same problems that ZF has. Modern foundation proposal try to take advantage of the deep links between proofs and computation.

• But ZF is not a theory for "mathematical logic", is it now? – Asaf Karagila Jun 2 '12 at 8:42
• No, I don't mean that. It seems to me that in type theory things are differently balanced : a much richer logic, a very few (or none) axioms. – Lierre Jun 2 '12 at 8:53
• And by the way — I should have make it clear sooner —, I'm not at all a specialist. I what I say is crap, just explain me why and I'll be happy to learn something. These day I've been playing with Coq which does not seem to be very well-know on math.SE, that's wy I wanted to talk about it a bit. – Lierre Jun 2 '12 at 9:04
• @Lierre, I'm writing my master thesis on homotopy type theory and I did a bit of Coq hacking too. If you have any questions, now you know that there's at least somebody who can understand them. I'd be happy to answer any :) – Egbert Jun 2 '12 at 9:11
• @Egbert: I'd have some questions, if you're up to it. I'm a physicist and take some formal notes (on the wiki you find on my page). I've written down a set theory axioms for foundations, but I also want to take notes on categories and types (+HoTT). For this I try to patch things together so I get some kind of consistency. In particular I try to squeeze sets into my type system somehow, this is the bulk of it. If you're motivated, please write me a mail (first paragraph) and make some comments/extend what I mean. – Nikolaj-K Apr 4 '14 at 9:42