Well-founded induction

The well-founded induction is a formal mathematical proof methodology , which is also in computer science (for example, in functional programming languages ) applies. The principle is: Show that a statement is true for all elements , provided that it is true for all "smaller" elements. A well-founded relation is required as the “smaller” order relation . ${\displaystyle \operatorname {A} }$ ${\displaystyle \prec }$

The scheme of well-founded induction is:

${\displaystyle {\frac {\forall y{\Big (}{\big (}\forall z\prec y\ \operatorname {A} (z){\big )}\Rightarrow \operatorname {A} (y){\Big )}}{\forall x\ \operatorname {A} (x)}}}$

In contrast to structural induction, there is no explicit induction basis and also no explicit induction step: The statement must be shown for all , assuming that applies to all . (The latter proof is analogous to the usual complete induction step.) If the premise is empty, which means that there are no smaller elements than , then there is an implicit base case. ${\displaystyle \operatorname {A} (y)}$ ${\displaystyle y}$ ${\displaystyle \operatorname {A} (z)}$ ${\displaystyle z\prec y}$ ${\displaystyle \forall z\prec y\ \operatorname {A} (z)}$ ${\displaystyle y}$

See also

• Well-founded relation
• Well-founded set # Noetherian induction
• Complete induction