Justification of inductive definitions in formal ZFC

Question

General question: How can one justify inductive definitions in formal ZFC?

Usually, if we want to define a notion per recursion, we just write for example

$$F_1 = 1; \, F_2=1$$ $$F_{n+2} = F_n + F_{n+1}\quad\text{where }n\geq 1$$

and trust that this yields a unique sequence $(F_n)$. If one wants to formalize this process, the first thing that comes to my mind is that this can be viewed as an axiomatic definition: we just state the properties we want the notion that is to be defined to have. But formal ZFC – the first-order theory over the language $\{\in\}$ – is static, we can't do that.

But how can we justify the definition in formal ZFC? Can one prove in ZFC that

$$\text{there is a unique sequence $(F_n)$ such that the above properties hold}$$ ? Or can one give a formula $\phi(x,y)$ that expresses $F_x = y$?

In the first possibility (proof that this sequence is unique), one talks about the notion of a sequence. This isn't possible if one wants to define per recursion a notion where the domain would be a proper class, as for example in the definition of the von Neumann universe:

$$V_0=\emptyset$$ $$V_{\beta+1}= P(V_{\beta})$$ $$V_{\lambda}=\bigcup_{\beta<\lambda} V_{\beta}$$

The ordinals do not constitute a set, therefore one can't speak about the sequence $(V_{\alpha})$ directly. But then, how can one speak about $(V_{\alpha})$ in formal ZFC? Can one give a formula $\phi$ that defines this notion?

Answer 1

Your instinct is right: for class-length inductions, we use formulas. So, for example, the statement "The sequence $V_\alpha$ ($\alpha\in ON$) exists" isn't quite right; rather, we can write down a formula $\varphi$ of two variabls such that $\varphi(x, y)$ means that $y$ is an ordinal and $x=V_y$. We can now argue that $V_\alpha$ exists for every ordinal, by showing that for every ordinal $\alpha$ there is some $x$ such that $\varphi(x, \alpha)$ holds; and to do this we use induction on the ordinals, that is, the fact that every nonempty set of ordinals has a least element. Note that we can talk about "arbitrary ordinal-length sequences": namely, a set $s$ is a sequence of ordinal length iff for some $\alpha$ and some set $X$, $s$ is a function from $\alpha$ to $X$. We then have in ZFC:

Suppose $\varphi$ is a formula in two variables such that for every sequence of ordinal length $s$, there is exactly one $x$ such that $\varphi(s, x)$ holds. Then for every ordinal $\alpha$, there is a unique sequence $t$ of length $\alpha$ (that is, function out of $\alpha$) such that for all $\gamma<\alpha$, $\varphi(t\upharpoonright\gamma, t(\gamma))$ holds.

So, for instance, for every $\alpha$ we can define the sequence $(V_\beta:\beta<\alpha)$ via the claim above applied to the formula $$\varphi(s, x)\equiv\mbox{$s$ is a sequence of length $\gamma$ for some $\gamma$, and $x=\mathcal{P}(\bigcup ran(s))$.}$$