Constructive toposes with countable sums as models of constructive set theory (Q448336): Difference between revisions

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.