I'm taking the liberty of forwarding to the categories mailing list the following challenge posted by Harvey Friedman to Steve Simpson's Foundations of Mathematics mailing list. This is the latest in a long-running engagement about sets vs. categories on the latter list, recent postings to which can be read at http://www.math.psu.edu/simpson/fom/postings/9801.html Postings with "categor{y,ical}" in their subject lines are the relevant ones. Information about the fom list (how to subscribe etc.) can be found at http://www.math.psu.edu/simpson/fom/fom-info As we were fond of saying quarter of a century ago, Peace Vaughan Pratt ------- Forwarded Message Date: Fri, 23 Jan 1998 00:54:20 +0100 To: fom@math.psu.edu From: Harvey Friedman <friedman@math.ohio-state.edu> Subject: FOM: Set Theory Axioms 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. ------- End of Forwarded Message