duction. The predicate Q(x) in question is (x + 1 = 1 + x). We need

to prove the basis case, Q(0), and the induction step

∀x (Q(x) ’ Q(x + 1))

The basis case requires us to prove that 0 + 1 = 1 + 0. By axiom 3,

0 + 1 = 1. By axiom 4, 1 + 0 = 1. Hence, 0 + 1 = 1 + 0, as desired.

We now prove the induction step. The proof is by general conditional

proof. Let n be any number such that Q(n). This is our inductive

hypothesis. Using it, we need to prove Q(n + 1). That is, our induc-

tion hypothesis is that n + 1 = 1 + n and our goal is to prove that

(n + 1) + 1 = 1 + (n + 1). This takes two steps, as follows:

(n + 1) + 1 = (1 + n) + 1 by the inductive hypothesis.

= 1 + (n + 1) by axiom 5.

Using this, one can go on to prove that addition is commutative, and so on.

There are, however, truths about the natural numbers that cannot be proven G¨del Incompleteness

o

Theorem

from pa. Not only that, but any attempt to set down a list of ¬rst-order

axioms true of the natural numbers must, in some sense, fail. We will discuss

this result, known as the G¨del Incompleteness Theorem, in Chapter 19.

o

Section 16.4

458 / Mathematical Induction

Exercises

16.19 Use Fitch to give a formal proof of ∀x (x + 1 = 1 + x) from the Peano axioms. You will ¬nd

‚ the problem set up in the ¬le Exercise 16.19, which contains the four axioms you will need

as premises (including the appropriate instance of the induction scheme). Your proof should

parallel the informal proof given above.

Give informal proofs, similar in style to the one in the text, that the following statements are consequences

of pa. Explicitly identify any predicates to which you apply induction. When proving the later theorems,

you may assume the results of the earlier problems.

16.20 ∀x (0 + x = x) 16.21 ∀x (1 — x = x)

16.22 ∀x (0 — x = 0) 16.23 ∀x (x — 1 = 1 — x)

16.24 ∀x ∀y ∀z ((x + y) + z = x + (y + z)) [Hint: This is relatively easy, but you have to per-

form induction on z. That is, your basis case is to show that (x + y) + 0 = x + (y + 0).

You should then assume (x + y) + n = x + (y + n) as your inductive hypothesis and show

(x + y) + (n + 1) = x + (y + (n + 1)).]

16.25 ∀x ∀y (x + y = y + x)

16.26 ∀x ∀y (x — y = y — x) [Hint: To prove this, you will ¬rst need to prove the lemma

∀x ∀y ((x + 1) — y = (x — y) + y). Prove this by induction on y.]

Section 16.5

Proving programs correct

Induction is an important technique for proving facts about computer pro-

grams, particularly those that involve recursive de¬nitions or loops. Imagine

that we ask a programmer to write a program that adds the ¬rst n natural

numbers. The program, when given a natural number n as its input, should

return as its result the sum 0 + 1+ 2+ . . .+ n. We will call this the speci¬cation

program speci¬cation

of the program.

One way to do this is to write a so-called recursive program like this:

recursive program

Chapter 16

Proving programs correct / 459

public natural sumToRec(natural n) {

sumToRec

if(n == 0) return 0;

else return n + sumToRec(n ’ 1);

}

This program is written in an imaginary, Java-like language. We could para-

phrase what it says as follows. See if you can understand the program even if

you don™t know how to program.

The program de¬nes a function sumToRec that takes a natural num-

ber as argument and produces a natural number as result. Let n be a

natural number given as argument. If n is 0, then the result returned

is 0; otherwise the result is n plus the result returned by calling this

same function with argument n ’ 1.

It is pretty clear that this produces the right answer, but let™s see how

we would prove it using a simple inductive proof. The goal of the proof is to

show that the program meets its speci¬cation, that for any n, sumToRec(n) =

0 + 1 + 2 + . . . + n.

Proof: The proof proceeds by induction. Basis: For our basis case

we need to show that sumToRec(0) = 0. But with argument 0, the

result returned by the program is 0, as required.

Induction: Suppose that the result returned by the program for ar-

gument k is correct, i.e., sumToRec(k) = 0 + 1 + 2 + . . . + k. We must

show that the result returned for k + 1 is also correct. Since k + 1

cannot be 0, the program is de¬ned to return sumToRec(k) + (k + 1)

in this case. By the inductive hypothesis

sumToRec(k) + (k + 1) = (0 + 1 + 2 + . . . + k) + (k + 1)

as required. This concludes our inductive proof.

Induction is also useful when the program contains loops rather than direct

recursive de¬nitions as in the program for sumToRec. But it is a bit less

obvious how induction applies in these cases. To see how, let™s look at another

implementation of the same function, one that uses a while loop: while loop

public natural sumUpTo(natural n) {

natural sum = 0;

sumUpTo

natural count = 0;

while(count < n) {

Section 16.5

460 / Mathematical Induction

count += 1;

sum += count;

}

return sum;

}

