Induction

Source file content/methods/induction/induction.tex

Source file content/methods/induction/introduction.tex

Introduction

Induction is an important proof technique which is used, in different forms, in almost all areas of logic, theoretical computer science, and mathematics. It is needed to prove many of the results in logic.

Induction is often contrasted with deduction, and characterized as the inference from the particular to the general. For instance, if we observe many green emeralds, and nothing that we would call an emerald that's not green, we might conclude that all emeralds are green. This is an inductive inference, in that it proceeds from many particular cases (this emerald is green, that emerald is green, etc.) to a general claim (all emeralds are green). Mathematical induction is also an inference that concludes a general claim, but it is of a very different kind than this “simple induction.”

Very roughly, an inductive proof in mathematics concludes that all mathematical objects of a certain sort have a certain property. In the simplest case, the mathematical objects an inductive proof is concerned with are natural numbers. In that case an inductive proof is used to establish that all natural numbers have some property, and it does this by showing that

1. $0$source has the property, and

2. whenever a number $k$source has the property, so does $k+1$source.

Induction on natural numbers can then also often be used to prove general claims about mathematical objects that can be assigned numbers. For instance, finite sets each have a finite number $n$source of elements, and if we can use induction to show that every number $n$source has the property “all finite sets of size $n$source are dots” then we will have shown something about all finite sets.

Induction can also be generalized to mathematical objects that are inductively defined. For instance, expressions of a formal language such as those of first-order logic are defined inductively. Structural induction is a way to prove results about all such expressions. Structural induction, in particular, is very useful---and widely used---in logic.

Source file content/methods/induction/induction-on-N.tex

Induction on $\Nat$source

In its simplest form, induction is a technique used to prove results for all natural numbers. It uses the fact that by starting from $0$source and repeatedly adding $1$source we eventually reach every natural number. So to prove that something is true for every number, we can (1) establish that it is true for $0$source and (2) show that whenever it is true for a number $n$source, it is also true for the next number $n+1$source. If we abbreviate “number $n$source has property $P$source” by $P(n)$source (and “number $k$source has property $P$source” by $P(k)$source, etc.), then a proof by induction that $P(n)$source for all $n \in \Nat$source consists of:

1. a proof of $P(0)$source, and

2. a proof that, for any $k$source, if $P(k)$source then $P(k+1)$source.

To make this crystal clear, suppose we have both (1) and (2). Then (1) tells us that $P(0)$source is true. If we also have (2), we know in particular that if $P(0)$source then $P(0+1)$source, i.e., $P(1)$source. This follows from the general statement “for any $k$source, if $P(k)$source then $P(k+1)$source” by putting $0$source for $k$source. So by modus ponens, we have that $P(1)$source. From (2) again, now taking $1$source for $n$source, we have: if $P(1)$source then $P(2)$source. Since we've just established $P(1)$source, by modus ponens, we have $P(2)$source. And so on. For any number $n$source, after doing this $n$source times, we eventually arrive at $P(n)$source. So (1) and (2) together establish $P(n)$source for any $n \in \Nat$source.

Let's look at an example. Suppose we want to find out how many different sums we can throw with $n$source dice. Although it might seem silly, let's start with $0$source dice. If you have no dice there's only one possible sum you can “throw”: no dots at all, which sums to $0$source. So the number of different possible throws is $1$source. If you have only one die, i.e., $n=1$source, there are six possible values, $1$source through $6$source. With two dice, we can throw any sum from $2$source through $12$source, that's $11$source possibilities. With three dice, we can throw any number from $3$source to $18$source, i.e., $16$source different possibilities. $1$source, $6$source, $11$source, $16$source: looks like a pattern: maybe the answer is $5n+1$source? Of course, $5n+1$source is the maximum possible, because there are only $5n+1$source numbers between $n$source, the lowest value you can throw with $n$source dice (all $1$source's) and $6n$source, the highest you can throw (all $6$source's).

Very often we use induction when we want to prove something about a series of objects (numbers, sets, etc.) that is itself defined “inductively,” i.e., by defining the $(n+1)$source-st object in terms of the $n$source-th. For instance, we can define the sum $s_n$source of the natural numbers up to $n$source by

This definition gives:

Now we can prove, by induction, that $s_n = n(n+1)/2$source.

The important lesson here is that if you're proving something about some inductively defined sequence $a_n$source, induction is the obvious way to go. And even if it isn't (as in the case of the possibilities of dice throws), you can use induction if you can somehow relate the case for $k+1$source to the case for $k$source.

Source file content/methods/induction/strong-induction.tex

Strong Induction

In the principle of induction discussed above, we prove $P(0)$source and also if $P(k)$source, then $P(k+1)$source. In the second part, we assume that $P(k)$source is true and use this assumption to prove $P(k+1)$source. Equivalently, of course, we could assume $P(k-1)$source and use it to prove $P(k)$source---the important part is that we be able to carry out the inference from any number to its successor; that we can prove the claim in question for any number under the assumption it holds for its predecessor.

