Is it known how much of ZFC is actually necessary for the basic, familiar constructions and theorems in sheaf theory, along the lines of section II.1 (and its exercises) in Hartshorne's "Algebraic Geometry" textbook?


I apologize for this strange question. Here is the motivation behind it: I am a mathematician who works automatically and implicitly in ZFC, like most users of this website. Last year some members of the philosophy department at my university showed me some old questions in metaphysics which seemed to me as though they ought to be approachable axiomatically. Indeed they were, and some of the structures studied by the philosophers turn out to be (non-obviously) equivalent to sheaves of sets on a certain topological space. I was able to make some progress on those problems by using some classical, elementary ideas in sheaf theory, particularly the equivalence of sheaves of sets and local homeomorphisms. My colleagues in philosophy are supportive of this, but they suggest that unrestrained use of the ZFC axioms to resolve questions in philosophy may open the door for argument from philosophers who have various kinds of skepticism about set theory, and that it is best to offer the argument in a way that uses only as weak of a fragment of ZFC as possible. 


I spent a while looking over the proofs of the theorems from sheaf theory that I am using, and it appears to me that the proofs all work in ZAC (Zermelo set theory with choice), but perhaps one can go weaker still. The outcome will be better if this kind of work is done by someone that knows more set theory than I do, so I would be happiest if someone else has already figured out how strong a set theory is necessary for elementary sheaf theory. Is this already out there, somewhere, in the literature? I am not even aware of a journal where investigations of this kind would appear, but perhaps people working in some areas of foundations of mathematics have someplace where they figure out such things.


I apologize for my ignorance of foundations of mathematics, and I also apologize again for this very strange question.



How strong a set theory is necessary for practical purposes in sheaf theory?
Colin McLarty has looked into this



> 
> *The large structures of Grothendieck founded on finite order arithmetic*, Review of Symbolic Logic **13** issue 2 (2020) pp. 296--325, doi:[10.1017/S1755020319000340](https://doi.org/10.1017/S1755020319000340), arXiv:[1102.1773](https://arxiv.org/abs/1102.1773).
> 
> 
> 


with abstract (emphasis added):



> 
> The large-structure tools of cohomology including toposes and derived categories stay close to arithmetic in practice, yet published foundations for them go beyond ZFC in logical strength. We reduce the gap by **founding all the theorems of Grothendieck’s SGA, plus derived categories, at the level of Finite-Order Arithmetic, far below ZFC.** This is the weakest possible foundation for the large-structure tools because one elementary topos of sets with infinity is already this strong.
> 
> 
> 


In the arXiv version the abstract claimed all of EGA's theorems as well, but I haven't investigated why this was removed. Certainly it is generally considered that the axiom of Replacement is not needed for 'generic' (i.e. non-logical/set-theory) mathematics, hence for algebraic geometry generally. In particular, it's generally accepted (though one might have to check specific statements that seem very strong) that [ETCS](https://ncatlab.org/nlab/show/ETCS) is sufficient as a foundation, roughly equivalent to, but slightly weaker than, what you call ZAC.


