Transfinite induction is an extension of mathematical induction that is applicable to well-founded classes such as an ordinal notation, an ordinal, the class $$\textrm{On}$$ of ordinals, and the class $$V$$ of sets. It can be used in proving the statements about ordinals such as comparisons of fast-growing functions, and in constructing maps on $$\textrm{On}$$ or $$V$$ such as elementary operators of ordinals and the rank of sets.

## Definition

Let $$P(\alpha)$$ be a predicate on an element $$\alpha$$ of a well-founded class $$(X,<)$$. Suppose that for all $$\alpha \in X$$, if $$P(\beta)$$ holds for all $$\beta \in X$$ satisfying $$\beta < \alpha$$, then $$P(\alpha)$$ also holds. Then transfinite induction tells us that $$P$$ is true for all $$\alpha \in X$$.

In the case $$(X,<) = (\textrm{On},\in)$$, although transfinite induction does not refer to whether $$\alpha$$ is a successor ordinal or not, a proof is frequently devided in to the following three cases:

• Zero case: prove that $$P(0)$$ holds.
• Successor case: prove that $$\forall \alpha \in \textrm{On} : P(\alpha) \rightarrow P(\alpha+1)$$ (for any successor $$\alpha$$, $$P(\alpha)$$ implies $$P(\alpha+1)$$) holds.
• Limit case: prove that $$\forall \lambda \in \textrm{On} \setminus \{0\} : (\forall \beta \in \lambda : \lambda \neq \beta+1) \rightarrow ((\forall \beta \in \lambda : P(\beta)) \rightarrow P(\lambda))$$ (for any non-zero limit ordinal $$\lambda$$, $$P(\beta)$$ implies $$P(\lambda)$$) holds.

## As axiom schema

In ZFC set theory, transfinite induction is a valid deduction. In other words, for any predicate $$P(\alpha)$$ on an element $$\alpha$$ of a well-founded class $$(X,<)$$, the closed formula "for all $$\alpha \in X$$, if $$P(\beta)$$ holds for all $$\beta \in X$$ satisfying $$\beta < \alpha$$, then $$P(\alpha)$$ holds" is provable in $$\textrm{ZFC}$$ set theory. This statement, which includes the quantification of the formula $$P$$ and the class $$(X,<)$$, itself is not a theorem in $$\textrm{ZFC}$$ set theory, but is a metatheorem, i.e. a theorem in the metatheory, on the provability of the transfinite induction schema.

In ZFC set theory, the axiom of regularity implies $$V = \textrm{WF}$$, where $$\textrm{WF}$$ denotes von Neumann universe, and hence the well-foundedness of $$(V,\in)$$. Therefore transfinite induction ensure the metatheorem that for any predicate $$P(x)$$ on a set $$x$$, the closed formula "for all set $$x$$, if $$P(y)$$ holds for all $$y \in x$$, then $$P(x)$$ holds" is provable in $$\textrm{ZFC}$$ set theory. On the other hand, when we deal with a weaker set theory such as KP set theory, the metatheorem does not necessarily hold. Therefore the transfinite induction on $$(V,\in)$$ or its restriction to a specific class of predicates can be non-trivial axiom schema.

When we deal with an arithmetic such as Peano arithmetic, then the well-foundedness of the formalisation of a recursive well-orderring in the metatheory is not necessarily provable in the arithmetic. Therefore the transfinite induction on a recursive well-orderring does not necessarily hold for the arithmetic. Therefore the transfinite induction on a recursive well-orderring can be non-trivial axiom schema. Indeed, when the metatheory is a set theory, we can define the notion of proof-theoretic ordinal using the provability of axiom schema for (premitive) recursive well-orderrings whose ordinal type is bounded by a given ordinal. Note that the precise definition of proof-theoretic ordinal is quite complicated, and is not literally given as the supremum of ordinals $$\alpha$$ in the metatheory such that the transfinite induction on the formalisation of a recursive well-orderring of ordinal type bounded by $$\alpha$$ holds for the arithmetic.

## Examples

There are many functions and hierarchies defined by transfinite induction: