FOM: strengthening induction hypotheses

[Todd Wilson]

This recent bunch of posts on mathematical induction reminds me of
some basic questions I've wondered about from time to time.  Please
pardon me if they seem too trivial.

Is there any good explanation of the phenomenon that in order to prove
P(n) for all natural numbers, it is often necessary to strengthen the
induction hypothesis by replacing P with Q such that Q(n) => P(n)
for all n, but that Q(n) => Q(n+1) is somehow easier to establish
than P(n) => P(n+1)?

If P(n) is true for all n, then certainly P(0) and P(n) => P(n+1) for
any n, so it's not that P *can't* be proven directly by induction.  Or
can it?  Could it be that the only way to show that P(n) => P(n+1) for
all n is to first show P(n) for all n?  Does it even make sense, in
proof theory, to ask whether the only way to prove B is to first prove 
an equivalent statement A?

Finally, are there any general procedures that suffice, in many cases,
to obtain Q from P, or is it entirely human ingenuity?  For example,
it seems that the set of "good induction hypotheses" are the formulas
that are (relatively speaking) easily shown to be "closed under
successor".  Are there any useful closure procedures that, at least in
some cases, could close up P (perhaps through some iterative process)
to produce Q?  I'm thinking of something that might be useful in an
automated theorem prover.

-- 
Todd Wilson
Computer Science Department
California State University, Fresno