[Haskell-cafe] Induction (help!)

[PR Stanley]

You've got the right idea.
	Paul: At long last! :-)
	I should point out that it doesn't make sense to say p(Succ n) = 
Succ(p(n)),  p(x) represents some statement that is either true or 
false, so it doesn't make sense to say Succ(p(n)). .
	Paul: okay, da capo: We prove/test through case analysis
that the predicate p holds true for the first/starting case/element 
in the sequence. When dealing with natural numbers this could be 0 or 
1. We try the formula with 0 and if it returns the desired result we 
move onto the next stage. If the formula doesn't work with 0 and so 
the predicate does not hold true for the base case then we've proved 
that it's a nonstarter.

In the inductive step we'll make a couple of assumptions: we'll 
imagine that p(j). We'll also assume that p holds true for the 
successor of j - p(j+1).
Then with the help of rules and the protocol available to us we'll 
try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1)
So, we know that the predicate holds for 0 or at least one element. 
By the way, could we have 3 or 4 or any element other than 0? Anyway, 
p(0). Then we set out to find out if p holds for the successor of 0 
followed by the successor of the successor of 0 and so forth. 
However, rather than laboriously applying p to every natural number 
we innstead try to find out if f(j+1) - f(1) will take us back to 
fj). I think this was the bit I wasn't getting. The assumptions in 
the inductive step and the algebraic procedures are not to prove the 
formula or premise per se. That's sort of been done with the base 
case. Rather, they help us to illustrate that f remains consistent 
while allowing for any random element to be succeeded or broken down 
a successive step at a time until we reach the base/starting element/value.
Okay so far?

Cheers
Paul