Is there a generalization of transfinite recursion that allows defining proper classes?

Question

Transfinite recursion lets one define a sequence of sets $S_\alpha$, for $\alpha$ an ordinal. My question is whether it is possible to generalize this recursion to allow $S_\alpha$ to be classes, not just sets. I would be thankful for a reference to such a generalization.

In the Wikipedia article, the transfinite recursion is formalized using a class function $G: V \rightarrow V$, where $V$ is the class of all sets. The $S_\alpha$, for $\alpha \in \mathrm{Ord}$, is in particular a value of $G$, so it belongs to $V$ and thus is a set. This suggests that the generalization I'm looking for would run into a problem, because now values of $G$ would have to be classes, so we couldn't use a class function anymore. But maybe there is some other approach that goes around this problem.

Answer 1

Let me work with second-order set theories like $\mathsf{NBG}$ to handle classes more conveniently.

It depends on the complexity of classes you want to define. For example, the trivial sequence of classes (e.g., $S_\alpha=V$ for all $\alpha$) does not require any machinery beyond $\mathsf{NBG}$. However, not every class enjoys such property.

Before explaining the 'difficulty' of class recursion, let me start with a positive result: Morse-Kelley set theory $\mathsf{MK}$ proves such recursion is possible. More specifically, $\mathsf{MK}$ proves

Theorem. ($\Sigma^1_\omega$-transfinite recursion) Let $\phi(x,Y,P)$ be a formula of second-order set theory, with a class parameter $P$, and $R$ be a well-founded class relation with the transitive closure $<_R$. Then there is a class $S\subseteq \operatorname{dom}R\times V$ such that $$(S)_r=\{x:\phi(x,S\upharpoonright r, A)\}$$ for all $r\in \operatorname{dom}R$, where $S\upharpoonright r:=S\cap \{r'\in \operatorname{dom}R\mid r'<_R r\}\times V$.

(In fact, $\Sigma^1_\omega$-transfinite recursion is equivalent to the full second-order separation scheme over $\mathsf{NBG}$.)

We can see that $\Sigma^1_\omega$-transfinite recursion works with a class well-order instead of ordinals. The reason is that class well-orders may have a longer 'length' than the class $\mathrm{Ord}$ of all ordinals: $\mathrm{Ord}+1$ or $\mathrm{Ord}\cdot 2$ would be easy examples.

As we may expect, transfinite recursion over 'longer' well-order and 'with a more complex $\phi$' requires much power. According to a diagram in Williams' doctoral dissertation (printed page number 58, pdf page number 66 of the linked paper), the complexity of $\phi$ affects more the strength of the transfinite recursion scheme than the length of $<_R$. (Also note that Willams used $\mathsf{GBC}$ and $\mathsf{KM}$ for denoting $\mathsf{NGB}$ and $\mathsf{MK}$ respectively.)

We can see that transfinite recursion for first-order formulas (what Williams called $\Sigma^1_0$-formulas) of length $\omega$ proves the truth predicate of a first-order set theory exists. However, $\mathsf{NBG}$ does not prove there is a truth predicate of a first-order set theory since $\mathsf{NBG}$ is a conservative extension of $\mathsf{ZFC}$.

Thus, $\mathsf{NBG}$ has some non-definable classes. The truth predicate of first-order set theory is an example as we saw. Another example of a non-definable class over $\mathsf{NBG}$ is the class forcing relation, which is proved in

Victoria Gitman, Joel David Hamkins, Peter Holy, Philipp Schlicht, and Kameryn Williams. "The exact strength of the class forcing theorem." The Journal of Symbolic Logic 85.3 (2020) pp. 869 - 905.