26
$\begingroup$

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)?
Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ One possible "suitable sense" for your final bullet point would be to consider the theory of a bounded geometric morphism between elementary toposes, i.e. a "Grothendieck topos over an arbitrary base topos". $\endgroup$
    – Mike Shulman
    Commented May 30, 2017 at 14:50

2 Answers 2

Reset to default
21
$\begingroup$

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

  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, AMC, SVC, and SCSA, 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. 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, 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").

Improve this answer
$\endgroup$
3
  • $\begingroup$ What does it mean for the axiom of choice to fail in at most a small way? (I don't quite understand your parenthetical.) $\endgroup$
    – Noah Schweber
    Commented May 28, 2017 at 21:47
  • $\begingroup$ @NoahSchweber I added some links. $\endgroup$
    – Mike Shulman
    Commented May 28, 2017 at 21:52
  • $\begingroup$ For precision, because it is vague from your answer which ones are known: WISC is true in a Grothendieck topos if it is true in $\mathbf{Set}$. More generally, WISC passes up a bounded geometric morphism, and is even preserved by realisability toposes (I believe these observations are due to Benno van den Berg). $\endgroup$
    – David Roberts ♦
    Commented Jun 12, 2020 at 5:53
7
$\begingroup$

Regarding the bullet point list of questions at the end, I believe that every true $\Pi^0_1$-sentence holds in the internal logic of any Grothendieck topos, so in that case $T_{\mathbf{GrTop}}$ is definitely not recursively axiomatizable.

If I understand correctly what you mean by "its contents depend on set-theoretic issues," this is already answered by some of the axioms listed in Mike Shulman's answer. In order to show WISC we need to assume the axiom of choice in the background set theory, and if we only work over $\mathbf{ZF}$ then e.g. $\mathbf{Set}$ is a Grothendieck topos where we can't prove that WISC holds.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks, especially for the observation about $\Pi^0_1$ sentences. Do you have a source for that claim? I think I agree after playing around with it, but I'm not super confident in my work. $\endgroup$
    – user71137
    Commented May 30, 2017 at 15:06
  • $\begingroup$ I don't know a reference for it, but after thinking some more, I think it should be fairly straightforward to prove. In Grothendieck toposes the n.n.o. is just the coproduct of $\mathbb{N}$ copies of $1$ with "standard" zero and successor. So if $\forall n\,\phi(n)$ is a true $\Pi^0_1$, it suffices to show for every $n$, $\phi(\bar{n})$ holds (with $\bar{n}$ the $n$th successor of zero). But this holds in general when $\phi(\bar{n})$ is true and primitive recursive. $\endgroup$
    – aws
    Commented May 30, 2017 at 18:19

You must log in to answer this question.