nLab constructive set theory

Context

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

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.

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

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.

References

See also

Last revised on November 27, 2022 at 23:39:32. See the history of this page for a list of all contributions to it.