helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 3 page 2

Sum of the First n Natural Numbers

We will show that   1+...+n   equals   n(n+1)/2   .

We want to prove
( N  : Nat  ) sum(N) + sum(N) = N * (s N) .
We use induction on N to prove this goal. For this, we use the induction scheme based on the signature { 0, s } for Nat. Induction requires that we do the following:
  1. Base case: prove the assertion for N = 0 .
  2. Induction case: assume the assertion for N = N0 , and then prove it for N = s N0 .


This is the most typical kind of induction. The main point worth remarking upon is that this proof needs several lemmas about the natural numbers. Two of these are the associative and commutative laws for addition, which are in this case already included in the specification, in the form of so-called attributes of the addition operation. A third lemma is a kind of "distributive law" between the successor operation and multiplication, and it too is already included in the specification. Since this is just an expository example, this is justified by the great familiarity and general utility of these laws, but in general, lemmas should of course be proved before they are used.

Another point is that we do not prove

1+ 2+ ... + n = n(n+1)/2
but instead we prove the equivalent formula
sum(n) + sum(n) = n(n+1)
where sum(n) = 1+ 2+ ... + n. The recursively defined operation sum is of course needed to make precise the informal notation 1+ 2+ ... + n, and the reformulation in terms of sum + sum is in order to avoid introducing the division operation.

BOBJ proof scoreLeft    Up    Down    Right   

       This page was generated by Kumo on Tue Feb 13 17:31:26 PST 2001.