You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
John Onstead (Oct 07 2025 at 11:29):Doing math from the category theoretic and from the materialist perspective offer two independent ways of defining a mathematical object. In category theory, a mathematical object can be defined internally to any category with sufficient properties to express it, via a structure-preserving functor into that category (IE, a group is a finite product functor from the Lawvere theory into Set). In material mathematics, a mathematical object is instead defined internally to an appropriate theory (like ZFC) by simply "building up" the object inside of that theory (IE, defining a group as a certain kind of set you can build in ZFC).
John Onstead (Oct 07 2025 at 11:30):While these appear to be independent worlds, in some set theories, one can use a "material-structural adjunction" to go from a model of set theory to a category Set of sets. Oftentimes, objects you can define in a consistent way within the model of set theory can then be given as appropriate structure-preserving functors into that corresponding Set category. However, set theory isn't the only way of doing math in a materialist way. For instance, in reverse mathematics, the idea of a second order arithmetic is used, and instead of ZF or ZFC, we instead consider theories such as RCA, WKL, ACA, ATR, and so on.
John Onstead (Oct 07 2025 at 11:31):So here's my question. Is there any way to "translate" doing mathematics internally to a model of second order arithmetic into doing mathematics internally to some corresponding category, as we can when moving between set theory models and categories of sets? It seems more difficult- for instance, there doesn't seem to be an obvious way to code the abstract idea of a "group" inside of RCA, and yet if there is some category corresponding to a model of RCA, one should be able to define a group object internally to it. Might there be some sort of "material-structural" adjunction for second order arithmetic just like with set theory, or does this not exist?
John Baez (Oct 07 2025 at 11:43):This is a nice question! I think if I were going to tackle it, I'd try to find some 2-category of categories - i.e. some 'doctrine' - whose internal logic can somehow be seen as RCA, or more precisely .
John Baez (Oct 07 2025 at 11:46):I don't know of work along these lines, but I hope someone tries (or even better, has done it).
The closest thing I know concerns [[primitive recursive functions]], which are less general than recursive functions. These are related to parametrized natural numbers objects and arithmetic pretoposes:
The functions which are constructible out of the structure of a category with finite products and such a “parametrized NNO” are precisely the primitive recursive ones. Specifically, the unique structure-preserving functor from the free such category F into Set yields a bijection between and the actual natural numbers, as well as surjections from onto the primitive recursive functions of arity m for each finite m. With cartesian closure, however, this identification no longer holds, since some non-primitive recursive functions (such as the Ackermann function) become definable as well.
In this context an important class is the class of pretoposes with a parametrized NNO - the so called arithmetic pretoposes.
But all this is only vaguely related to your specific question about RCA.
John Onstead (Oct 07 2025 at 18:46):John Baez said:
whose internal logic can somehow be seen as RCA, or more precisely .
...
These are related to parametrized natural numbers objects and arithmetic pretoposes:
That's interesting! The article on arithmetic pretopos did mention finding a syntactic category for PA, so maybe it's as simple as trying to find the syntactic category for RCA.
John Baez (Oct 08 2025 at 09:26):Or as difficult as that.
John Onstead (Oct 09 2025 at 11:22):This also makes me wonder, what it even "means" to be able to define a mathematical object internal to some theory. For instance, one can easily define mathematical objects internal to ZFC (most mathematical objects can be) and to RCA (for instance, I believe there's coding mechanisms that allow even complete separable metric spaces to be definable within that context). However, there are also theories like the theory of groups or the theory of topological spaces that we don't usually consider as theories we can define mathematical objects internally to.
John Onstead (Oct 09 2025 at 11:23):Here's my question about this. Which of the following two possibilities is the correct one: 1. There is a clear cut dividing line between theories in which one can define mathematical objects (like ZFC and RCA) and those in which one cannot (such as groups and topological spaces). If this is the case, then what is the nature of this dividing line? 2. There is a spectrum of theories: the "weaker" the theory, the less mathematical objects you can define internal to it, and the "stronger" it is, the more you can define internal to it. If this is the case, then what exactly determines this sort of "strength" of a theory?
John Baez (Oct 09 2025 at 11:54):However, there are also theories like the theory of groups or the theory of topological spaces that we don't usually consider as theories we can define mathematical objects internally to.
Classical logicians call these theories structures and talk a lot about definable relations in these theories. That's probably because they're focused on "untyped" theories, i.e. theories with one basic type , so they less focused on defining objects other than subobjects of , which are the relations they're talking about.
John Baez (Oct 09 2025 at 11:58):But knowing some category theory we can easily talk about "objects definable in the Lawvere theory of groups" or "objects definable in the finite limits theory of groups" or "objects definable in the first-order theory of groups", etc. Here I've taken the same concept, "group", and imagined theories of in 3 different doctrines. As we increase the power of the doctrine, more objects become definable.
John Baez (Oct 09 2025 at 12:00):Here's my question about this. Which of the following two possibilities is the correct one: 1. There is a clear cut dividing line between theories in which one can define mathematical objects (like ZFC and RCA) and those in which one cannot (such as groups and topological spaces). If this is the case, then what is the nature of this dividing line? 2. There is a spectrum of theories: the "weaker" the theory, the less mathematical objects you can define internal to it, and the "stronger" it is, the more you can define internal to it.
I guess I'm coming down on side 2 of this question.
If this is the case, then what exactly determines this sort of "strength" of a theory?
I'm more used to think about the strength of a doctrine, as above, but I don't think I have it nicely formalized. Something about adjunctions between stronger doctrines and weaker ones?