NUK - logo
FMF, Mathematical Library, Lj. (MAKLJ)
  • Constructive toposes with countable sums as models of constructive set theory
    Simpson, Alex ; Streicher, Thomas, 1958-
    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, ▫$\mathbf{{CZF}_{Exp}}$▫ (that is, the variant of Aczel's Constructive Zermelo-Fraenkel set theory ▫$\mathbf{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_{\omega_1}$▫ (in an appropriate formulation). It follows that the full Separation schema is always refuted.
    Source: Annals of pure and applied Logic. - ISSN 0168-0072 (Vol. 163, iss. 10, 2012, str. 1419-1436)
    Type of material - article, component part ; adult, serious
    Publish date - 2012
    Language - english
    COBISS.SI-ID - 17091417

    Link(s):

    http://dx.doi.org/10.1016/j.apal.2012.01.013

source: Annals of pure and applied Logic. - ISSN 0168-0072 (Vol. 163, iss. 10, 2012, str. 1419-1436)

loading ...
loading ...
loading ...

Shelf entry