# Examples of statements that are valid in every spatial topos

I am looking for statements¹ that, when interpreted in the internal language of a topos, are valid in all spatial toposes (i.e., the topos of sheaves of any topological space) that are not valid in all Grothendieck toposes. Is there somewhere I could find various examples of such things, to get a feel of what they look like and how they are proved?

Essentially the only example I know is: “the unit interval $$[0,1]$$ is compact” or its variation, “Cantor space $$2^{\mathbb{N}}$$ is compact”: these statements hold in any spatial topos but not in any Grothendieck topos. For proofs of these fact, see theorem 3.2 and §4, as well as the postscript, in: Fourman & Hyland, “Sheaf models for analysis”, p. 280–301 in Fourman, Mulvey & Scott (eds.), Applications of Sheaves (Durham 1977) (Springer LNM 753, 1979).

While I'm at it, I'm also interested in the threefold separation:

• Examples of statements valid in all spatial toposes that are not valid in all localic toposes.

• Examples of statements valid in all localic toposes that are not valid in all Grothendieck toposes.

• Examples of statements valid in all Grothendieck toposes that are not valid in all elementary topoi² with natural numbers object.

— provided these do exist, which I'm not at all sure of (except for the above-mentioned examples for the first point).

1. Let's say, to be more precise: statements in higher-order logic whose types are constructed by finite applications of finite products, finite coproducts and internal hom (function types) over the basic types $$0$$, $$1$$, $$\Omega$$ (type of truth values) and $$N$$ (type of natural numbers).

2. (Here following the convention that the plural of “Grothendieck topos” is “Grothendieck toposes” but that of “elementary topos” is “elementary topoi”.)

• I'm not sure but I think the fact that any Grothendieck topos admits a (geometric) surjection from a localic topos might be relevant to the second separation Jun 9, 2022 at 18:15
• Footnote 2 made me laugh. What is the source of this convention?? Jun 9, 2022 at 19:58
• @AlexKruckman: I admit I don't remember where I got this, and it's a bit of a joke compromise, but the logic is that it's not the same word: Grothendieck forged “un topos” as a companion to “une topologie” (and he and his students used “des topos” as plural), whereas Lawvere thought of the Greek word “τόπος”. Jun 9, 2022 at 20:45
• @Gro-Tsen Actually I think even the joke compromise is conventionally the other way around: "Grothendieck topoi" but "elementary toposes". Jun 10, 2022 at 11:33
• Anyway, back to your original question: how about theories in geometric logic? There are many examples of propositional theories that have no models in any spatial topos but do have models in some localic toposes. (Every locale without points gives rise to such a thing, tautologically!) Jun 10, 2022 at 11:39

• Thanks! For completeness of MO, Zorn's lemma is stated as follows for a poset $P$: “If every part of $P$ that is linearly ordered has an upper bound (in $P$) then $P$ has a maximal element”, where a poset is defined by a lax order $≤$ that is reflexive, antisymmetric and transitive, “linearly ordered” means $∀x.∀y.(x≤y∨y≤x)$, and a “maximal” element is an $m$ such that $∀z.(m≤z⇒m=z)$. Nov 26, 2022 at 8:32
• @TimCampion The topos of $G$-sets for a group $G$ has LEM but not AC, hence also no Zorn's lemma. Nov 27, 2022 at 19:41
• Note also that $G$-sets have IC, and, accordingly, I believe, for a $G$-poset $P$ satisfying the internal Zorn condition (that is, the projection from the object of pairs $(\text{chain of$P$}, \text{its upper bound})$ to the object of chains of $P$ is epi), $\max(P)$ is as inhabited as $P$ (but may fail to have any global elements, that is, $G$-fixed points). Nov 27, 2022 at 19:45