On the definition of ordinal addition using transfinite recursion

Question

Am reading the textbook Introduction to Set Theory 3rd ed. by Hrbacek and Jech. In chapter 6 the authors present two versions of the transfinite recursion theorem:

Transfinite Recursion Theorem. Let $G$ be an operation. Then there exists an operation $F$ such that $F(\alpha)=G(F\restriction\alpha)$ for all ordinals $\alpha$.

Transfinite Recursion Theorem, Parametric Version. Let $G$ be an operation. Then there exists an operation $F$ such that $F(z,\alpha)=G(z,F_z\restriction \alpha)$ for all ordinals $\alpha$ and all sets $z$.

Then the authors use the parametric recursion theorem to define addition of two ordinals $\alpha$ and $\beta$, i.e. $\alpha+\beta$ is defined as $F(\alpha,\beta)$ where $F$ is defined as in the parametric recursion theorem for some suitable operation $G$.

But I have seen many textbooks (e.g. Enderton p. 232) define ordinal addition $\alpha+\beta$ using the usual non-parametric version. The idea is that for a fixed $\alpha$ you can define $\alpha+\beta$ as $F_\alpha(\beta)$ where $F_\alpha$ is taken from the non-parametric recursion theorem based on a suitable operation $G_\alpha$ (which depends on $\alpha$).

Basically the first definition is done in "one-shot" while the second definition is done "conditional" on a fixed ordinal $\alpha$.

Questions:

1. Is there anything wrong/informal about the second definition? (Am not an expert in logic).

2. If the second definition is correct, then why should we bother with the parametric version?

Thanks a lot for your help.

Answer 1

I will try to explain why the second definition is "incorrect/informal".

Basically one cannot "fix a set $y$" and define a formula $F_y(x)$ with free variable $x$.

What is really happening is that you are defining a formula $F(x,y)$ with two free variables $x,y$.

For more details one can look at the definition of ordinal addition on p. 26 of Kunen's book.

In particular the sentence : "More formally still, the subscripted $\alpha$ becomes an additional free variable in the formula $F$ occurring in our official explication of Theorem 9.3".