Alternative set theories

This is a (soft!) question for students of set theory and their teachers.

OK: ZFC is the canonical set theory we all know and love. But what other, alternative set theories, should a serious student encounter (at least to the extent of knowing that the theory exists, and about why it is thought interesting)?

Suggestions might be SP (Scott-Potter), NBG, NF, ZFA, IST, ETCS (for a few sentences of explanation, see

But what would be on your list of alternative set theories would be it good for advanced students to hear about, if only briefly?

Solutions Collecting From Web of "Alternative set theories"

Peter, there is a nice paper on precisely this topic. It is not quite exhaustive, but it provides an extensive bibliography and a good overview:

M. Randall Holmes, Thomas Forster and Thierry Libert. Alternative Set Theories. In Handbook of the History of Logic, vol. 6, “Sets and Extensions in the Twentieth Century”, 2012, Elsevier/North-Holland, Dov Gabbay, Akihiro Kanamori, and John Woods, eds., pp. 559-632.

For some reason, the volume does not appear on MathSciNet, so I’ll say a few words about the contents of the paper.

The paper begins by discussing (Section 2) Simple Type Theory, Mac Lane’s and Zermelo’s, not because they are alternative theories, but because they are needed to understand some of them (such as New Foundations and its variants), though the authors mention that “Zermelo set theory or variants of Zermelo set theory have been pressed into service themselves as alternative set theories, presumably by workers nervous about the high consistency strength of $\mathsf{ZFC}$.”

Section 3 covers theories with classes: First Von Neumann-Gödel-Bernays and Kelley-Morse set theory, then Ackermann set theory (where non-set classes can belong to other classes, this theory is equiconsistent with $\mathsf{ZF}$), and then a weak system that they call “Pocket set theory”, an expansion due to Holmes of a suggestion by Rudy Rucker.

Section 4 covers theories with atoms and with anti-foundation axioms. They first discuss $\mathsf{ZFA}$, then Aczel’s anti-foundation axiom, and Boffa’s axiom (in this system, there is a proper class of $x$ with $x=\{x\}$, while in Aczel’s system there is only one).

They continue in section 5 with New Foundations and related systems (such as the much better understood $\mathsf{NFU}$, where urelements are allowed). Naturally, this section occupies the main bulk of the paper.

Section 6 discussed Positive set theory and its fragments and variants, typically denoted $\mathsf{PST}$, perhaps with sub- and superscripts (an exception to this notation is the theory $\mathsf{GPK}^+_\infty$, mutually interpretable with an extension of Kelley-Morse by large cardinals). This leads to Topological set theory.

Since the systems in section 6 allow talk of super- or hyperuniveses, section 7 discusses systems motivated by non-standard analysis, such as Nelson’s Internal set theory, or Vopěnka’s.

Section 8 concludes the list and covers “curiosities”: The double extension set theory of Andrzej Kisielewicz (that “has the property which is usually ascribed to New Foundations (we believe not entirely fairly) of being motivated by a syntactical trick without any semantic motivation”), and Zermelo’s set theory extended by an axiom asserting that there is an elementary $j:V\to V$, which turns out to be significantly high in terms of consistency strength

Let me add that the theory $\mathsf{ZF}$ augmented by such an axiom has also been studied, even fairly recently, but I would not classify it by any means as alternative. In general, extensions of $\mathsf{ZF}$ via large cardinals, forcing, or inner-model theoretic considerations are just part of the standard set theoretic landscape.

Something that the paper definitely does not cover is systems motivated by algebraic geometry, topos theoretic, or categorical considerations, such as Grothendieck universes. On the topic of categorical set theory, and Lawvere’s Elementary Theory of the Category of Sets, there is a recent paper that has gathered some attention,

Tom Leinster. Rethinking set theory. ArXiv:1212.6543.

Finally, there is also Bourbaki’s set theory, about which Mathias has written a few critiques. You may enjoy the discussion at the nForum.

There is the structural set theory SEAR (and variants) by Mike Shulman.

SEAR takes as basic the notion of sets, elements and relations, and has as logical grounding dependent type theory, in that elements are typed by the set they belong to (unlike ZFC, elements are not themselves sets, and cannot belong to more than one set), and relations are typed by their domain and codomain. The axioms let you construct a category of sets with nice properties very quickly (i.e. a topos) and in the end you get something equiconsistent with ZF. There is an extension SEAR-C including the axiom of choice; this is equiconsistent with ZFC.

If anyone is counting, SEAR-C has 7 axioms, two of which are schema. If I was pressed, at the moment I’d nominate SEAR(-C) for my favourite foundational system.

(Aside: People should definitely learn the not-quite formalised contrast between material and structural set theories: the former is basically anything that treats elements as supreme, having independent existence and all there is, the latter is more isomorphism invariant and elements don’t have independent existence (this is my own spin on it – there is no watertight definition). Note that ‘categorical’ set theory is subsumed by structural set theory, as SEAR is not given by axiomatising a category of sets, it just heads that way as it was invented and developed by category theorists)

Kripke-Platek set theory is a well-explored axiomatisation of a weakened first-order set theory that gives it pleasing correlations with the language of second-order arithmetic (itself a first-order theory).

This is probably the most useful field of non-standard set theory to know if you are interested in second-order comprehension axioms, recursive model theory, or reverse mathematics.

I would suggest that some constructive alternatives to ZF should be on the list.

Martin-Löf Type Theory is not a set theory as such, but I think could still be included.

IZF and CZF are subtheories of ZF with intuitionistic logic instead of classical (no excluded middle). They can both expand to ZF when excluded middle is added as an axiom, and yet can also be extended with several non-classical axioms including:

  • All functions $\mathbb{R} \rightarrow \mathbb{R}$ are continuous.
  • Church’s Thesis: all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable
  • Uniformity principle: for every formula $\phi$, $(\forall x)(\exists n \in \omega)\phi(x, n) \rightarrow (\exists n \in \omega)(\forall x)\phi(x, n)$

I presented in my web site an expression of set theory that seems new. My purpose in designing it, was to give a clean and efficient way to build mathematics from scratch for the interest of clever undergraduate students, providing a direct path to higher mathematical tools and meta-mathematical considerations.
This is not only a different formalization of set theory but a way to introduce mathematics combining this set theory with model theory.
To sum up the main differences of this set theory from ZF:

The basic kinds of objects are elements, sets and functions. Each element is either a set or a function or none (pure). More kinds of objects can either be seen as additional kinds or constructed from the previous ones : operations, relations, tuples.
Many symbols are admitted beyond the mere ∈ of ZF, most of which are not new but an official recognition of widely used mathematical notations, here taken as (more or less) primary. Some are in neither of both standard kinds of structure symbols of first-order logic (operators and predicates) but are a different kind of symbols: the binders, that bind a variable on a set. Apart from including bounded quantifiers as particular cases, examples include the function definer (E∋x↦…); the set-builders {x∈E|…} and {f(x)|x∈E}; symbols of union and product of a family of sets defined by a term. Also I express and justify a principle giving several axioms of set existence as particular cases.
Classes are defined not as objects of this set theory but as meta-objects.