Is there a relation between the ZFC set axioms and our intuitive notion of sets? A question about history.
When I took my first course in set theory, I had the perception that ZFC axioms weren't the most intuitive thing in relation to what common people would usually call a set. So I have this curiosity: is the intention at using them to formalise our intuitive notion of sets (in the sense of 'a collection of things' but avoiding paradoxes) or rather are they just used because all mathematics (all the stuff that is done in analysis, algebra, etc.) can be built upon them?
If the first is true, how is that correspondence between ZFC sets and the ordinary use of 'set'?
If the second is true, what is mathematics about? I have the idea (please correct me if I'm wrong) that mathematics is generally based upon sets, specifically ZFC sets. But if a set is just 'a structure upon which mathematics can be done', what are then the foundations of mathematics?
Thanks!
 A: History, unfortunately, is more complicated than your choices permit.
Presumably, Zermelo had proposed his 1908 axioms in support of his well ordering theorem. In so far as his axioms might relate to intuitive notions of set, his original axioms admitted urelements and relied on singletons to substantiate the truth of equality statements. The idea that a theory of pure sets suffice for mathematics is attributed to Skolem as far as I know. With a little further consideration, this may be seen as assuming the arithmetization of mathematics.  As such, one must recognize the chicken and egg problem that arises if linguistic symbols that are not pure sets become conflated with some Goedellian encoding for the sake of claiming that everything is a set.
Zermelo's reliance on singletons reflects the relationship of his system with Frege's logic. Category theorists claim that Zermelo had to make s choice between differing views expressed by Frege and Cantor. Since the relevant text is not translated into English, I cannot judge this claim. Nevertheless, Frege speaks of object identity and concept identity in a circular fashion that arises from Leibniz' principle of the identity of indiscernibles. Zermelo's use of singletons ought to be understood in this context. Foundationalism in the sense of Russell's logical atomism stipulates that object identity is fundamental. Hence, one has "first-order logic" with the proviso that "identity" is a "second-order" concept.
Since modern accounts of Zermelo-Fraenkel set theory are now based upon the first-order paradigm and the presumption that a theory of pure sets suffice for mathematics, urelements are treated in a derivative theory often called ZFA where the 'A' stands for (logical) atoms. The theory assumes that the urelements form a set (in conformance with the "everything is a set" presupposition). And, it is an important theory because of the models that arise from permuting the urelements.
It is, however, entirely plausible to understand urelements with respect to an antichain relation in a different signature.
Among other things to be found in Russell's writings, is the question of how a set is comparable to an object. While no one would ask that particular question today, the fact that urelements are not sets means that an antichain whose denial yields an order based on membership is entirely conceivable.
Such a theory would permit one to assert how non-sets satisfy the real number axioms, for example.
Understanding the distinction between urelements and sets in this manner permits one to understand how Cohen's forcing can extend a given model with "ideal subsets." The axiom of extension is contingent upon the denial of an antichain.
But, since such a view is not of interest to established mathematicians, students of set theory need to focus on the affirmative claims of first-order logic and set theory without concern for "intuition."
With regard to your second question, let me suggest that you look at the papers by Augustus de Morgan found in Ewald's two-volume anthology, "From Kant to Hilbert. "  This will provide you with a good foundation for understanding what the assertion, "mathematics is formal," really means.
The received view corresponding with first-order model theory reduces mathematics to language signatures, stipulation of relations and operations involving the symbols of such signatures, and a specification of the arities for each symbol in the signature. These constructs are often called "similarity types."
Of course, the "first-order" designation goes back to the foundationalist stipulation that object identity is fundamental.  So, language signatures will contain a symbol denoting an extensional domain of discourse. Extension is important to mathematical practice so that linguistic expressions intended to have "the same meaning" denote "singularly."
It had been Skolem's criticism of Zermelo's theory that gave impetus to this use of language signatures in mathematics over the notion that "mathematics is extensional." This particular claim arises from a different history. It is, of course, important for model theory. But, in the model theory of set theory it yields the "unfolding" and "geology" of possible models studied by set theorists using Cohen's forcing. What Skolem observed about Zermelo's axioms is that they could not be "categorical" in the sense of specifying a single, unique interpretation of the language symbols.
