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:
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 NaturalNumbers are defined by the original PeanoPostulates? this way:
@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 @somenumsNow, 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