Constructive toposes with countable sums as models of constructive set theory

Alexander Simpson, Thomas Streicher

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We define a constructive topos to be a locally cartesian closed pretopos. The terminology is supported by the fact that constructive toposes enjoy a relationship with constructive set theory similar to the relationship between elementary toposes and (impredicative) intuitionistic set theory. This paper elaborates upon one aspect of the relationship between constructive toposes and constructive set theory. We show that any constructive topos with countable coproducts provides a model of a standard constructive set theory, CZFExp (that is, the variant of Aczel’s Constructive Zermelo–Fraenkel set theory CZF obtained by weakening Subset Collection to the Exponentiation axiom). The model is constructed as a category of classes, using ideas derived from Joyal and Moerdijk’s programme of algebraic set theory. A curiosity is that our model always validates the axiom V=Vω1 (in an appropriate formulation). It follows that the full Separation schema is always refuted.

Original languageEnglish
Pages (from-to)1419-1436
Number of pages18
JournalAnnals of Pure and Applied Logic
Volume163
Issue number10
Early online date16 Feb 2012
DOIs
Publication statusPublished - 2012

Keywords / Materials (for Non-textual outputs)

  • Constructive set theory
  • Categorical logic
  • Sheaves

Fingerprint

Dive into the research topics of 'Constructive toposes with countable sums as models of constructive set theory'. Together they form a unique fingerprint.

Cite this