Hi,
The actual elements used for a mathematical construction are never of interest. Imagine your reaction to an interruption at the beginning of
It's perfectly feasible to imagine that in say, descriptive set theory, properties of certain structures could be shown by showing (1) they have a certain cardinality, (2) sets of such cardinality have epsilon trees with a certain property and (3) using epsilon induction over such epsilon trees to prove something about our original structures. [I don't know of any such instances; I'm not a descriptive set theorist.] Alternatively, what about Godel's constructible universe. This seems to be a mathematical construction, and the actual element relation seems to be not only of interest, but essential to the construction.
a lecture on number theory, "Which construction of the natural numbers do you have in mind? Russell's or Van Neumann's?" My favorite example of the sort of perverse question one can ask if one were to take formal set theory seriously is "Does any simple group appear as a zero of the Riemann Zeta function?"
This is an interesting example. You state a question in mathematical English, and then criticise ZF for being able to express this question, while category theory cannot. One wonders what other questions stated in mathematical English---some of them perhaps perfectly sensible---can be stated in the language of ZF, but not in the language of category theory. I'd much rather that my formalisation of mathematics could state nonsensical things (consistency strength isn't an issue here), than to be living in the fear that my formalisation may be inadequate to express some sensible arguments. Two examples that I think are relevant to this debate. Category theorists are keen on statements to the effect that structures are defined by their universal properties. A typical book on topos theory may define an elementary topos as a category with finite limits and power objects. It then goes on to show that any topos has internal-homs. How? By defining the function space as a certain set of sets of ordered pairs... Let Nat(x) be the statement "x is a triple (omega,S,0) to which the Peano axioms apply". ZF |- "there exists x such that Nat(x)". This is sufficient to do arithmetic; after proving this single existential statement, one need never give a particular construction of the natural numbers again. Indeed, if one is really worried about these things, note that ZF+"Nat(omega)" (where omega is a new constant symbol) is conservative over ZF and then work in the latter theory, without ever fixing on a particular interpretation of ZF+"Nat(omega)" into ZF. Both category theory and set theory are amenable to working with mathematical structures by either explicit constructions or by uniquely characterising properites. In both category theory and set theory, we prove the existence of structures with certain uniquely characterising properties via explicit construction. Ralph.