7
$\begingroup$

It's a well-known fact that the theory of a well-pointed topos with a natural numbers object (NNO) has the same consistency strength as MacLane set theory (also known as bounded Zermelo). There are many weaker, more general classes of categories that have been studied, but what is known about their consistency strengths relative to classical theories of sets and second- and first-order arithmetic?

(What I mean by consistency strength here is slightly ambiguous, but for now I am interpreting consistency questions for a category as consistency of the theory of the category as a classical two-sorted structure with sorts for objects and morphisms. In principle this is different from the consistency of local set theories corresponding to toposes, for instance, although I suspect that these different interpretations don't differ that much.)

I'm interested in this kind of issue in general, but I should focus on specifics in an MO question.

Question 1. What is known about the consistency strengths of the following?

  • Toposes with an NNO (but no assumption of well-pointedness).
  • Toposes with a 'Dedekind-infinite object' (i.e., an object with a self-monomorphism that is not an epimorphism) with or without well-pointedness.
  • Toposes in general with or without well-pointedness.

$\mathsf{PA}$ (and fragments of it which are not too weak) interprets a theory of finite sets, which gives a well-pointed topos without an NNO. I think that there is an interpretation of a non-well-pointed topos with an NNO in $\mathsf{RCA}_0$ (some of the constructions in higher reverse math seem like they build such a thing), which would indicate that dropping the well-pointedness condition reduces the consistency strength quite a bit.

I'm also curious about 'toposes without subobject classifiers,' but I'm not sure what good definitions there are of such things. As a very ignorant guess, I'll ask the following precise question.

Question 2. Is anything known about the consistency strength of bi-Cartesian closed categories (possibly with Dedekind-infinite objects and/or well-pointedness)?

I think you can show that a bi-Cartesian closed category interprets Robinson arithmetic (although it's unclear that they actually interpret an arithmetic in which exponentiation is a total function, despite the presence of power objects), so even very weak generalizations of toposes land in the range of first-order theories where consistency statements are meaningful.

Improve this question
$\endgroup$
7
  • $\begingroup$ If you interpret ‘consistency strength of a topos’ as meaning the consistency strength of the axiomatic set theory corresponding to the internal logic of the topos, then Mike Shulman’s paper might interest you; the type of topos corresponding to an internal consistency strength $\geq ZFC$ is called autological. $\endgroup$
    – Alec Rhea
    Commented Apr 27, 2021 at 20:14
  • $\begingroup$ @AlecRhea Thank you very much for the reference. I had wondered about how you would even formalize collection or replacement principles in toposes, but I should say that I am more concerned with going downwards in consistency strength rather than upwards. $\endgroup$
    – James E Hanson
    Commented Apr 27, 2021 at 20:19
  • 2
    $\begingroup$ I'd expect that the theory of a (non-degenerate) well-pointed topos, without NNO, could be interpreted in theories far weaker than PA. My guess would be $I\Delta_0$ plus existence of exponentials. $\endgroup$
    – Andreas Blass
    Commented Apr 27, 2021 at 21:00
  • 1
    $\begingroup$ I think (but don't guarantee) that coequalizers are OK, because exponentiation lets you code finite sequences and also gives you bounds for the codes of one-to-one sequences with terms below a given number. $\endgroup$
    – Andreas Blass
    Commented Apr 27, 2021 at 21:10
  • 1
    $\begingroup$ There is a very nice concept of 'toposes [with NNO but] without subobject classifiers', namely the arithmetic universes pioneered by Joyal and studied by Maietti, Vickers and recently Alexander Oldenziel. While the initial elementary topos with NNO is a souped-up version of Heyting arithmetic, the initial arithmetic universe is a souped-up version of PRA. $\endgroup$
    – Ingo Blechschmidt
    Commented Apr 27, 2021 at 22:20

0

Reset to default

You must log in to answer this question.