Structural Induction vs Normal (Mathematical) Induction

Question

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?

Answer 1

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. Also notice that as Zhen Lin points out Noetherian induction cannot always be reduced to normal induction on the natural numbers. His example is particularly clear since the ordinals are uncountable while the natural numbers are countable.

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$