Categorical set theory: A characterization of the category of sets

AbstractWe consider Zermelo-Fraenkel set theory ZF and the theory ETS(ZF) of the elementary topos of ZF sets, which is an extension of Lawvere-Tierney's theory of elementary topoi, and prove that the theory ETS(ZF) characterizes the category (topos) of ZF-sets in the following sense. The category (topos) of ZF sets satisfies the axioms of ETS(ZF), and conversely we can define within topos theory ETS(ZF) the model of set-objects in which the ZF axiloms hold, and, furthermore, the model of set-objects in the topos of ZF sets is “equivalent” to set theory ZF and the topos of set-objects in ETS(ZF) is “logical equivalent” to topos theory ETS(ZF). Actually, the corresponding result for a weak set theory Z and the theory ETS(Z) of the elementary topos of Z sets is proved. Adding further axioms (axiom of choice, continuum hypothesis, etc.), various results of the same character are obtained.The construction of the model of set-objects uses a universal mapping property of transitive sets, which enables us to introduce transitive-set-objects in any elementary topos and to prove their basic properties