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?

Solution 1:

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

Solution 2:

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.

Solution 3:

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.

Solution 4:

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.