nLab constructive set theory

Redirected from "CZF".

Context

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

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

On constructive set theory in homotopy type theory:

Last revised on November 6, 2023 at 16:12:19. See the history of this page for a list of all contributions to it.