It seems to me that MathematicalInduction is simply what you get when you apply RefactorMercilessly to mathematics itself, in a loose mental concept sort of way. Here's how it goes:

1) Mathematics contains many ''constructive'' definitions of sets, which (e.g.) define the set of Foo in two parts:

	* The designated element BAZ is an element of Foo.
	* Applying the function Phlorb to any element of Foo produces another element of Foo.

2) Mathematics contains many ''constructive'' definitions of predicates (boolean functions) which (e.g.) discuss the predicate Burble in two parts:

	* Burble is true for the designated element BAZ; i.e. Burble(BAZ) is true.
	* If Burble(Quux) is true, then Burble(Phlorb(Quux)) is demonstrably true.

Noticing the common behavior between these two methods leads us to conclude that Burble must be true for any Foo.

True Mathematicians will notice that I cheated in the first point above. There is usually a third clause, which says "Foo contains ONLY those elements that result from one of the two preceding rules." This allows the possibility that Burble is true for some things that are not in Foo, unless we can add a corresponding "but nothing else" clause to the definition of Burble, in which case we have shown that the predicate Burble selects exactly the elements of Foo.

As an application of this idea, consider that the NaturalNumber''''''s are defined by the original PeanoPostulates this way:

	* Zero is a member of the NaturalNumber''''''s.
	* If N is in the NaturalNumber''''''s, then Successor(N) is in the NaturalNumber''''''s.

Similarly, we can show that 2m+1 is odd for all NaturalNumber''''''s m by showing:

	* It is true for Zero; 2*0+1 = 1 is odd.
	* Whenever it is true for some NaturalNumber k, it must be true for Successor(k); from the fact that 2k+1 is odd (and the fact that adding 2 to an odd number yields an odd number) we can see that 2k+1 + 2 = 2k+2 + 1 = 2(k+1) + 1, all of which must be odd.

Having a soft spot for correctness arguments, I immediately see this as a way to show that a loop does what I intend, based on some fact that is invariant across the loop. (Pardon the fact that the example is in Perl... I don't know Smalltalk well enough to compose at the keyboard with confidence.)

 @somenums = (3, 4, 1, 7, 2, 9, 6);
 # I need to total the above numbers (yeah, trivial example!)

 $total = 0; @temp = @somenums;
 # after 0 times thru the loop, $total + sum @temp = sum @somenums

 while (@temp) {
  $total += shift @temp;
  # this preserves my invariant that $total + sum @temp = sum @somenums
 }

 # on exit, @temp is empty, therefore sum @temp = 0 ...
 # therefore $total = sum @somenums
Now, of course, no practicing programmer would write it this way. This is exactly analogous to the fact that we begin in junior high algebra by writing each tiny step in detail, skipping the detailed steps only once we have satisfied ourselves (and our teacher) that we have mastered them. (And we can still make occasional mistakes trying to do too much at once!) Just as the experienced algebraist could have stated 2k+1 + 2 = 2(k+1) + 1 without needing the intermediate step above, the experienced programmer could have stated

 $total = 0;
 foreach (@somenums) {$total += $_}
without needing the explicit intermediate reasoning about @temp (assuming, of course that foreach is guaranteed to visit each element exactly once!)

-- JoelNeely
----
CategoryMath