Intuitionistic set theory - Grayson, RJ (1978)
We describe the formal system of higher—order intuitionistic logic with power types and (impredicative) comprehension which provides the basis for our "set theory"; this is adapted from the system of FOURMAN (D.Phil. Thesis, Oxford 1974), and such theories are equivalent to the notion of a topos. We interpret the basic concepts of sets, relations and functions; we consider relations of equality, apartness and order, and develop some of the intuitionistic theory of complete Heyting algebras (cHa's). We give the semantical definitions which make sheaves over a cHa into a model for the formal system. We give a unified description of the Dedekind reals and Baire space as the spaces of models of geometric propositional theories, from which follows the usual characterisation of them as they appear in sheaf models.