FOM: Set Theory Axioms

[Harvey Friedman]

The point of this posting is to give some entirely conventional axioms for
set theory that are a bit simpler than many that are normally given. They
are fully formal. By comparison, look at the axioms of elementary topoi
that are given in MacLane/Moerdijk, Sheaves in Geometry and Logic, A first
Introduction to Topos Theory, Springer-Verlag, 1994, on p. 163. The
difference in complexity is strikingly grotesque.

I challenge anyone to write down their favorite fully formal axioms for
topoi that are sufficient to do real analysis, so we can compare them side
by side with the fully formal axioms I write down here.

Topos theory with natural number object is insufficient to develop
undergraduate real analysis - although many fom postings conceal this fact.
One has to add to topoi: natural number object, well pointedness, and
choice. The latter two are nothing more than slavish translations of set
theory into the topos framework. The "idea" is to take a fatally flawed
foundational idea and force it to "work" by transporting important ideas
from set theoretic foundations.

But the axioms of elementary topoi are already incomparably more
complicated than the axioms for set theory presented here.

Let me start with the dramatically simple axioms of finite set theory.
These amazingly simple axioms are tremendously powerful. We work in the
usual classical predicate calculus with equality and one binary relation
symbol epsilon - which we abbreviate here by "in." It is also useful to use
the constant symbol 0 (for the empty set), the unary function symbol { }
(for singletons), and the binary function symbol U (for pairwise union).
Note that axioms 2-4 amount to the most trivial of definitions.

1. (forall x)(x in a iff x in b) implies a = b.
2. (forall x)(not(x in 0)).
3. x in {a} iff x = a.
4. x in a U b if and only if (x in a or x in b).
5. [phi(0) & (forall x,y)((phi(x) & phi(y)) implies phi(x U {y}))] implies
phi(x).

Here phi(x) is any formula in the language in which y is not free.

That's all! One ***derives*** pairing, union, power set, foundation,
replacement, and choice, from these axioms alone!!! Also, when
appropriately formalized, "every set is finite" and things like "every set
has a transitive closure." These axioms are "practically" complete - an
informal concept that I have alluded to before on the fom.

Now for ZFC. We take a different tack and only use epsilon.

1. (forall x)(x in a iff x in b) implies a = b.
2. (therexists x)(a in x & b in x).
3. (therexists x)(forall y in a)(forall z in y)(z in x).
4. (therexists x)(forall y)((forall z in a)(z in y) implies y in x).
5. (forall x,y)(x in y implies (therexists z in y)(forall w in z)(w notin y)).
6. (therexists x,y)(x in y & (forall z in y)(therexists w in y)(z in w)).
7. (therexists x)(forall y)(y in x iff (y in a & phi)), where phi is any
formula in the language in which x is not free.
8. (forall x in a)(therexists y)(phi) & (forall x,y,z)((phi(x,z) &
phi(y,z)) implies x = y) implies (therexists w)(forall x in a)(therexists
unique y in w)(phi),

A novelty is the axiom of infinity, 6, is simpler than usual; and also
choice and replacement are combined nicely by 8. This allows such a simple
axiomatization in purely primitive notation. Try to right down the axioms
of a topos with natural number object, well pointed, and choice, in simple
primitive notation!! Good luck.

As is well known, ZFC is "practically" complete.

The version in the book on p.163 - which does not even include natural
number object, well pointedness, or choice - requires a very substantial
amount of preliminary abbreviations in order to formalize.