Well-founded induction is the natural generalization of mathematical induction to sets other than the natural numbers. It is also sometimes called Noetherian induction, after Emmy Noether.
Proposition. Let (A, ≤) be a well-founded partial order, and let Φ be a property such that (*) if Φ(x) for all x<y then Φ(y). Then we have Φ(x) for every x∈A.
The condition (*) above implies that &Phi(y) for all minimal elements y∈A. If y is a minimal element, then there are no elements x<y, so the hypothesis is vacuously true.
To see why this works, form the set of counterexamples C = {x∈A|not &Phi(x)}. Assume this is non-empty. Then it has a minimal element c. Since c is minimal, we know that Φ(x) holds for all x<c. But then we can use (*) to conclude that Φ(c) holds, which is a contradiction.
The converse is in fact also true: if (A, ≤) is a partial order such that ((∀x<y . Φ(x)) ⇒ Φ(y)) ⇒ ∀x∈A . Φ(x), then (A, ≤) is well-founded. The proof is a fiddly induction argument.
Well-founded induction can be convenient because some problems are easier to think about in terms of some other partial order than the natural numbers. Here is an example, typical of some computer science problems. We wish to compute a certain function using the following program:
fun A(0,n) = n+1
| A(m,0) = A(m-1,1)
| A(m,n) = A(m-1, A(m, n-1))
The problem is showing that the recursion terminates for all pairs (n,m) of natural numbers. If we try to use mathematical induction on m or n, we run into difficulties with the third line, where the second argument in the recursive call quickly is growing large.
Instead, we use well-founded induction. Take the ordered set to be N2 under the lexicographic order (this is a well-founded order). Let the property be Φ(m,n) ⇔ A(m,n) terminates. We want to show (∀(n',m')<(n,m).Φ(n',m'))⇒&Phi(n,m).
There are three cases: (1) m=0. Then the first clause applies and the computation immediatly terminates with value n+1. (2) m≠0 and n=0. The second clause applies. But (m-1,n)<(m,n), so by the induction hypothesis A(m-1,1) will terminate. (3) m,n≠0. The third clause applies. (m,n-1)<(m,n), so A(m, n-1) will terminate and yield some value N. Also, (m-1,N)<(m,n) for all N, so A(m-1, N) will also terminate. End of proof.
The set of natural numbers is well-founded, so normal mathematical induction is a special case of well-founded induction. Furthermore, the set of ordinals is well-founded, so transfinite induction is another special case. | 
