basic constructions:
strong axioms
further
A structural set theory is a set theory which describes structural mathematics, and only structural mathematics. As conceived by the structuralist, mathematics is the study of structures whose form is independent of the particular attributes of the things that make them up. For instance, in ZF set theory, “the set of natural numbers” can be defined as the von Neumann naturals $\omega_N = \{ \emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}, \dots \}$ or alternately as the Zermelo naturals $\omega_Z = \{ \emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \dots \}$, but either definition has all the necessary properties (namely, the properties making it a natural numbers object in the category of sets, when equipped with an appropriate successor operation). See, for instance, Benacerraf’s paper.
The structuralist says, essentially, that the number “$3$” should denote “the third place in a natural numbers object” rather than some particular set such as $\{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}$ as it does in any definition of “the set of natural numbers” in ZF.
Structural set theory provides a foundation for mathematics which is free of this “superfluous baggage” attendant on theories such as ZF, in which there is lots of information such as whether or not $3\in 17$ (yes, says von Neumann; no, says Zermelo) which is never used in mathematics. In a structural set theory, the elements (such as $3$) of a set (such as $\mathbb{N}$) have no identity apart from their existence as elements of that set, and whatever structure is given to that set by the functions and relations placed upon it. That is, sets (together with other attendant concepts such as elements, functions, and relations) are the “raw material” from which mathematical structures are built. By contrast, theories such as ZF may be called material set theories or membership-based set theories.
Thus, somewhat paradoxically, it turns out that one of the primary attributes of a structural set theory is that the elements of a set have no “internal” structure; they are only given structure by means of functions and relations. In particular, they are not themselves sets, and by default cannot be elements of any other set (not in the sense that it is false that they are, but in the sense that it is meaningless to ask whether they are), so that elements of different sets cannot be compared (unless and until extra structure is imposed). Structural set theory thus looks very much like type theory. We contrast it with material set theories such as ZF, in which the elements of sets can have internal structure, and are often (perhaps always) themselves sets.
It is hard to say precisely what makes a set theory “structural”, but one attempt is the notion of a structurally presented set theory.
Among category theorists, it’s popular to state the axioms of a structural set theory by specifying elementary properties of the category of sets. For this reason structural set theory is often called categorial set theory.
The original, and most commonly cited, categorially presented structural set theory is Bill Lawvere’s ETCS. It is weaker than ZFC and must be supplemented with an axiom of collection to handle some esoteric parts of modern mathematics, although it suffices for most everyday uses. McLarty’s paper argues that ETCS resolves the issues originally raised by Benacerraf.
Another structural set theory, which is stronger than ETCS (since it includes the axiom of collection by default) and also less closely tied to category theory, is SEAR.
Set theory set up in extensional intuitionistic type theory via setoids is structural.
Local set theory avoids the use of any global universe but instead is formulated in a many-sorted language that has various forms of sorts including, for each sort a power-sort; see Bell and Aczel.
Set theory set up via h-sets in homotopy type theory is structural (Rijke-Spitters 13).
Egbert Rijke, Bas Spitters, Sets in homotopy type theory (arXiv:1305.3835)
John Bell, Notes on toposes and local set theories PDF
Peter Aczel, Local Constructive Set Theory and Inductive Definitions, PDF