Structural induction

Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields.

A well-founded partial order is defined on the structures ("subformula" for formulas, "sublist" for lists, and "subtree" for trees).

(Formally speaking, this then satisfies the premises of an axiom of well-founded induction, which asserts that these two conditions are sufficient for the proposition to hold for all x.)

It is recursively defined: As an example, the property "An ancestor tree extending over g generations shows at most 2g − 1 persons" can be proven by structural induction as follows: Hence, by structural induction, each ancestor tree satisfies the property.

If the set of all structures of a certain kind admits a well-founded partial order, then every nonempty subset must have a minimal element.

Suppose there is a counterexample; then there must exist one with the minimal possible number of interior nodes.

The partial ordering implied by 'smaller' here is the one that says that S < T whenever S has fewer nodes than T. Early publications about structural induction include: