Elementary toposes form an elementary class in that they are axiomatizable by (finitary) first-order sentences in the "language of categories" (consisting of a sort for objects, a sort for morphisms, function symbols for domain and codomain, and a ternary relation symbol on morphisms for composition). Grothendieck toposes do not form an elementary class: Giraud's axioms are inherently infinitary. However, we can form the "elementary theory of Grothendieck toposes" as the theory axiomatized by every (finitary first-order) sentence true in every Grothendieck topos. (Apply your favorite workaround for size issues. If the size issues are important in this context, though, I'd enjoy reading why.)

The elementary theory of Grothendieck toposes (which I'll denote $T_{\operatorname{GrTop}}$) is a proper strengthening of the theory of elementary toposes (which I'll denote $T_{\operatorname{ElTop}}$): it stronger because every Grothendieck topos is an elementary topos, and it is properly stronger because, at a minimum, $T_{\operatorname{GrTop}}$ contains a sentence asserting the existence of a natural number object.

Beyond the existence of a natural number object, I can't think of any other concrete ways in which $T_{\operatorname{GrTop}}$ is stronger than $T_{\operatorname{ElTop}}$ (but I don't really know what to look for). My question is, **what is known about $T_{\operatorname{GrTop}}$**? I'm asking out of general interest, so I'd value any information at all including,

- Can we give explicit axioms for it?
- If not, is it at least known to be recursively axiomatizable?
- If not, might its contents depend on set-theoretic issues?
- If it does depend on set-theoretic issues, do we get interesting results by redefining $T_{\operatorname{GrTop}}$ to be the theory axiomatized by all sentences true in all Grothendieck toposes "in all models of set theory" (in some suitable sense)?