Am Freitag, 9. Mai 2008 13:50 schrieb PR Stanley: > 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. > > Well, it might hold for all n >= 3. But you're right, if p doesn't hold > for the base case, then it doesn't hold for _all_ cases. > Paul: I don't understand the point you're contending. We've chosen 0 > as our base case and if p(0) doesn't hold then nothing else will for > our proof. Granted, you may want to start from 3 or 4 as your base > case but we're not doing that here and for all we know forall n >= 3 > p(n) but this isn't relevant to our proof, surely.
Right. I only wanted to say that we might have chosen the wrong base case for the proposition. If p(0) doesn't hold, then obviously [for all n. p(n)] doesn't hold. But [for all n. p(n) implies p(n+1)] could still be true, and in that case, if e.g. p(3) holds, then [for all n >= 3. p(n)] holds. So if the base case fails, still a large portion of the proposition might be saved, but if the induction step fails, that is not so. > > Paul: 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). > > Daniel: No. In the induction step, we prove that > IF p(j) holds, THEN p(j+1) holds, too. > p(j) is the assumption, and we prove that *given that assumption*, p(j+1) > follows. > Then we have proved > (*) p(j) implies p(j+1), for all j. > Paul: No, you haven't proved anything! I'm sorry but your assertion > fails to make much sense. Sorry? The induction step consists of proving that WHATEVER j is, IF p(j) holds, THEN p(j+1) holds, too. If or when we have done that, it is tautological to say that we proved (*) for all j. [p(j) implies p(j+1)]. In the notation used by Ryan Ingram yesterday, the induction step consists of proving L, j :: Nat |- p(j) => p(j+1) typically, that is done via proving L, j :: Nat, p(j) |- p(j+1) , i.e. proving p(j+1) under the assumption p(j), which by the logical rule of deduction/implication introduction is equivalent to L, j :: Nat |- p(j) => p(j+1). > > Daniel: If we already have established the base case, p(0), we have > p(0) and (p(0) implies p(1)) - the latter is a special case of (*) - from > that follows p(1). > Then we have > p(1) and (p(1) implies p(2), again a special case of (*), therefore p(2). > Now we have p(2) and (p(2) implies p(3)), hence p(3) and so on. > > Paul: 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? > > Daniel: Sure, anything. Start with proving p(1073) and the induction > proves p(n) for > all n >= 1073, it does not say anything about n <= 1072. > > Paul: 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe