The (transfinite) induction principle says that, for any property $P(\alpha)$, the following is a theorem:
$$ \forall \alpha \in On \ [(\forall \beta<\alpha \ P(\beta)) \implies P(\alpha)]\implies \forall \alpha \in On \ P(\alpha) $$
where $On$ denotes the class of ordinals. We can also allow parameters: If $P(\alpha,p_1,\dots,p_k)$ is a property then the following is also theorem:
$$ \forall p_1 \dots \forall p_k \bigg( \forall \alpha \in On \ [(\forall \beta<\alpha \ P(\beta, p_1,\dots,p_k)) \implies P(\alpha, p_1,\dots,p_k)]\implies \forall \alpha \in On \ P(\alpha, p_1,\dots,p_k) \bigg ) $$
In practice I find it difficult to choose what should be the parameters in my proofs. To be specific consider the following theorem:
Theorem. Let $(W_1,<_1)$ and $(W_2,<_2)$ be well-ordered sets, isomorphic to ordinals $\alpha_1$ and $\alpha_2$ respectively, and let $(W,<)$ be the sum of $(W_1,<_1)$ and $(W_2,<_2)$. Then $(W,<)$ isomorphic to the ordinal $\alpha_1+\alpha_2$.
The proof is "by induction on $\alpha_2$". However there are different ways to look at the property to be proven:
- $P(\alpha_2)$, no parameter. This is obtained by quantifying over $\alpha_1,W_1,W_2$.
- $P(\alpha_1,\alpha_2)$, one parameter. This is obtained by quantifying over $W_1,W_2$.
- $P(W_1,W_2,\alpha_1,\alpha_2)$, three parameters.
For case 1 the proof would apply transfinite induction without parameters.
For case 2 instead the proof would start by fixing some arbitrary ordinal $\alpha_1$, appeal to the parametic version of transfinite induction to deduce that $P(\alpha_1,\alpha_2)$ holds for all ordinals $\alpha_2$, and then apply universal generalization to deduce that $P(\alpha_1,\alpha_2)$ holds for all ordinals $\alpha_1,\alpha_2$. Similarly for case 3.
The proof of the theorem is given here. For this specific example I think all three methods work. But how to choose in general?