On 5/8/08, Daniel Fischer wrote:

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.

To formalize this, you can work in a system of logic with the following rules: Variable introduction: x is not free in L, L |- t is a type proves L, x :: t |- x :: t --- this is a proof of "x has type t" Forall introduction (removing the above assumption) L, x :: t |- p proves L |- forall x :: t. p Assumption of a proposition: L, p |- p --- no pre-requisites Impication introduction ("Deduction"; if P then Q) L, p |- q proves L |- p => q The part to the left of the |- is an "environment"; it represents assumptions you have made up to this point. The part to the right is a statement which is "true" in that environment; the L just represents "any environment". For example, in the first rule, we say that if we know that t is a type, and we haven't assumed anything about x yet, we can assume that x is a member of that type. Then in the second rule, if we've proved some proposition "p" once we've assumed that x is something of type t, we can say that p holds for -all- x of type t; we didn't assume anything about that x besides its type. Induction corresponds to adding the following rule to the logic: L |- p(0) L |- forall x :: Nat, p(x) => p(x+1) proves L |- forall x :: Nat, p(x) A "true" statement is one that holds with no environment: |- p Now, if you are proving something by induction, you had to prove that second line; and the only way to do so is by making some assumptions. A skeleton of a proof: axiom |- Nat is a type variable introduction x :: Nat |- x :: Nat proposition introduction x :: Nat, p(x) |- p(x) ... some proof using p(x) here ... x :: Nat, p(x) |- p(x+1) deduction x :: Nat |- p(x) => p(x+1) forall introduction |- forall x :: Nat, p(x) => p(x+1) ... some proof of p(0) here ... |- p(0) induction |- forall x :: Nat, p(x) Every proof by induction looks basically like this; you just need to fill in the "... some proof here..." parts. -- ryan

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