View source for Transfinite induction

A principle enabling one to infer that a proposition $ A(x) $ holds for every element $ x $ of a well-ordered class $ (E,<) $ if it is established that for each $ z \in E $, the truth of $ A(y) $ for all $ y < z $ implies the truth of $ A(z) $:
$$
(\forall z)((\forall y)((y < z) \Longrightarrow A(y)) \Longrightarrow A(z)) \Longrightarrow (\forall x) A(x).
$$

When $ E $ is the segment of [[Ordinal number|ordinal number]]s less than $ \alpha $, we have the following equivalent formulation: If

* $ A(0) $,
* $ A(\beta) \Longrightarrow A(\beta + 1) $, and
* $ A(\cdot) $ is preserved under limits, i.e., $ \displaystyle \left( \left( \beta = \sup_{i \in I} \beta_{i} \right) \land (\forall i \in I) A(\beta_{i}) \right) \Longrightarrow A(\beta) $,

then $ A(\beta) $ for any $ \beta < \alpha $. A special case of transfinite induction is [[Mathematical induction|mathematical induction]]. If the relation $ < $ defines on the class $ E $ a well-founded tree (i.e., a tree all branches of which terminate), then transfinite induction for such an $ E $ is equivalent to [[Bar induction|bar induction]]: If $ A $ is true for all end vertices and is inherited on moving from them towards the root, then $ A $ is true for the root. This form is important in intuitionistic mathematics. The deductive power of a formal system can often be measured in terms of the provability of transfinite induction up to various ordinals.

====References====

<table>
<TR><TD valign="top">[a1]</TD><TD valign="top">
S. Feferman, “Theories of finite type related to mathematical practice”, J. Barwise (ed.), ''Handbook of mathematical logic'', North-Holland (1977), pp. 913–972.</TD></TR>
</table>