# Transfinite recursion and Replacement

I have a question about the use of Replacement when proving the transfinite recursion theorem. It seems that the crucial use of Replacement is made in the step involving the set of all partial functions defined over the ordinals (I'm being generic here, because I'm unsure if there is a stable terminology for these partial functions; Enderton talks about a function being "$\gamma$-constructed up to $t$", Jech and Hrbacek talk about "computations of length $\alpha$" an Schimmerling about $z$-approximations), as the class of all ordinals is, well, a class, and not a set, and so it's necessary to use Replacement in order to obtain the desired set. My question is: if the above reasoning is correct (and I'm not sure if it is!), then can we dispense with Replacement by setting an initial boundary (say, an ordinal $\theta$) to the recursive theorem? I'm thinking about something along Schimmerling's lines. Here's how he states the theorem on p. 35 of A Course on Set Theory:

"Suppose that $\theta$ is an ordinal. Let $F : \theta \times P \to B$ be a function where $B$ is a set and $P$ is the set of partial functions from $\theta$ to $B$. Then there is a unique function $G : \theta \to B$ such that $G(\beta) = F(\beta, G \restriction \beta)$ for every $\beta < \theta$."

This seems a bit weaker than the usual formulations of transfinite recursion, as it's only defined for ordinals up to $\theta$, and not all ordinals. So, is it still necessary to use Replacement to prove this version?

If $B$ is a set, then the claim is provable without replacement. For instance, the set of all functions from $\theta$ to $B$ is a subset of $\mathcal P(\theta\times B)$ (whose existence follows by union, powerset, and separation). So when you want to construct the union $f_\lambda$ of some partial functions $f_\beta$ from $\theta$ to $B$, you just use separation on $\mathcal P(\theta\times B)$ and then apply union. (For the successor case, we use pairing and union to add the pair $\langle \alpha, F(\alpha, f_\alpha)\rangle$ to $f_\alpha$). If we don't assume that the range of $F$ is a set, then we have the following interesting connection between the claim and replacement.
For simplicity, I'll work in an extension of ZFC - replacement with classes. I'll also assume that the $G$ in the claim is a set function (which I'll denote $g$). Then we can show that the claim for $\theta$ is equivalent to replacement from $\theta$ -- that is, it is equivalent to:
(*) If $F$ is a function on the ordinals, then $rng(F\upharpoonright \theta)$ is a set.
${\it Proof:}$ For the rtl direction, let $F$ be a function on the ordinals. Then define $F^*$ on $\theta\times P$ such that $F^*(\langle \beta, x\rangle) = F(\beta)$. Then, by the claim, there is a unique set function $g$ on $\theta$ such that $g(\beta) = F(\beta)$, for all $\beta<\theta$. Since $g$ is a set, $rng(g) = rng(F\upharpoonright \theta)$ is a set.
For the ltr direction, suppose that we have partial functions $f_\beta$ on all $\beta<\lambda <\theta$. Then, letting $F$ map $\beta$ to $f_\beta$ well get a set of the $f_\beta$'s. Applying union we get $f_\lambda$. (The successor case doesn't require replacement). $\Box$