Constructive toposes with countable sums as models of constructive set theory
type: Item
instance of: scholarly article
title: Constructive toposes with countable sums as models of constructive set theory
zbMATH Open document ID: 1275.03145
author: Thomas Streicher
author: Alex Simpson
published in: Annals of Pure and Applied Logic
publication date: 2012-09-06T00:00:00Z
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.
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18B25
zbMATH DE Number: 6078323
zbMATH Keywords: constructive set theory
zbMATH Keywords: categorical logic
zbMATH Keywords: sheaves
zbMATH Keywords: constructive topos
zbMATH Keywords: CZF
MaRDI profile type: Publication
full work available at URL: j.apal.2012.01.013
OpenAlex ID: W2042711307
cites work: Q3937387
cites work: Q3762311
cites work: Relating first-order set theories, toposes and categories of classes
cites work: Q5701016
cites work: Q4680361
cites work: Aspects of predicative algebraic set theory. I: Exact completion
cites work: A Unified Approach to Algebraic Set Theory
cites work: Aspects of predicative algebraic set theory III: sheaves
cites work: Aspects of predicative algebraic set theory. II: Realizability
cites work: Q4936141
cites work: Q4304740
cites work: Sheaf models for set theory
cites work: Set theoretic foundations for constructive analysis
cites work: Q3963000
cites work: Q4783274
cites work: Q4853985
cites work: Q4807625
cites work: Impredicativity entails untypedness
cites work: Independence results around constructive ZF
cites work: A characterization of the left exact categories whose exact completions are toposes
cites work: Wellfounded trees in categories
cites work: Type theories, toposes and constructive set theory: Predicative aspects of AST
cites work: Constructive set theory
cites work: Realizability. An introduction to its categorical side
DOI: 10.1016/J.APAL.2012.01.013
reviewed by: John L. Bell
description: scientific article; zbMATH DE number 6078323