Weshowhowto interpretthelanguage offirst-orderset theoryin an elementary toposendowedwith,asextrastructure,adirectedstructuralsystemofinclusions(dssi). Asour mainresult,weobtainacompleteaxiomatizationoftheintuitionisticsettheoryvalidatedbyall suchinterpretations. Sinceeveryelementarytoposisequivalenttoonecarryingadssi,wethus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo-Fraenkel set theory (IZF). §1. Introduction. Thenotionofelementarytoposabstractsfromthestruc- ture of the category of sets. The abstraction is su!cientl y general that elementary toposes encompass a rich collection of other very di"er ent cat- egories, including categories that have arisen in fields as diverse as alge- braic geometry, algebraic topology, mathematical logic, and combinatorics. Nonetheless, elementary toposes retain many of the essential features of the category of sets. In particular, elementary toposes possess an internal logic, which is a form of higher-order type theory, see e.g., (11, 13, 9). This logic allows one to reason with objects of the topos as if they were abstract sets in the sense of (12); that is, as if they were unstructured collections of elements. Although the reasoning supported in this way is both powerful and natural, it di" ers in several respects from the set-theoretic reasoning available in the familiar first-order set theories, such as Zermelo-Fraenkel set theory (ZF). A first main di" erence between the internal logic and ZF is: 1. Except in the special case of boolean toposes, the underlying internal logic of a topos is intuitionistic rather than classical. Many toposes of mathematical interest are not boolean. Thus the use of intuitionistic logic is unavoidable. Moreover, as fields such as synthetic dif- ferential geometry and synthetic domain theory demonstrate, the non-validity of classical logic has mathematical applications. In these areas, intuitionis- tic logic o" ers the opportunity of working consistently with convenient but
['Steven Awodey', 'Carsten Butz', 'Alexander Simpson', 'Thomas Streicher']
Relating first-order set theories and elementary toposes