There is a variant of the principle of induction in which we don't just assume that the claim holds for the predecessor $k-1$source of $k$source, but for all numbers smaller than $k$source, and use this assumption to establish the claim for $k$source. This also gives us the claim $P(n)$source for all $n \in \Nat$source. For once we have established $P(0)$source, we have thereby established that $P$source holds for all numbers less than $1$source. And if we know that if $P(l)$source for all $l<k$source, then $P(k)$source, we know this in particular for $k=1$source. So we can conclude $P(1)$source. With this we have proved $P(0)$source and $P(1)$source, i.e., $P(l)$source for all $l<2$source, and since we have also the conditional, if $P(l)$source for all $l<2$source, then $P(2)$source, we can conclude $P(2)$source, and so on.

In fact, if we can establish the general conditional “for all $k$source, if $P(l)$source for all $l<k$source, then $P(k)$source,” we do not have to establish $P(0)$source anymore, since it follows from it. For remember that a general claim like “for all $l<k$source, $P(l)$source” is true if there are no $l<k$source. This is a case of vacuous quantification: “all $A$sources are $B$sources” is true if there are no $A$sources, $\lforall[x][(!A(x) \lif !B(x))]$source is true if no $x$source satisfies $!A(x)$source. In this case, the formalized version would be “$\lforall[l][(l < k \lif P(l))]$source”---and that is true if there are no $l < k$source. And if $k=0$source that's exactly the case: no $l<0$source, hence “for all $l<0$source, $P(0)$source” is true, whatever $P$source is. A proof of “if $P(l)$source for all $l<k$source, then $P(k)$source” thus automatically establishes $P(0)$source.

This variant is useful if establishing the claim for $k$source can't be made to just rely on the claim for $k-1$source but may require the assumption that it is true for one or more $l<k$source.

Source file content/methods/induction/inductive-definitions.tex

Inductive Definitions

