MCS discusses induction in chapter 5. This text is intended to supplement, not replace, that text.

1 The idea, programmer’s version

Suppose I have a loop that iterates over some list. How do I know what the results will be after the loop is over? The most common reasoning goes like this:

1. I know what’s true before the loop starts
2. I know it stays true each pass through the loop
   1. because it starts true
   2. and one step of the loop does not make it false
3. So I know it must be true at the end

This outline may make intuitive sense, but we need to formalize it to make it into a proof strategy.

1. We need some starting place. We call that the base case. It can be as complicated as we need, though often it will be quite simple.

2. We need some loop-like way of getting from one truth to the next. We call that the inductive step. It generally works as follows

   1. we assume it starts true; this assumption is called the inductive hypothesis
   2. we use that assumption to prove that it will still be true one step later

3. We conclude it must always be true. This step is not a proof, it’s a rule called the principle of induction.

2 The idea, formal logic version

The principle of induction is a proof rule that looks like:

\begin{aligned} &P(0)\\ &P(n) \rightarrow P(n+1)\\ \therefore\;&\forall x \in \mathbb N \;.\; P(x) \end{aligned}

Thus, to use it, we first prove P(0); then prove P(n) \rightarrow P(n+1) by assuming P(n) and proving P(n+1); then state that by the principle of induction, \forall x \in \mathbb N \;.\; P(x).

In this approach first prove P(0) is called the base case; then prove P(n) \rightarrow P(n+1) is called the inductive step; and by assuming P(n) is called the inductive hypothesis.

What if your base case is more involved than P(0)? The formal answer is define a different P

Although we can convert arbitrary induction into a formal variation, we won’t in this class or anywhere else outside of formal logic.

3 Examples

double babylonian(double x) {
    double y = 1;
    for(int i=0; i<20; i+=1) {
        y = (y + x/y)/2;
    }
    return y;
}

def babylonian(x):
    y = 1
    for i in range(20):
      y = (y + x/y)/2
    return y