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 numbers 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. 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: 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

[a1]	S. Feferman, “Theories of finite type related to mathematical practice”, J. Barwise (ed.), Handbook of mathematical logic, North-Holland (1977), pp. 913–972.