Switch to: Citations

Add references

You must login to add references.
  1. Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
    Download  
     
    Export citation  
     
    Bookmark   131 citations  
  • (1 other version)Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
    Download  
     
    Export citation  
     
    Bookmark   80 citations  
  • The strength of Mac Lane set theory.A. R. D. Mathias - 2001 - Annals of Pure and Applied Logic 110 (1-3):107-234.
    Saunders Mac Lane has drawn attention many times, particularly in his book Mathematics: Form and Function, to the system of set theory of which the axioms are Extensionality, Null Set, Pairing, Union, Infinity, Power Set, Restricted Separation, Foundation, and Choice, to which system, afforced by the principle, , of Transitive Containment, we shall refer as . His system is naturally related to systems derived from topos-theoretic notions concerning the category of sets, and is, as Mac Lane emphasises, one that is (...)
    Download  
     
    Export citation  
     
    Bookmark   37 citations  
  • Relating First-Order Set Theories and Elementary Toposes.Steve Awodey & Thomas Streicher - 2007 - Bulletin of Symbolic Logic 13 (3):340-358.
    We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions . As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...)
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Relating first-order set theories and elementary toposes.Steve Awodey, Carsten Butz & Alex Simpson - 2007 - Bulletin of Symbolic Logic 13 (3):340-358.
    We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Computational adequacy for recursive types in models of intuitionistic set theory.Alex Simpson - 2004 - Annals of Pure and Applied Logic 130 (1-3):207-275.
    This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations