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)?



Precise relationship between elementary and Grothendieck toposes?
There are known statements that are true in any Grothendieck topos, but not in every elementary topos with NNO. For instance:


1. Freyd's theorem that a complete small category is a preorder is not constructively provable and can fail in elementary toposes with NNO, such as the effective topos; but can be shown to hold in any Grothendieck topos by an "external" argument (see [this question](https://mathoverflow.net/questions/43433/small-complete-categories-in-a-grothendieck-topos)).
2. Axioms that assert things like "the axiom of choice fails in at most a small (i.e. set-indexed rather than proper-class-indexed) way" often tend to be true in Grothendieck toposes (at least when defined over ZFC), but can fail in elementary toposes that correspond to things like "permutation models over proper classes". Some "small choice" axioms are [WISC](https://ncatlab.org/nlab/show/WISC), [AMC](https://ncatlab.org/nlab/show/axiom+of+multiple+choice), [SVC](https://ncatlab.org/nlab/show/small+violations+of+choice), and [SCSA](https://ncatlab.org/nlab/show/small+cardinality+selection+axiom), but I don't know offhand the situation for all of these regarding their truth in Grothendieck topoi.
3. An axiom scheme that holds in all Grothendieck toposes, but not all elementary toposes with NNO, is "autology" (representability of large quantification in the stack semantics) as defined in [this paper](https://arxiv.org/abs/1004.3802). This is a sort of "replacement axiom" for topos theory, and fails in models like $V\_{\omega\cdot 2}$.
4. A Grothendieck topos (defined over ZFC) also has all [higher inductive types](https://arxiv.org/abs/1705.07088), including in particular localizations at any set of maps, and free algebras for all (even infinitary) algebraic theories. These can also fail in elementary toposes with NNO, such as a model of ZF in which $\omega$ is the only infinite regular cardinal (see Blass's paper "Words, free algebras, and coequalizers").


