nLab constructive set theory

Idea

Constructive set theory is set theory in the spirit of constructive mathematics.

Algebraic set theory is a categorical presentation of such set theories.

Some more information can be found at ZFC. Perhaps this should be moved here.

Axiom systems

There are a number of axiom systems:

Impredicative set theories

All of these set theories can be interpreted in a set-level type theory with a type of all propositions.

• The impredicative IZF which includes the power set or power object axiom.
• ISEAR - the allegorical set theory version of IZF.
• IETCSR - the categorical set theory version of IZF.

Weakly predicative set theories

All of these set theories can be interpreted in set-level type theory with no type of all propositions, but with function types and dependent function types

• The variant CZF for predicative mathematics.
• CSEAR - the allegorical set theory version of CZF.
• CETCSR - the categorical set theory version of CZF.

Strongly predicative set theories

All of these set theories can be interpreted in set-level type theory with only dependent function types for families of subsingletons.

• PSEAR

Related concepts

• constructive analysis

• constructive algebraic topology

• taboo

References

• Peter Aczel, Michael Rathjen, Notes on Constructive Set theory, 2001 (pdf, pdf)

See also

• Wikipedia, Constructive set theory

On constructive set theory in homotopy type theory:

• Håkon Robbestad Gylterud, Elisabeth Bonnevier, Non-wellfounded sets in HoTT [arXiv:2001.06696, talk video:YT]