In "Rethinking Set Theory", Tom Leinster argues in favor of teaching axiomatic set theory via Lawvere's Elementary Theory of the Category of Sets with 10 axioms (but phrased in a way that requires no knowledge of category theory) which uses sets and functions as primitive elements compared to ZFC which uses sets and elements as primitives. (although if you really insist you can reintroduce elements as primitives at the expense of more clauses). This is weaker than ZFC but can be made equivalent to ZFC (or equiconsistent according to François G. Dorais) with the addition of a hardly ever needed 11th axiom.
http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html
How would set theory research be affected by using ETCS instead of ZFC?
Is ETCS less cumbersome than ZFC or more, or does it not matter? Does it make proofs longer/shorter or easier/harder?
Would automated theorem provers work better with ETCS?
To clarify, the question is not about the strength of ETCS: assume whatever is needed to bring ETCS up to strength with ZFC. The question is about practicalities of working with the ETCS axioms. I guess most mathematicians don't directly work with axioms of set-theory at all. So the question is: if your work does involve working directly with such axioms then what difference (if any) does it practically make to you as a set-theory researcher to use a different set of axioms that have equal strength. If I understand correctly the goal of Tom Leinster's paper was to reflect actual (non-set-theoretical)-mathematical practice but my question is about what set-theorists would do if they used these axioms. Assume also that for the purposes of this question ETCS refers specifically to the rephrasing used in this paper that is free of category and topos terminology. Perhaps this rephrasing should be renamed ETS. Adding replacement would give the name ETSR.
Best Answer
I like the fact that you asked this question, but I'm a little worried that it will be seen as "subjective and argumentative".
For the second question, I think a lot of set theorists (trained since childhood in ZFC) have gone on record saying they do find ETCS not easy to work with or not user-friendly, and I find this quite understandable. There is a critical hump of lemmas to get over in the beginning when working with ETCS, because unlike ZFC or some variation thereof, there is no ready-made comprehension scheme in ETCS (at least as it is ordinarily presented). Rather, a stock of instances of comprehension (where one builds up an "internal logic" by hand, as it were) have to proven before one is ready to fly. But after some point, with enough of these beginning lemmas under the belt, the development of mathematics, say of the core undergraduate curriculum involving basic results of real analysis, algebra, topology, etc., proceeds pretty much the same way as what one is used to. So in that sense, I'd say "it does not matter" for the needs of working mathematicians.
In developing his new set theory SEAR (Sets, Elements, And Relations), Mike Shulman recognized this cumbersome aspect of ETCS, quoting an analogy I made once about ETCS on the now-moribund "Todd and Vishal's blog":
So SEAR aims to combine the advantages of ETCS (as a truly "structural" set theory, where the aspects of sets we truly care about are isomorphism-invariant, and carry less "cruft") with the advantages of ZFC (where comprehension principles, etc. are built right in; see his axiom 1). SEAR will probably look more home-y and familiar to those used to traditional naive set theory; there is none of this intimidating "well-pointed topos with NNO and choice" business to wade through at the outset.