# Properties of the internal language of the category of sheaves

Consider a simple case of set-valued sheaves on some topological space $X$, $\operatorname{Sh}(X)$. All of these are Grothendieck toposes but clearly not all of them are equivalent.

Is there an overview of what properties of $\operatorname{Sh}(X)$ are induced by the properties of $X$? The properties I am interested in are the logical principles that hold in the internal logic. Of course the properties must necessarily be the properties of the locale of opens $\mathcal{O}(X)$.

Sketches of an Elephant has a list of some properties induced by the properties of $\mathcal{O}(X)$, but most of these are about the existence of geometric morphisms, which of course in some cases allow one to define some modalities in the internal language, but I would also like to know if there are some formulas of ordinary higher-order logic that are valid.

For example, suppose $X$ is compact. Is there a useful or interesting logical principle that holds in $\operatorname{Sh}(X)$ but does not hold in sheaves over non-compact spaces? Perhaps some form of choice?

I asked this question on math.stackexchange.com but did not receive an answer so I hope it's OK to ask here.

• You should probably have a look at the work of Olivia Caramello: a large portion is about precisely this. – Zhen Lin Nov 26 '13 at 20:25
• Not sure about "precisely". These ones here are maybe vaguely related: Olivia Caramello, "Site characterizations for geometric invariants of toposes" (arxiv.org/abs/1112.2542) and "Topologies for intermediate logics" (arxiv.org/abs/1205.2547) – Urs Schreiber Nov 27 '13 at 8:57