[FOM] Why ZF as foundation of mathematics?

[D. Klein]

Dear readers (Sirs AND madams), dear Zuhair Al-Johar

Rather than reacting to your suggestion, I'd like to elaborate a bit more on the question in the title - hoping that some people on the list who thought more about it throw in some comments. 




It seems that the question on why ZFC happens to be in the situation it is yet, or more generally on how to choose between different systems as foundations of mathematics has many dimensions, some of them being a tradeoff between mathematical and philosophical motivations. 

Relevant points seem to you:

- historical contingencies (most of your quotes on ZF seem to point at least partially to this dimension)

- inner-mathematical reasons (weakness/strength, easiness to actually derive theorems, closeness between the formal systems and "informal" mathematical arugments ...)

- Ontological harmlessness (rather one than two types of objects, first order ...)

- Intuitiveness: In a fairly  intuitive  sense, we want to be sure to not just talk about some mathematics, but "the" mathematics, as the "right" abstraction from the outside world. In this sense we want axioms to be "beyond discussion" in a sense that anybody interested would more or less immediately accept the axioms as being true beyond any reasonable doubt, in a metalogical sense, of course.  This seems to be, for instance, a claim that distinguishes ZF from Homotopy Type Theory: I'd be able to sell the axioms of ZF to most people on the street as capturing "what they always took to be true about sets. Thus, I'm pretty sure to (be able to) create consensus on the truth of mathematical arguments following from these axioms. With HoTT in contrast, it seems to me that it takes some fairly advanced mathematician to actually see that the kind of axiomatic statements made should be necessariily true and we should all agree on that (for metalogical reasons). So in a sense, we can be less sure that there is a uniersal acceptance for these axioms than for the ZF axioms.

On the other hand, both axiomatic systems only have consent of an educated insiders group (people having attended something equivalent to a western style primary school vs. a bit further advanced mathematicians), still the kind of ingroup consent seems to add sth. to the argument. 

- Applicability: part of an axiomatic system is the implicit promise that  most "real life" mathematical arguments (i.e. stuff said by people in PDE, topology, algebraic geometry...) could be formalized in it. Again, this claim has two dimensions: Is the formalization achievable in principle, and is it even achievable within a reasonable amount of time, effort and creativity. As I take it, one of the main motiations of the homotopy type program is the second question. The first dimension seems to be one of the main dividing lines between typed and untyped systems: The necessity to control for stratifiedness in any formalisation definitely reduces my subjective belief of the existence of such a formalisation. 


Did I forget any dimensions?

All the best,
Dominik

________________________________________
Van: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] namens Zuhair Abdul Ghafoor Al-Johar [zaljohar at yahoo.com]
Verzonden: zondag 10 november 2013 23:36
Aan: fom at cs.nyu.edu
Onderwerp: [FOM] Why ZF as foundation of mathematics?

Dear Sirs,

ZFC is been mentioned as the foundation theory of mathematics:

Some quotes:

"Today ZFC is the standard form of axiomatic set theory and as such is the most common foundation of mathematics" [Wikipedia]

"Russell's Paradox can be avoided by a careful choice of construction principles, so that one has the expressive power needed for *usual mathematical arguments* while preventing the existence of paradoxical sets. See the supplement on Zermelo-Fraenkel Set Theory" [Thomas Jech: Stanford Encyclopedia of Philosophy]

Also Thomas Jech in his "Introduction to Set Theory" makes similar remarks about ZF role in codifying mainstream mathematics.

On the other hand it is well known that most of mainstream mathematics can be formalized in second order arithmetic, which is way weaker than ZF.

So why ZF is mentioned for that purpose if much weak class\set theories can do the job of formalizing mainstream mathematics in set theory?

I suggest a simple alternative class\set theory in mono-sorted first order logic language with a single extra-logical symbol, that of class membership, all objects are classes. The followings are the axioms:

[1] Given a property there exists a class of all sets(i.e., elements of classes) that satisfy that property.
[2] for any "singleton or empty" classes A,B; the class
{x|set(x) & (x=A or x=B)} is a set.
[3] Extensionality over all classes.

This has the strength of second order arithmetic, has much simpler structure than ZF (proves only classes of hereditarily 'empty or singleton' sets and classes of pairs of those sets), and the axioms are dead simple.

Best Regards,

Zuhair Al-Johar
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom