Constructive toposes with countable sums as models of constructive set theory (Q448336): Difference between revisions
From MaRDI portal
Latest revision as of 15:19, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Constructive toposes with countable sums as models of constructive set theory |
scientific article |
Statements
Constructive toposes with countable sums as models of constructive set theory (English)
0 references
6 September 2012
0 references
The authors define a constructive topos to be a locally Cartesian closed pretopos. Using ideas derived from Joyal and Moerdijk's algebraic set theory, they show that any constructive topos with countable coproducts is a model of of a certain system of constructive predicative set theory CZF. They point out that, since there are numerous natural examples of constructive toposes with countable coproducts which are neither complete nor elementary toposes -- and so in which impredicative set theories such as ZF and IZF cannot be interpreted -- their results provide a purely mathematical reason for considering predicative set theories, one wholly independent of the constructivst rejection, on philosophical grounds, of impredicative and non-constructive principles.
0 references
constructive set theory
0 references
categorical logic
0 references
sheaves
0 references
constructive topos
0 references
CZF
0 references