On 5/8/08, Daniel Fischer
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