Structural Induction vs Normal (Mathematical) Induction

In computer science and semantics I have come across structural induction many times. In that context, it is often presented as something different from but similar to mathematical induction, sometimes being described as a generalization of it, and often proofs or discussions of foundations are omitted, replaced with an appeal to plausibility. Wikipedia's Structural Induction page states that "Just as standard mathematical induction is equivalent to the well-ordering principle, structural induction is also equivalent to a well-ordering principle." While that doesn't quite say it and I don't have a reference that says it, I suspect that structural induction is mathematical induction on a well founded structure that may not be the natural numbers, and who can tell about Zorn's Lemma? I also suspect that it can be reduced to mathematical induction over the natural numbers if one is clever enough. Do I have that right, and can you point me to any references that get into these types of details of the mathematical/foundational aspects of this computer science-y topic?

• No, structural induction cannot always be reduced to mathematical induction. (For example, transfinite induction over the ordinals.) However, mathematical induction is a special case of structural induction. Jan 9 '15 at 19:27
• Structural induction is a special case of Noetherian induction, however it doesn't seem to be clear when something is Structural induction. Vaguely the relation on the well founded set needs to be defined by some kind of recursion. Jan 9 '15 at 20:15
• Sect. 4.7 of Makinson's "Sets, Logic and Maths for Computing" provides a very accessible introduction to recursion and induction over well-founded sets (a.k.a. Noetherian induction). While mathematicians are happy with defining a structure as the least set closed under a certain set of constructing rules, a computer scientist is often happier to have data structures defined bottom up by the same set of rules, as this will allow her more naturally to implement operations by (structural) recursion and to perform verifications by (structural) induction. Jan 11 '15 at 23:43
• Thanks for the pointer to Makinson's book, @JMarcos.
– joeA
Jan 13 '15 at 1:52

The point of structural induction is to prove a property $P$ holds for all elements of a well founded set $S$. To do this you can assume it is not true, then there is a non-empty set $Q$ consisting of the objects that don't satisfy $P$. Since $S$ is well founded $Q$ contains a minimal element $m$. When we refer to structural induction the relation on $S$ is usually defined recursively (That is if $m<n$ if and only if $n$ can be obtained using the recursion on $m$ a finite number of times. Since $S$ is defined recursively the trick is usually to take an element $c$ smaller than $m$ and prove $m$ satisfies $P$ by using the fact $c$ satisfies $P$ and $m$ can be obtained from $c$ using the recursion. but if $c$ is in $P$ $m$ cannot be minimal, a contradiction.
Structural induction is useful when the recursion branches out into many levels and it is not very clear. For example consider the proof of the Sprague Grundy theorem, where one position $a$ is smaller than position $b$ if position $b$ is an option of position $a$