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”.)

  • 1
    $\begingroup$ 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 $\endgroup$ Jun 9, 2022 at 18:15
  • 1
    $\begingroup$ Footnote 2 made me laugh. What is the source of this convention?? $\endgroup$ Jun 9, 2022 at 19:58
  • 1
    $\begingroup$ @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 “τόπος”. $\endgroup$
    – Gro-Tsen
    Jun 9, 2022 at 20:45
  • 1
    $\begingroup$ @Gro-Tsen Actually I think even the joke compromise is conventionally the other way around: "Grothendieck topoi" but "elementary toposes". $\endgroup$
    – Zhen Lin
    Jun 10, 2022 at 11:33
  • 1
    $\begingroup$ 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!) $\endgroup$
    – Zhen Lin
    Jun 10, 2022 at 11:39

1 Answer 1


Great question!

One example is Zorn's lemma. Assuming ZL holds in the metatheory, ZL also holds in toposes of sheaves over locales, so in particular in toposes of sheaves over topological spaces. However ZL does not hold in all Grothendieck toposes.

The preservation is D4.5.14 in the Elephant. (There the assumption on the metatheory is that AC holds, but actually ZL is enough. AC is equivalent to LEM+ZL; without LEM, ZL is strictly weaker than AC.)

  • 3
    $\begingroup$ 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)$. $\endgroup$
    – Gro-Tsen
    Nov 26, 2022 at 8:32
  • 1
    $\begingroup$ What's an example of a Grothendieck topos where Zorn's lemma doesn't hold? $\endgroup$
    – Tim Campion
    Nov 27, 2022 at 15:51
  • 1
    $\begingroup$ @TimCampion The topos of $G$-sets for a group $G$ has LEM but not AC, hence also no Zorn's lemma. $\endgroup$ Nov 27, 2022 at 19:41
  • $\begingroup$ 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). $\endgroup$ Nov 27, 2022 at 19:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.