I was studying some Proof Theory in Pohlers' Proof Theory: first step into impredicativity , and I found myself facing a Set Theory's problem.
We need to define this transfinite hierarchy of proper classes:
$$\mathcal{C} (0) = H $$
$$\mathcal{C} ( \alpha + 1) = \mathcal{C} (\alpha) ' $$
$$ \mathcal{C} (\lambda) = \bigcap \{ \mathcal{C} (\delta) | \delta < \lambda \} ,\ if\ \lambda\ is\ a\ limit $$
Here, H is the (proper) class of principal ordinals (or additively indecomposable) and, if M is a class, M' is its derivative class (the precise definition of these concepts are not important for our pourposes). Those familiar with proof theory will see that this is just a step toward the definition of the hierarchy of Veblen functions, wich, in turn, is used to build a notation system for ordinals below $ \Gamma_0 $.
Well, the problem is this: is it possible to justify in ZFC a definition like that? If it is, How can I do that? The usual form of general transfinite recursion theorem (wich is yet a theorem-scheme) can justify the definition of hierarchies like the hierarchy of Aleph Numbers, or the hierarchy of Constructible Sets, and so on, where at each step of the recursion what is produce is a set , not a proper class. Just for clarity, the "usual form of general transfinite recursion theorem" that I'm talking about is this (see, for example, Set theory: an introduction to independence proofs, Kunen, 1980, pag. 25) :
Let $\psi(x,y)$ be a formula such that ZFC proves $\forall x \exists! y\ \psi(x,y)$ ; let's call G(x) the unique y such that $\psi(x,y)$ (i.e. , G is a class-function). Then, we can write another formula $\phi(u,w)$ such that:
1- ZFC proves $\forall \alpha \exists!w \phi(\alpha,w)$; let's call F($\alpha$) the unique w such that $\phi(\alpha,w)$. Here, obviously, $\alpha$ ranges over the class of ordinals.
2- ZFC proves $\forall \alpha\ [ F(\alpha)=G(F\lceil \alpha)]$
Now, the problem is that the "condition of existence" I need is not satisfied, as outputs of $\mathcal C$ are proper classes; so, this definition's pattern is not available for the definition of the hierarchy above mentioned. Any suggestion about how to handle this kind of situation in ZFC?
Thank you.
We can define the kind of recursion you specified directly for set initial segments of $H$, i.e. starting with $H\cap\alpha$ for any given $\alpha$, instead of the whole $H$. This proceeds with the usual transfinite recursion that you mention. We use this to define the recursion instead, and show that it works.
For any ordinal $\alpha$ and $C_\alpha=H\cap\alpha$, define sets $C_\alpha(\beta)$ as follows:
$C_\alpha(0)=C_\alpha$,
$C_\alpha(\beta+1)=C_\alpha(\beta)'$,
$C_\alpha(\beta)=\bigcap_{\gamma<\beta}C_\alpha(\gamma)$ for limits $\beta$.
Observe that $C_{\alpha}(\beta)\subseteq\alpha$ for all $\beta$, and if $\alpha_0<\alpha_1$ then $C_{\alpha_0}(\beta)=C_{\alpha_1}(\beta)\cap\alpha_0$ for all $\beta$.
For all ordinals $\beta$, define $C(\beta)=\{\xi\bigm|\exists\alpha\ [\xi\in C_\alpha(\beta)]\}$.
So $\xi\in C(\beta)$ iff $\xi\in C_\alpha(\beta)$ for some $\alpha>\xi$ iff $\xi\in C_\alpha(\beta)$ for all $\alpha>\xi$.
This gives a uniform definition of classes $C(\beta)$, done in ZF. Now observe that they satisfy the recursion that you specified, i.e. $C(0)=H$, $C(\beta+1)=C(\beta)'$, and intersections at limits.