. 83
( 107 .)


Proof: The proof is by the formalized version of mathematical in-
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
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.

Section 16.4
458 / Mathematical Induction


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) {
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;
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
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

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;
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


. 83
( 107 .)