Category-theoretic characterization of $L$

Question

Does there exist a characterization of Goedel's constructible universe $L$ in purely category-theoretic terms, or is constructibility an 'artifact' of material set theory? If, in fact, constructibility is an 'artifact' of material set theory, is there a category-theoretic 'analogue' for $L$?

Answer 1

$L$ is a very rigid and canonical object, so it's not that fundamentally difficult to write down a construction of the category of $L$-sets that is ostensibly couched in the language of category theory, but the result ends up not looking much like constructions you'd typically see in topos theory and other categorical treatments of set theory. (I'll discuss why I think this is somewhat inevitable at the end of my answer.) In particular, I don't think there's really a way to formalize this statement but in my mind the fact that $L$ is constructed by transfinite induction is in some sense essential. (The intuition that set theorists tend to have is that $L$ is a 'fattening of the ordinals'.)

A lot of work in 'fine structure' involves looking at hierarchies that are even more fine-grained than the typical one, but if we take the normal construction of $L$ and zoom out a little bit we can see structure that's not that foreign to category theory (although perhaps a little 'evil'). Recall the definition of the $L$-hierarchy: $L_0 = \varnothing$, $L_{\alpha+1}$ is the set of first-order definable subsets of $(L_\alpha,\in)$ (with parameters), and $L_\lambda = \bigcup_{\alpha < \lambda} L_\alpha$ for limit $\lambda$.

I want to think about this hierarchy only at the limit stages (i.e., stages of the form $L_{\omega\cdot\alpha}$). The following facts are relatively easy to verify:

• For every $\alpha > 0$, the collection of sets in $L_{\omega\cdot \alpha}$ is a category (with morphisms corresponding to functions in $L_{\omega\cdot\alpha}$ coded by their graphs). Moreover, it is a well-pointed Boolean pretopos.
• $L_\omega$ is equivalent to $\mathrm{FinSet}$ as a category.
• The inclusion of $L_{\omega \cdot \alpha}$ into $L_{\omega \cdot (\alpha + 1)}$ is a faithful exact functor. (Although note that it will not in general be full.) Moreover it is injective on objects.
• There is a category object in $L_{\omega\cdot(\alpha+1)}$ that is isomorphic to $L_{\omega\cdot \alpha}$. Moreover, this isomorphism is witnessed by data internal to $L_{\omega\cdot (\alpha+1)}$.
• For limit $\lambda$, $L_{\omega\cdot \lambda}$ is the directed colimit of the obvious diagram corresponding to $(L_{\omega\cdot\alpha})_{\alpha < \lambda}$.

Now, describing the precise relationship between $L_{\omega\cdot \alpha}$ and $L_{\omega \cdot (\alpha +1)}$ is somewhat complicated and not entirely clear categorically, but the construction of $L$ is so robust that we don't need to use that in particular. I will make the following semi-formal claim:

Semi-formal claim. Let $S$ be a 'sufficiently explicit' procedure that takes a small strict well-pointed Boolean pretopos $E$ and produces a small strict well-pointed Boolean pretopos $S(E)$ and an inclusion functor $\iota_E : E \to S(E)$ that 'preserves enough structure' (i.e., $\iota_E$ is faithful, exact, injective on objects, etc.) such that $S(E)$ contains a category object isomorphic to $E$ (with internal data witnessing this isomorphism). Let $E_0$ be a 'sufficiently explicit' small strict category equivalent to $\mathrm{FinSet}$. Define $(E_\alpha)_{\alpha \in \mathrm{Ord}}$ by $E_{\alpha + 1} = S(E_\alpha)$ and by taking colimits of the obvious diagram at limit ordinals. Then the large colimit of $(E_\alpha)_{\alpha \in \mathrm{Ord}}$ is equivalent to the category of $L$-sets.

Semi-formal proof. By sufficient explicitness, $E_0$ is isomorphic to a set in $L$ and $S$ is equivalent to a definable function in $L$ (when restricted to $L$), so we may assume without loss of generality that the construction is taking place in $L$. Conversely, since the $\iota_{E_\alpha}$'s preserve enough structure, the large colimit $E$ is a pretopos. It should be relatively straightforward to then verify that for every $\alpha$, there is a object with binary relation $(X_\alpha,R_\alpha)$ in $E_{\alpha}$ (or maybe something like $E_{\alpha+17}$) that is isomorphic to $(L_\alpha,\in)$. Since all of our categories are being treated strictly and by the sufficient explicitness of $S$, for any $\alpha$, there is an injection of the $E$-object isomorphic to $E_\alpha$ into some ordinal $\beta$ and therefore into $X_\beta$, implying that every object in $E$ is isomorphic to a subobject of some $X_\beta$, which is enough to show that the category of $L$-sets is equivalent to $E$, since $L$ will be able to build the isomorphism between $L_\beta$ and the internal $X_\beta$. ''$\square$''

In order to make the answer a tiny bit more mathematically legitimate, I'll say that the following choices are certainly sufficient for the above statement to be true. Let $E_0$ be the category of finite ordinals with arbitrary maps, and let $S$ be the operation that takes a strict well-pointed Boolean pretopos $F$, adjoins

• the 'strict diagram of $F$' (i.e., the set of objects in $F$, the set of morphisms in $F$, morphisms for the source, target, and identity-of-object maps, and subobjects for the partial morphism composition operator) and
• the coproduct $\coprod_{a \in \mathrm{ob}(F)}a$ along with attendant maps from the $a$'s and to the internal representation of $F$ ,

and closes under complements of subobjects and finite limits and colimits (as computed in $\mathrm{Set}$) in a 'freely strict' way (i.e., whenever we add a limit or colimit it is always a new object not equal to any of the other objects). (One thing to note here is that I'm actually closing under a little bit more than is required to get a Boolean pretopos, since I'm including coequalizers, but this doesn't matter because of how robust the construction of $L$ is. Essentially any 'reasonably explicit' notion of closure that's actually computed in $\mathrm{Set}$ and eventually allows for constructing subobjects via internal classical first-order logic should work. This is evidenced by the fact that in most fine structure hierarchies studied by set theorists, the levels of the hierarchy aren't even categories at many stages.)

---

So why is the $L$ construction so hard to state 'directly' in terms of, say, topos theory? I think there's actually a few reasons.

The first couple have to do with the internalization process. Internalizing the pretopos at some stage into the pretopos at the next stage forces us to consider them as strict categories. This is of course fairly anathema to category theory as a whole, but it's somewhat essential in understanding the behavior of $L$. The reason that the axiom of choice holds in $L$ is that everything in it is constructed so explicitly that every object has a very precise provenance that allows us to uniformly define well-orderings of every set. This kind of provenance is necessarily 'evil' to some extent; we're giving every object a unique identifying 'serial number' regardless of whether the object will eventually turn out to be isomorphic an earlier constructed object. (Note that in general, an isomorphism between two sets in $L_\alpha$ may not show up until some much later stage $L_\beta$. This is related to somewhat fundamental characteristics of the $L$-construction. I would guess that there is no direct 'explicit' construction of the skeleton of the category of $L$-sets.) This internalization is also something that seems to want close agreement between the external and internal logical properties of the pretopos, which in (pre-)topos theory in general do not always line up so well. (This is part of why replacement and collection are somewhat awkward to formalize in the context of arbitrary toposes, for instance.)

Another thing you might notice about the construction is that at no point did we explicitly adjoin power objects or exponential objects. This is absolutely crucial to the construction, because we're trying to avoid including too many things and full power sets are just too big. $L \cap \mathbb{R}$ is not in general equal to $\mathbb{R}$, for instance.) Everything in the construction is in some sense predicative except for the fact that we iterate along all of $\mathrm{Ord}$. (This was more or less Gödel's original intuition that led him to $L$.) In order to verify that power objects/sets exist in $L$, ostensibly one needs to rely on collection (essentially, in $V$, every $L$-subset of a set $x \in L$ must show up by some stage $\alpha$, so there's an $L_\beta$ at which they have all shown up by collection). Classically we get some more precise information about when we can expect these to show up by using the condensation lemma (which is why the $L$-construction still works in classical $\mathrm{Z}$ set theory and Mac Lane set theory as shown by Mathias in his tour de force paper The strength of Mac Lane set theory), but in constructive treatments of $L$, collection is the only known way to actually verify that power sets exist. This means that in particular, while there is probably a constructive variant of the above construction, in the context of arbitrary elementary toposes (which may have constructive internal logic), it's not a priori clear that the resulting category of $L$-sets would actually be a topos (rather than just a pretopos). And indeed it was shown by Matthews and Rathjen in their wonderfully titled paper Constructing the constructible universe constructively (with a really impressive argument combining $E$-recursive realizability and proof-theoretic ordinal analysis) that $L$ in $\mathsf{CZF}_{\mathcal{P}}$ (which is comparable to the theory of an elementary topos but actually slightly stronger) needn't even satisfy the exponentiation axiom. So it seems likely that the existing constructive treatments of $L$ cannot be adapted to topos theory in a way that will always produce toposes.

Answer 2

Consider the following statement from Lawvere's paper, "Cohesive Toposes and Cantor's 'lauter Einsen' (Philosophia Mathematicae (3) Vol. 2 (1994), pp. 5-15):

It might seem that G$\ddot o$del's $L$ would rest, if anything does, on von Neumann's a priori $\epsilon$-chains, but that was refuted twenty years ago by William Mitchell who showed how to construct it from a suitable given category, structured only by composition of maps; however, to my knowledge this has not been pursued since.

Though it might not be 'kosher' to answer a question with a question, why does Mitchell's construction not provide the necessary category-theoretic characterization of $L$ I seek (Mitchell's construction is contained in his papers, "Boolean Topoi and the Theory of Sets" (Journal of Pure and Applied Algebra 2(1972), 261-274) and "Categories of Boolean Topoi" (Journal of Pure and Applied Algebra 3 (1973) 193-201))?