Comparing material and structural set theories (Q1715477)

ZFC (Zermelo-Fraenkel set theory with the axiom of choice) and BZC (bounded Zermelo set theory) are \textit{material} set theories in the sense that they are based upon a global membership predicate (the word ``material'' was suggested in [\textit{S. Awodey}, Philos. Math., III. Ser. 4, No. 3, 209--237 (1996; Zbl 0874.00012)]), while ETCS (the theory of a well-pointed topos with a natural number object abiding by the axiom of choice) and its ilk are \textit{structural} set theories which take functions as primitive entities. It is well known [\textit{J. C. Cole}, in: The proceedings of the Bertrand Russell memorial logic conference, Uldum, Denmark, August 4--16, 1971. 351--399 (1973; Zbl 1416.03019); \textit{W. Mitchell}, J. Pure Appl. Algebra 2, 261--274 (1972; Zbl 0245.18001); \textit{W. Mitchell}, J. Pure Appl. Algebra 3, 193--201 (1973; Zbl 0272.18005)] that ETCS is equiconsistent with BZC. The principal objective in this paper is to obtain similar results for stronger and weaker theories in a unified manner. By removing such axioms as choice, classical logic and power set from BZC, one gets intuitionistic and predicative set theories corresponding to more general toposes and pretoposes, while the author proposes category-theoretic properties corresponding to such set-theoretic axioms as separation, replacement and collection. This paper is concerned entirely with (pre)toposes corresponding directly to set theories in the sense that the set-theoretic elements of a set \(X\) are in bijection with its category-theoretic global emements \(1\rightarrow X\), that is to say, the category is well-pointed. By dropping well-pointedness, one can interpret BZC in any Boolean topos with an NNO and choice with recourse to the internal logic. The paper is on the lines of [\textit{F. W. Lawvere}, Proc. Natl. Acad. Sci. USA 52, 1506--1511 (1964; Zbl 0141.00603)]; \textit{F. W. Lawvere}, Repr. Theory Appl. Categ. 2005, No. 11, 1--35 (2005; Zbl 1072.18005); \textit{C. McLarty}, Philos. Math. (3) 12, No. 1, 37--53 (2004; Zbl 1051.18004); \textit{G. Osius}, J. Pure Appl. Algebra 4, 79--119 (1974; Zbl 0282.02027)], but generalizes readily to the intuitionistic case. The author is now preparing a paper extending the usual internal logic that admits unbounded quantifiers [``Stack semantics and unbounded quantifiers in topos theory''].