In logic we very often define kinds of objects inductively, i.e., by specifying rules for what counts as an object of the kind to be defined which explain how to get new objects of that kind from old objects of that kind. For instance, we often define special kinds of sequences of symbols, such as the terms and formulas of a language, by induction. For a simple example, consider strings consisting of letters $\mathrm{a}$source, $\mathrm{b}$source, $\mathrm{c}$source, $\mathrm{d}$source, the symbol $\circ$source, and brackets $[$source and $]$source, such as “$[[\mathrm{c} \circ \mathrm{d}][$source”, “$[\mathrm{a}[]\circ]$source”, “$\mathrm{a}$source” or “$[[\mathrm{a} \circ \mathrm{b}]\circ \mathrm{d}]$source”. You probably feel that there's something “wrong” with the first two strings: the brackets don't “balance” at all in the first, and you might feel that the “$\circ$source” should “connect” expressions that themselves make sense. The third and fourth string look better: for every “$[$source” there's a closing “$]$source” (if there are any at all), and for any $\circ$source we can find “nice” expressions on either side, surrounded by a pair of parentheses.

We would like to precisely specify what counts as a “nice term.” First of all, every letter by itself is nice. Anything that's not just a letter by itself should be of the form “$[t \circ s]$source” where $s$source and $t$source are themselves nice. Conversely, if $t$source and $s$source are nice, then we can form a new nice term by putting a $\circ$source between them and surround them by a pair of brackets. We might use these operations to define the set of nice terms. This is an inductive definition.

This definition tells us that something counts as a nice term iff it can be constructed according to the two conditions (1) and (2) in some finite number of steps. In the first step, we construct all nice terms just consisting of letters by themselves, i.e.,

In the second step, we apply (2) to the terms we've constructed. We'll get

for all combinations of two letters. In the third step, we apply (2) again, to any two nice terms we've constructed so far. We get new nice term such as $[\mathrm{a} \circ [\mathrm{a} \circ \mathrm{a}]]$source---where $t$source is $\mathrm{a}$source from step 1 and $s$source is $[\mathrm{a} \circ \mathrm{a}]$source from step 2---and $[[\mathrm{b} \circ \mathrm{c}] \circ [\mathrm{d} \circ \mathrm{b}]]$source constructed out of the two terms $[\mathrm{b} \circ \mathrm{c}]$source and $[\mathrm{d} \circ \mathrm{b}]$source from step 2. And so on. Clause (3) rules out that anything not constructed in this way sneaks into the set of nice terms.

Note that we have not yet proved that every sequence of symbols that “feels” nice is nice according to this definition. However, it should be clear that everything we can construct does in fact “feel nice”: brackets are balanced, and $\circ$source connects parts that are themselves nice.

The key feature of inductive definitions is that if you want to prove something about all nice terms, the definition tells you which cases you must consider. For instance, if you are told that $t$source is a nice term, the inductive definition tells you what $t$source can look like: $t$source can be a letter, or it can be $[s_1 \circ s_2]$source for some pair of nice terms $s_1$source and $s_2$source. Because of clause (3), those are the only possibilities.

When proving claims about all of an inductively defined set, the strong form of induction becomes particularly important. For instance, suppose we want to prove that for every nice term of length $n$source, the number of $[$source in it is $< n/2$source. This can be seen as a claim about all $n$source: for every $n$source, the number of $[$source in any nice term of length $n$source is $< n/2$source.

Source file content/methods/induction/structural-induction.tex

Structural Induction

So far we have used induction to establish results about all natural numbers. But a corresponding principle can be used directly to prove results about all elements of an inductively defined set. This often called structural induction, because it depends on the structure of the inductively defined objects.

Generally, an inductive definition is given by (a) a list of “initial” elements of the set and (b) a list of operations which produce new elements of the set from old ones. In the case of nice terms, for instance, the initial objects are the letters. We only have one operation: the operations are

You can even think of the natural numbers $\Nat$source themselves as being given by an inductive definition: the initial object is $0$source, and the operation is the successor function $x + 1$source.

In order to prove something about all elements of an inductively defined set, i.e., that every element of the set has a property $P$source, we must:

1. Prove that the initial objects have $P$source

2. Prove that for each operation $o$source, if the arguments have $P$source, so does the result.

For instance, in order to prove something about all nice terms, we would prove that it is true about all letters, and that it is true about $[s_1 \circ s_2]$source provided it is true of $s_1$source and $s_2$source individually.

Let's give another proof by structural induction: a proper initial segment of a string $t$source of symbols is any string $s$source that agrees with $t$source symbol by symbol, read from the left, but $t$source is longer. So, e.g., $[a \circ {}$source is a proper initial segment of $[a \circ b]$source, but neither are $[b \circ {}$source (they disagree at the second symbol) nor $[a \circ b]$source (they are the same length).

Source file content/methods/induction/relations.tex

Relations and Functions

When we have defined a set of objects (such as the natural numbers or the nice terms) inductively, we can also define relations on these objects by induction. For instance, consider the following idea: a nice term $t_1$source is a subterm of a nice term $t_2$source if it occurs as a part of it. Let's use a symbol for it: $t_1 \sqsubseteq t_2$source. Every nice term is a subterm of itself, of course: $t \sqsubseteq t$source. We can give an inductive definition of this relation as follows:

This definition, for instance, will tell us that $\mathrm{a} \sqsubseteq [\mathrm{b} \circ \mathrm{a}]$source. For (2) says that $\mathrm{a} \sqsubseteq [\mathrm{b} \circ \mathrm{a}]$source iff $\mathrm{a} = [\mathrm{b} \circ \mathrm{a}]$source, or $\mathrm{a} \sqsubseteq b$source, or $\mathrm{a} \sqsubseteq \mathrm{a}$source. The first two are false: $\mathrm{a}$source clearly isn't identical to $[\mathrm{b} \circ \mathrm{a}]$source, and by (1), $\mathrm{a} \sqsubseteq \mathrm{b}$source iff $\mathrm{a} = \mathrm{b}$source, which is also false. However, also by (1), $\mathrm{a} \sqsubseteq \mathrm{a}$source iff $\mathrm{a} = \mathrm{a}$source, which is true.

It's important to note that the success of this definition depends on a fact that we haven't proved yet: every nice term $t$source is either a letter by itself, or there are uniquely determined nice terms $s_1$source and $s_2$source such that $t = [s_1 \circ s_2]$source. “Uniquely determined” here means that if $t = [s_1 \circ s_2]$source it isn't also $= [r_1 \circ r_2]$source with $s_1 \neq r_1$source or $s_2 \neq r_2$source. If this were the case, then clause (2) may come in conflict with itself: reading $t_2$source as $[s_1 \circ s_2]$source we might get $t_1 \sqsubseteq t_2$source, but if we read $t_2$source as $[r_1 \circ r_2]$source we might get not $t_1 \sqsubseteq t_2$source. Before we prove that this can't happen, let's look at an example where it can happen.

Bracketless terms are, e.g., $\mathrm{a}$source, $\mathrm{b} \circ \mathrm{d}$source, $\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}$source. Now if we defined “subterm” for bracketless terms the way we did above, the second clause would read

Now $\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}$source is of the form $s_1 \circ s_2$source with

Now is $\mathrm{a} \circ \mathrm{b}$source a subterm of $\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}$source? The answer is yes if we go by the first reading, and no if we go by the second.

The property that the way a nice term is built up from other nice terms is unique is called unique readability. Since inductive definitions of relations for such inductively defined objects are important, we have to prove that it holds.

We can also define functions inductively: e.g., we can define the function $f$source that maps any nice term to the maximum depth of nested $[\dots]$source in it as follows:

For instance

Here, of course, we assume that $s_1$source an $s_2$source are nice terms, and make use of the fact that every nice term is either a letter or of the form $[s_1 \circ s_2]$source. It is again important that it can be of this form in only one way. To see why, consider again the bracketless terms we defined earlier. The corresponding “definition” would be:

Now consider the bracketless term $\mathrm{a} \circ \mathrm{b} \circ \mathrm{c} \circ \mathrm{d}$source. It can be read in more than one way, e.g., as $s_1 \circ s_2$source with

Calculating $g$source according to the first way of reading it would give

But a function must always yield a unique value; so our “definition” of $g$source doesn't define a function at all.