Timeline for How much is known about the consistency strength of toposes and topos-like categories?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 28, 2021 at 5:32 | comment | added | David Roberts♦ | Well-pointedness shouldn't really make a difference. Every topos is internally constructively well-pointed, as proved by Mike Shulman. | |
| Apr 27, 2021 at 22:20 | comment | added | Ingo Blechschmidt | 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. | |
| Apr 27, 2021 at 21:10 | comment | added | Andreas Blass | 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. | |
| Apr 27, 2021 at 21:02 | comment | added | James E Hanson | @AndreasBlass I had thought of that, but I was worried about the existence of coequalizers. It's not immediately clear to me that you can form the smallest equivalence relation containing a given relation. | |
| Apr 27, 2021 at 21:00 | comment | added | Andreas Blass | 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. | |
| Apr 27, 2021 at 20:19 | comment | added | James E Hanson | @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. | |
| Apr 27, 2021 at 20:14 | comment | added | Alec Rhea | 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. | |
| Apr 27, 2021 at 19:42 | history | asked | James E Hanson | CC BY-SA 4.0 |