basic constructions:
strong axioms
The commonly accepted standard foundation of mathematics today is a material set theory, $ZFC$ or Zermelo–Fraenkel set theory with the axiom of choice.
The first version was developed by Ernst Zermelo in 1908; in 1922, Abraham Fraenkel and Thoralf Skolem? independently proposed a precise first-order version with the axiom of replacement; von Neumann added the axiom of foundation in 1925. All of these versions included the axiom of choice, but this was considered controversial for some time; one has merely $ZF$ if it is taken out.
$ZFC$ is similar to the class theories NBG (due to John von Neumann, Paul Bernays?, and Kurt Gödel) and $MK$ (due to Anthony Morse? and John Kelley, see Morse-Kelley set theory). The former is a conservative, finitely axiomatisable extension of $ZFC$, while the latter is stronger and cannot be finitely axiomatised (without introducing meta-classes or something).
Contemporary set theorists often accept additional large cardinal axioms, which can greatly increase the strength of $ZFC$, far beyond even $MK$. Other additional axioms which are sometimes added are the axiom of determinacy? (or various weaker versions of it) or the axiom of constructibility?. There are also weaker variants of $ZFC$, especially for constructive and predicative mathematics. Then there are alternatives on a different basis, notably $NFU$ (a very impredicative material set theory) and ETCS (a structural set theory).
(The source for this history, especially the dates, is mostly the English Wikipedia.)
$ZFC$ is a material set theory, based on a global binary membership predicate $\in$. Everything in standard $ZFC$ is a pure set, which we will call simply a set; but there are also variations with urelements and classes. Urelements may be distinguished from sets and classes since they have no elements (although the empty set also has no elements); sets are usually those classes that are themselves elements (members) of sets. Urelements are also called atoms, and $ZF$ with atoms included is sometimes called ZFA or $ZFU$.
Extensionality: If two sets have the same members, then they are equal and themselves members of the same sets. See axiom of extensionality for variations, such as whether this is taken as a definition or an axiomatisation of equality of sets, and how the condition might be strengthened if (10) is left out.
Null Set: There is an empty set: a set $\empty$ with no elements. By (1), it follows that this set is unique; by even the weakest version of (5), it is enough to state the existence of some set. (Analogous remarks apply to most of the other axioms.)
Pairing: If $a$ and $b$ are sets, then there is a set $\{a,b\}$, the unordered pairing of $a$ and $b$, whose elements are precisely those sets equal to $A$ or $B$. Between them, (2) and (3) form a nullary/binary pair; the unary version follows from (3), since $\{a\} = \{a,a\}$ by (1).
Union: If $\mathcal{C}$ is a set, then there is a set $\bigcup \mathcal{C}$, the union of $\mathcal{C}$, whose elements are precisely the elements of the elements of $\mathcal{C}$. It is normal to write $A \cup B$ for $\bigcup \{A,B\}$, etc. Besides its own power, this gives ternary and higher versions of (3), with $\{a,b,c\} = \{a\} \cup \{b,c\}$, etc.
Separation/Specification/Comprehension: Given any predicate $\phi[x]$ in the language of set theory with the chosen free variable shown, if $U$ is a set, then there is a set $\{x \in U \;|\; \phi[x]\}$, the subset of $U$ given by $\phi$, whose elements are precisely those elements $x$ of $U$ such that $\phi[x]$ holds. There are many variations, from Bounded Separation to Full Comprehension, which we should probably describe at axiom of separation. This is an axiom scheme, but it can be made a single axiom in $NBG$ (but not completely in $MK$). Note that (5) follows from (4) and (6) using classical logic, so it is often left out, except in weak or intuitionistic versions.
Replacement/Collection: Given a predicate $\psi[x,Y]$ with the chosen free variables shown, if $U$ is a set and if for every $x$ in $U$ there is a unique $Y$ such that $\psi[x,Y]$ holds, then there is set $\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U\}$, the image of $U$ under $\psi$, whose elements are precisely those sets $Y$ such that there is an element $x$ of $U$ such that $\psi[x,Y]$ holds; if $\Psi[x]$ is a defined term, then we write $\{\Psi[x] \;|\; x \in U\}$ for $\{\iota\,Y.\; Y = \Psi[x] \;|\; x \in U\}$. Again there are many variations, from Weak Replacement to Strong Collection, which we should probably describe at axiom of replacement. This can be made into a single axiom in both $NBG$ and $MK$. One could combine this with (5) to produce $\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U \;|\; \phi[x]\}$, but nobody seems to do this.
Power Sets: If $U$ is a set, then there is a set $\mathcal{P}U$, the power set of $U$, whose elements are precisely the subsets of $U$, that is the sets $A$ whose elements are all elements of $U$. When using intuitionistic logic, it is possible to accept only a weak version of this, such as Subset Collection or (even weaker) Exponentiation.
Infinity: There is a set $\omega$ of finite ordinals as pure sets. Normally one states that $\empty \in \omega$ and $a \cup \{a\} \in \omega$ whenever $a \in \omega$, although variations are possible. Using any but the weakest version of (6), it is enough to state that there is a set satisfying Peano's axioms of natural numbers, or even any Dedekind-infinite set. It seems to be uncommon to incorporate (2) into (8), but in principle (8) implies (2).
Choice: If $\mathcal{C}$ is a set, each of whose elements has an element, then there is a set with exactly one element from each element of $\mathcal{C}$. Note that this set is not unique, nor can we construct a canonical version which is, so we do not give it any name or notation. This version is the simplest to state in the language of $ZFC$; see axiom of choice for further discussion and weak versions. It is possible to incorporate (9) into (5) or (6), but this seems to be rare.
Foundation/Regularity/Induction: Given a formula $\phi$ with a chosen free variable $X$, if $\phi$ holds whenever $\phi[a/X]$ holds for every $a \in X$, then $\phi$ holds absolutely. For variations (including the axiom of anti-foundation), see axiom of foundation. This scheme can be made into a single axiom even in $ZFC$ itself (although not in versions with intuitionistic logic; in that case it can be made a single axiom only in a class theory).
Zermelo's original version consists of axioms (1–5) and (7–9), in a somewhat imprecise form (which affects the interpretation of 5) of higher-order classical logic.
The modern $ZF$ consists of (1–8) and (10), using first-order classical logic, the strongest form of (6) (that is, Strong Collection, although the standard Replacement is sufficient with classical logic), and the strongest form of (5) possible using only sets and not classes (Full Separation). Since Full Separation follows from Replacement with classical logic, it is often omitted from the list of axioms.
$ZFC$ adds (9) and is thus the strongest version without classes or additional axioms. The version originally formulated by Fraenkel and Skolem did not include (10), although the three founders all eventually accepted it.
It is common to take Zermelo set theory ($\mathrm{Z}$) to be $ZF$ without (6), although Zermelo never accepted the first-order formulation; note that the weakest form (Weak Replacement) of (6) follows from (7) and (5), so it holds even in $\mathrm{Z}$.
Another variant is bounded Zermelo set theory ($BZ$), which is like $\mathrm{Z}$ but with only Bounded Separation; this is of interest to category theorists because $BZC$ is equivalent to ETCS.
The most well-known foundations for constructive mathematics through material set theory are Peter Aczel's constructive Zermelo–Fraenkel set theory ($CZF$) and John Myhill?'s intuitionistic Zermelo–Fraenkel set theory ($IZF$).
$CZF$ uses axioms (1–8) and (10), usually weak forms, in intuitionistic logic; specifically, it uses Bounded Separation for (5), Strong Collection for (6), and an intermediate (Subset Collection) form of (7). $IZF$ is simliar, but it uses Full Separation for (5) and the full strength of (7); Myhill's original version uses only Replacement for (6), but Collection (equivalent to Strong Collection using Full Separation) is standard now.
Note that adding (9) to $IZF$ implies excluded middle and so makes $ZFC$. However, some authors like to include a weak form of (9), such as dependent choice or COSHEP.
Mike Shulman's unfinished survey of material and structural set theories takes $CPZ^{\circlearrowleft-}$ as the most basic form; it consists of (1–4) and the weakest versions (Bounded Separation and Weak Replacement) of (5&6) in intuitionistic logic. Adding (10) gives $CPZ^{-}$, adding (8) gives $CPZ^{\circlearrowleft}$, and adding both gives $CPZ$, constructive pre-Zermelo set theory. Shulman gives systematic notation for other versions, which includes those (constructive and classical) listed above.
Myhill has another version, constructive set theory ($CST$); this consists of (1–4), Bounded Separation for (5), Replacement for (6), the weakest (Exponentiation) form of (7), (8), and a weak version (Dependent Choice) of (9). It also uses a variation of the language, with urelements for natural numbers; note that the existence of $\omega$ still follows using (6). This classifies $CST$ as $\mathrm{C}{\Pi}ZF^{\circlearrowleft} + DC$ in Shulman's system if one ignores the use of urelements and strengthens Replacement to Strong Collection.
Morse--Kelley class theory ($MK$) features both sets and proper classes. This allows it to strengthen (5) to Full Comprehension, since $\phi$ can include quantification over classes; the same holds in (6) and (10), although this does not add any additional strength.
Von Neumann–Bernays–Gödel class theory ($NBG$) uses the same language as $MK$, but it still uses only Full Separation for (5). This makes it conservative over $ZFC$ and also allows for a finite axiomatisation; we replace the formulas in (5) and (6) with classes, and add some special cases of (5) for subclasses, one for each logical connective. (It is provable that plain $ZF$, if consistent, cannot be finitely axiomatized in its own first-order language; $NBG$ escapes this conclusion by extending the language with the notion of classes.)
One can also rework all of the weak versions of set theory above into a class theory like $NBG$, which is conservative over the original set theory. One can also use a class theory like $MK$, although this destroys any attempt to use a weak version of (5).
One often adds axioms for large cardinals to $ZFC$. Even (8) can be seen as a large cardinal axiom, stating that $\aleph_0$ exists. These additional axioms are most commonly studied in the context of a material set theory, but they work just as well in a structural set theory.
Note that adding an inaccessible cardinal (commonly considered the smallest sort of large cardinal) to $ZFC$ is already stronger than $MK$: given an inaccessible cardinal $\kappa$, one can interpret the sets and classes in $MK$ as the sets in $V_\kappa$ and $V_{\kappa+1}$, respectively. Of course, one can add a large cardinal to $MK$ to get something even stronger.
It is often convenient to assume that one always has more large cardinals when necessary. You cannot say this in an absolute sense, but you can adopt the axiom that every set belongs to some Grothendieck universe. Adding this axiom to $ZFC$ makes Tarski–Grothendieck set theory ($TG$). This is not the last word, however; you can make it stronger by adding classes in the style of $MK$, or even adding a cardinal which is inaccessible from $TG$. In fact, we have barely begun the large cardinals known to modern set theory!
The axiom of constructibility?, usually notated “$V = L$”, is a very strong axiom that can be added to $ZF$; it asserts that all sets belong to the constructible universe $L$, which can be “constructed” in a definable way through a transfinite procedure. This notion of “constructible” should not be confused with constructive mathematics; for instance, $V = L$ implies the axiom of choice and thus also excluded middle even with intuitionistic logic. $V = L$ also implies the generalized continuum hypothesis ($GCH$), which is how Gödel originally proved that $GCH$ was consistent with $ZFC$. However, it is incompatible with the sufficiently large cardinals: the existence of a measurable cardinal implies that $V \neq L$. Most contemporary set theorists do not regard $V = L$ as potentially “true.”
The axiom of determinacy? ($AD$) is another axiom that can be added to $ZF$; it asserts that a certain class of infinite game?s is determined (one player or the other has a winning strategy). $AD$ is inconsistent with the full axiom of choice, although it is consistent with dependent choice. A weaker form of $AD$ called “projective determinacy” is consistent with $AC$ and is equiconsistent with certain large cardinal assertions.
The $GCH$ itself, or its negation, could also be regarded as an additional axiom that can be added to $ZF$. Many set theorists would prefer to find a more “natural” axiom, such as a large cardinal axiom, which implies either $GCH$ or its negation. The equiconsistency of projective determinacy with a large cardinal assertion can be regarded as a step in this direction.
The structural set theory ETCS is equivalent to $BZC$ in that the category of sets in that theory satisfies $ETCS$ while the well-founded pure sets in $ETCS$ satisfy $BZC$. This uses (1–4), Bounded Separation for (5), and (7–10), with Weak Replacement following from (5) and (7).
Shulman's SEARC is equivalent to $ZFC$ in the same way. $SEAR$, which lacks the axiom of choice, is equivalent to $ZF^{\circlearrowleft}$, which is $ZF$ without (10), in a weaker sense.