Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: Mathematical objects internal to theories

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 $\text{RCA}_0$.

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 $\text{Hom}_F(1,\mathbb{N})$ and the actual natural numbers, as well as surjections from $\text{Hom}_F(\mathbb{N}^m, \mathbb{N})$ 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 $\text{RCA}_0$.
...
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 $X$, so they less focused on defining objects other than subobjects of $X^n$, 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?

John Onstead (Oct 09 2025 at 18:35):

John Baez said:

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.

I'm a little bit confused by this. Shouldn't there be a difference between the concepts "mathematical object defined in a theory" and "object internal to the syntactic category of the theory"? For instance, let's consider a set theory. A "group" in the set theory is simply an element of some "universe" of that set theory satisfying certain properties. On the other hand, the syntactic category of a set theory isn't itself some category of sets, and so it's unlikely a group object internal to it has anything to do with the actual groups one can define within that theory of sets. (Though that does raise the question of what exactly a group object internal to the syntactic category is supposed to be, if anything.)

John Onstead (Oct 09 2025 at 18:37):

John Baez said:

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?

I think I understand. I remember seeing somewhere a spectrum of doctrines, something like finite products -> finite limits -> regular -> coherent -> geometric -> first order or something like that.

John Baez (Oct 09 2025 at 19:25):

On the other hand, the syntactic category of a set theory isn't itself some category of sets, and so it's unlikely a group object internal to it has anything to do with the actual groups one can define within that theory of sets.

They're not the same, but I think there's a strong relation. If you take a group object internal to the syntactic category of a theory $T$, and then take a model of $T$ in $\mathsf{Set}$, you should get a group object in $\mathsf{Set}$, which is just a group.

John Baez (Oct 09 2025 at 19:27):

By the way, $T$ can even be some theory of sets, like $T = \text{ZFC}$. This example is perhaps confusing, because the concept of set is showing up in two different ways, but people study models of $\text{ZFC}$ in $\mathsf{Set}$ all the time in set theory.

John Onstead (Oct 15 2025 at 09:38):

Hi, sorry for taking so long to get back to this, I had to think about it for a while!

John Baez said:

They're not the same, but I think there's a strong relation. If you take a group object internal to the syntactic category of a theory $T$, and then take a model of $T$ in $\mathsf{Set}$, you should get a group object in $\mathsf{Set}$, which is just a group.

So if I take $T$ to be a syntactic category for any theory, and define $F: T \to \mathrm{Set}$ as a model, almost always this means $F$ is at minimum finite product preserving. If I then have a group object in $T$, given by $G: \mathrm{Group} \to T$, then I can just compose these two finite product preserving functors to get a finite product preserving functor $F \circ G: \mathrm{Group} \to \mathrm{Set}$, IE, a group object in Set. I hope that's right!

John Onstead (Oct 15 2025 at 09:40):

However, I still am trying to understand the idea of a "definable object in a theory" and what that means. In category theory, this is given as an object of some category (usually Set) equipped with extra structure and property, but in material math (like ZFC), this is given as an element of some set (a "universe") equipped with extra property (I guess this is almost a sort of decategorification?) I'm struggling to see how this "extra property" (written as a string in the logical language of the set theory) manifests in the context of the syntactic category for some set theory.

John Onstead (Oct 15 2025 at 09:40):

For instance, let $T$ be the syntactic category for some set theory (like ZFC). Define $S$ to be the object in $T$ such that a model functor $M: T \to \mathrm{Set}$ sends $S$ to the universe of sets of the model $M$, $\mathrm{sets}(M)$. Might there be an object $G$ in $T$ along with a monomorphism $m: G \to S$ such that applying $M$ gives the injective function $M(m): \mathrm{groups}(M) \to \mathrm{sets}(M)$ which is precisely the very injective function that embeds the set of all groups in $M$ into the set of all material sets in $M$?

John Baez (Oct 16 2025 at 13:53):

You are blending category theory and traditional logic (untyped first-order logic and material set theory like ZFC) in a way that seems not to have been studied as much as it should be. So I think you may be on new ground - sadly. I.e., you may need to make up your own definitions and prove your own theorems.

Why is this? I think it's because people who care about "syntactic categories" tend to shun untyped first-order logic and material set theory. There are more convenient frameworks if you like category theory.

Unfortunately there are still a lot of deep results about set theory that haven't been translated to these more convenient frameworks.

But people have to decide whether they're going to invest energy into the old frameworks or the new ones.

John Onstead (Oct 17 2025 at 09:12):

John Baez said:

You are blending category theory and traditional logic (untyped first-order logic and material set theory like ZFC) in a way that seems not to have been studied as much as it should be. So I think you may be on new ground - sadly. I.e., you may need to make up your own definitions and prove your own theorems.

Hmm... well, for what it's worth, I've come across the following relevant observation- maybe it will help?

John Onstead (Oct 17 2025 at 09:13):

Let's assume there does exist an object $G$ in $T$ such that for any model $M$ of $T$, $M(G)$ is the set of sets that satisfy the property of being groups in $M$. Now, we have a Yoneda embedding $y: T^{op} \to [T, \mathrm{Set}]$ (or $[T, \mathrm{SET}]$ if $T$ is large, which it probably is). $M$ is an object in this copresheaf category, and the Yoneda lemma states that the set of natural transformations between $y(G)$ and $M$ is $M(G)$. However, above we assumed that $M(G)$ is the set of groups in $M$. Thus, every morphism from $y(G)$ into $M$ "picks out" a group in $M$. Even better, $\mathrm{Mod}(T)$ is a full subcategory of that copresheaf category, meaning the same holds true in there, with the model $y(G)$ of the set theory basically the "walking group" set theory model.

John Onstead (Oct 17 2025 at 09:13):

Why I find this so remarkable is that this is a direct decategorification of the idea of "functorial semantics". To categorify the above we just need to replace $\mathrm{Mod}(T)$ with the 2-category of finite product categories (the category of models in Cat of the 2-theory of finite product categories), $y(G)$ with the Lawvere theory of groups, and $M$ with any finite product category (IE, Set) we want to define group objects internally to! So if this is true then it would demonstrate there actually isn't much of a difference between the traditional way of doing logic and categorical logic.

John Onstead (Oct 20 2025 at 10:12):

For anyone who was interested, I've found the solution to all these questions. The objects of a syntactic category are "contexts", and in the case of ZFC for instance, they are "formulas in context" $\set{x, y, ... | P}$ where $P$ is some property written in the language of the theory. This is meant to be a sort of "abstract class", that is, "all variables $(x, y, ...)$ such that $P$ holds". When we apply a model functor, it instantiates this abstract class as an actual class- namely, it returns the class of all material sets in that model which satisfy property $P$. This is grounded in where the model functor sends the special object $\set{x | T}$, where T is the property that always evaluates to "true", and hence is sent to the class of all material sets in the model. More elaboration can be found starting on page 2 here.

John Onstead (Oct 20 2025 at 10:13):

This resolves the question since the definition of a group can be encoded as a property $\mathrm{Group}(x)$ which can be thought of as taking in a material set and returning "True" if that set is a group, and "false" if it is not. Hence, there indeed exists an object in the syntactic category $\set{x | \mathrm{Group}(x)}$ that does exactly what is described above. Indeed, the definition of any mathematical object in ZFC can be written in the language of ZFC + FOL, and hence as such a formula $P$, and so appears as an object in its syntactic category.