Constructive toposes with countable sums as models of constructive set theory (Q448336): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 5 users not shown) | |||
Property / author | |||
Property / author: Alex K. Simpson / rank | |||
Property / author | |||
Property / author: Alex K. Simpson / rank | |||
Normal rank | |||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: John L. Bell / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03E70 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F50 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03G30 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 18B25 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6078323 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
constructive set theory | |||
Property / zbMATH Keywords: constructive set theory / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
categorical logic | |||
Property / zbMATH Keywords: categorical logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
sheaves | |||
Property / zbMATH Keywords: sheaves / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
constructive topos | |||
Property / zbMATH Keywords: constructive topos / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
CZF | |||
Property / zbMATH Keywords: CZF / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2012.01.013 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2042711307 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3937387 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3762311 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Relating first-order set theories, toposes and categories of classes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5701016 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4680361 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Aspects of predicative algebraic set theory. I: Exact completion / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Unified Approach to Algebraic Set Theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Aspects of predicative algebraic set theory III: sheaves / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Aspects of predicative algebraic set theory. II: Realizability / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4936141 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4304740 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Sheaf models for set theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Set theoretic foundations for constructive analysis / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3963000 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4783274 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4853985 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4807625 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Impredicativity entails untypedness / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Independence results around constructive ZF / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A characterization of the left exact categories whose exact completions are toposes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Wellfounded trees in categories / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Type theories, toposes and constructive set theory: Predicative aspects of AST / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Constructive set theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Realizability. An introduction to its categorical side / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 16: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