2.4 Induction

---

2.4 Induction

Proofs by induction are ubiquitous in the theory of programming languages, as in most of computer science. Many of these proofs are based on one of the following principles.

2.4.1 Axiom [Principle of Ordinary Induction on Natural Numbers]

Suppose that P is a predicate on the natural numbers. Then:

• If P(0)

• and, for all i, P(i) implies P(i + 1),

• then P(n) holds for all n.

2.4.2 Axiom [Principle of Complete Induction on Natural Numbers]

Suppose that P is a predicate on the natural numbers. Then:

• If, for each natural number n,

  • given P(i) for all i < n

  • we can show P(n),

• then P(n) holds for all n.

2.4.3 Definition

The lexicographic order (or "dictionary order") on pairs of natural numbers is defined as follows: (m, n) ≤ (m′, n′) iff either m < m′ or else m = m′ and n ≤ n′.

2.4.4 Axiom [Principle of Lexicographic Induction]

Suppose that P is a predicate on pairs of natural numbers.

• If, for each pair (m, n) of natural numbers,

  • given P(m′, n′) for all (m′, n′) < (m, n)

  • we can show P(m, n),

• then P(m, n) holds for all m, n.

The lexicograpic induction principle is the basis for proofs by nested induction, where some case of an inductive proof proceeds "by an inner induction." It can be generalized to lexicographic induction on triples of numbers, 4-tuples, etc. (Induction on pairs is fairly common; on triples it is occasionally useful; beyond triples it is rare.)

Theorem 3.3.4 in Chapter 3 will introduce yet another format for proofs by induction, called structural induction, that is particularly useful for proofs about tree structures such as terms or typing derivations. The mathematical foundations of inductive reasoning will be considered in more detail in Chapter 21, where we will see that all these specific induction principles are instances of a single deeper idea.

---