We could paraphrase this program in English in the following way.

The program de¬nes a function sumUpTo, whose arguments are nat-

ural numbers. Let n be a natural number that is input as argument.

Initialize the variables sum and count, also natural numbers, both

to be 0. Then, so long as the value of count is less than n, repeat

the following two steps: increase count by 1 and then add count to

sum. When ¬nished with the loop, return the value of sum.

How would we prove that this new program meets the speci¬cation? A

complete proof requires that we spell out a precise semantics for each pro-

gramming construct in our programming language. Fortunately, the program

above uses only three constructions.

—¦ Simple assignment. An example of a simple assignment is the statement

sum = 0. After executing such a statement we know that the value of

the program variable on the left of the assignment (sum) has the value

on the right of the assignment (0).

—¦ Additive assignment. An example is the statement sum += count. After

executing such a statement the value of the program variable on the left

(sum) is increased by the value of the variable on the right (count).

—¦ While loop. A while loop repeats the statements in the body of the loop

(in the example, the statements sum += count and count += 1) until

the test condition governing the loop (count < n) becomes false. Then

execution resumes with the statement after the while loop.

To prove that our program meets the speci¬cation, we will give two inductive

proving correctness

of sumUpTo arguments. The ¬rst will show that on input n, the body of the loop is executed

exactly n times. The second will demonstrate that a certain invariant holds

of the loop, namely, that after n loops, the value of sum is 0 + 1 + 2 + . . . + n.

Putting these together gives us the result we need.

To prove the ¬rst claim, we will prove something stronger: that for any

k, if the test at the while loop is reached with the value of n ’ count equal

to k, then the loop will execute exactly k more times. This will prove the

Chapter 16

Proving programs correct / 461

claim, since the ¬rst time the test is reached, count has the value 0, and so

n ’ count = n. We prove the claim by induction on k, that is, on the quantity

n ’ count.

Proof: Basis: Suppose that n ’ count is 0 when the test is reached.

Then n = count and therefore the test is false. The body of the loop

is not executed again. So when n ’ count is 0 the loop is executed 0

more times, as required.

Induction: Our inductive hypothesis is that if the test is reached with

n ’ count = k then the loop executes k more times. We must show

that if the test is reached with n ’ count = k + 1, then the loop will

execute k + 1 more times. Suppose that n ’ count = k + 1. The test

in the while loop is therefore true, since n ’ count is positive and so

count < n. So the body of the loop will execute, and this will result

(in part) in count increasing by 1. So when the test is next reached,

after one execution of the body, n ’ count = k. This will result in k

more executions of the loop, by the induction hypothesis. So in all,

the body of the loop will execute k + 1 times, as required.

We now know that the program above is guaranteed to terminate, whatever

value of n is passed in as its argument, and that it will execute the loop exactly

n times.

Now we turn our attention to proving that when the program terminates,

the value in the variable sum is the sum of the ¬rst n natural numbers. We

again prove something slightly stronger, namely, that after k iterations of the

while loop, the value of the variables sum and count are given by the following

formula:

sum = (0 + 1 + 2 + . . . + k) § count = k

This is called an invariant for the loop. It describes in essence how the program invariant

works: sum accumulates the sum of the initial segment of natural numbers,

increasing by one element each iteration, while count records the number of

iterations that have been completed.

Proof: Basis: When k = 0, we have performed 0 iterations of the

while loop. At this point sum = 0 and count = 0, and so the formula

is obviously true.

Induction: We assume that the formula holds after k iterations of

the body of the loop, and must show that it holds again after k + 1

iterations of the loop. Let sum be the value of sum after k iterations

of the loop, and sum be the value of sum after k + 1 iterations.

Similarly for count.

Section 16.5

462 / Mathematical Induction

Then

sum = (0 + 1 + 2 + . . . + count)

by the inductive hypothesis. After k +1 iterations, the value of count

is increased by 1 and sum is increased by count (since the loop

increments count before sum), and so we have:

sum = sum + count

= sum + (count + 1)

= 0 + 1 + 2 + . . . + count + (count + 1)

= 0 + 1 + 2 + . . . + k + (k + 1)

This concludes our induction.

Finally, we know that when the condition on the loop becomes false, count

must equal n, and so at this point sum = 0 + 1 + 2 + . . . + count = 0 + 1 + 2 +

. . . + n. Since sum is the value returned, this shows that the program meets

the original speci¬cation.

A third implementation

Suppose that another programmer writes the following code and claims that

this new program also implements a function meeting our speci¬cation.

public natural sumDownFrom(natural n) {

natural sum = 0;

sumDownFrom

natural count = n;

while(count > 0) {

sum += count;

count ’= 1;

}

return sum;

}

We could paraphrase this program as follows:

Let n be a natural number. Initialize sum and count, also natural

numbers, to 0 and n respectively. Then, so long as count is greater