Editing Structural induction (section)

{{short description|Proof method in mathematical logic}}

'''Structural induction''' is a [[proof method]] that is used in [[mathematical logic]] (e.g., in the proof of [[Ultraproduct#Łoś's theorem|Łoś' theorem]]), [[computer science]], [[graph theory]], and some other mathematical fields.  It is a generalization of [[mathematical induction|mathematical induction over natural numbers]] and can be further generalized to arbitrary [[Noetherian induction]].  '''Structural recursion''' is a [[recursion]] method bearing the same relationship to structural induction as ordinary recursion bears to ordinary [[mathematical induction]].

Structural induction is used to prove that some proposition {{math|''P''(''x'')}} holds [[for all]] {{mvar|x}} of some sort of [[recursive definition|recursively defined]] structure, such as
[[First-order logic#Formulas|formulas]], [[List (computer science)|lists]], or [[Tree (graph theory)|trees]].  A [[well-founded]] [[partial order]] is defined on the structures ("subformula" for formulas, "sublist" for lists, and "subtree" for trees).  The structural induction proof is a proof that the proposition holds for all the [[minimal element|minimal]] structures and that if it holds for the immediate substructures of a certain structure  {{mvar|S}}, then it must hold for  {{mvar|S}} also. (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 {{mvar|x}}.)

A structurally recursive function uses the same idea to define a recursive function: "base cases" handle each minimal structure and a rule for recursion.  Structural recursion is usually proved correct by structural induction; in particularly easy cases, the inductive step is often left out.  The ''length'' and ++ functions in the example below are structurally recursive.

For example, if the structures are lists, one usually introduces the partial order "<", in which {{math|''L'' < ''M''}} whenever list {{mvar|L}} is the tail of list {{mvar|M}}.  Under this ordering, the empty list {{math|[]}} is the unique minimal element.  A structural induction proof of some proposition {{math|''P''(''L'')}} then consists of two parts:  A proof that {{math|''P''([])}} is true and a proof that if {{math|''P''(''L'')}} is true for some list {{mvar|L}}, and if {{mvar|L}} is the tail of list {{mvar|M}}, then {{math|''P''(''M'')}} must also be true.

Eventually, there may exist more than one base case and/or more than one inductive case, depending on how the function or structure was constructed. In those cases, a structural induction proof of some proposition {{math|''P''(''L'')}} then consists of: 
{{ordered list|list_style_type=upper-alpha
|a proof that {{math|''P''(''BC'')}} is true for each base case {{mvar|BC}},
|a proof that if {{math|''P''(''I'')}} is true for some instance {{mvar|I}}, and {{mvar|M}} can be obtained from {{mvar|I}} by applying any one recursive rule once, then {{math|''P''(''M'')}} must also be true.}}