Inductive definitions and proofs
From Learning Logic for Computer Science
Induction is a principle in mathematics, which is used in definitions of sets and functions and in proofs. There are different variants of this principle. In mathematical logic, when it comes to syntax and semantics of formal languages, one uses structural induction. In general, the principle is often applicable when objects are composed of elementary objects by successive applications of construction rules.
Contents
Inductive definitions of sets
To define a set by induction, there are two things to be done:
- A (small) set of base elements has to be given. They form the base set.
- A set of rules—so-called inductive rules—has to be given.
The set defined is the smallest set containing the base set and satisfying the inductive rules.
In the simplest form such a rule is of the form: If $x$ is an element of the set, then so is $f(x)$, where $f$ is some function.
Example The set of even numbers can be defined as follows.
Base elements:
- The number \(0\) is an element (even number).
Inductive rule:
- If \(x\) is an element (even number), then $x + 2$ is an element (even number).
In more complicated cases, a new element is constructed from more than just one element.
Example One way to model full binary trees is by using pairing. As a reminder: a full binary tree is a binary tree, in which every node has either zero or two children. For example, the expression $\langle \emptyset, \langle \emptyset, \emptyset\rangle\rangle$ would stand for a full binary tree with five nodes. Each $\emptyset$ corresponds to a leaf node and each $\langle \cdot, \cdot \rangle$ expression represents an internal node, thus the example tree has three leaves and two internal nodes, which results in the stated five nodes.
The set of all full binary trees can then be defined inductively.
Base elements:
- The empty set $\emptyset$ is an element (full binary tree).
Inductive rule:
- If $x$ and $y$ are elements (full binary trees), then $\langle x, y \rangle$ is an element (full binary tree).
Here is an example with two rules:
Example The set of all bit sequences can inductively be defined as follows.
Base elements:
- The empty set $\emptyset$ is a bit sequence.
Inductive rules:
- If $s$ is a bit sequence, then $\langle 0, s\rangle$ is a bit sequence.
- If $s$ is a bit sequence, then $\langle 1, s\rangle$ is a bit sequence.
The previous example is often phrased as follows.
Example The set of all bit sequences can inductively be defined as follows.
Base elements:
- The empty set $\emptyset$ is a bit sequence.
Inductive rule:
- If $s$ is a bit sequence and $b \in \{0,1\}$, then $\langle b, s\rangle$ is a bit sequence.
So two induction rules are merged into one induction rule by introducing a parameter.
Here is one more example of this type, with an infinite number of parameters:
Example The set of lists of natural numbers can be defined as follows.
Base elements:
- The empty set is a base element.
Inductive rule:
- If \(l\) is a list of natural numbers and \(n\) is a natural number, then \(\langle n, l\rangle\) is a list of natural numbers.
So \(\langle 3, \emptyset \rangle\) and \(\langle 3, \langle 4, \emptyset \rangle\rangle\) are lists of natural numbers, but \(\langle 3, 2\rangle\) ist not.
Observe that if, in the above definition, the base elements are \(\emptyset\) and \(\langle 42, \emptyset \rangle\), the same set is obtained.
Unambiguous set definitions
An inductive definition of a set \(S\) is unambiguous if every element can only be constructed in exactly one way from base elements using inductive rules.
Example The first definition of the set of lists of natural numbers is unique, provided $\emptyset$ is not a pair, what is generally assumed.
The reason is: First, the only base element, \(\emptyset\), is not obtained by applying the only inductive rule. Second, if we have a non-base element, then there is only one way to write it as \(\langle m, l\rangle\). This is a defining property of \(\langle \cdot, \cdot \rangle\).
This need not always be the case. Here is an artifical example that explains that.
Example The second definition of the set of lists of natural numbers, where $\langle 42, \emptyset\rangle$ is given as a base element, is not unique.
The reason is that $\langle 42, \emptyset\rangle$ can be obtained by applying the induction rule to \(\emptyset\) (with 42 as a parameter) and $\langle 42, \emptyset\rangle$ is a base element—so the element can be obtained in two ways.
Inductive definitions of functions
If a set is defined by an unambiguous inductive definition, then one can use the induction principle to define functions on this set. To carry out such a definition, every base element needs to be mapped to an element—base mapping—and for every inductive rule in the set definition there must be a corresponding inductive rule in the function definition.
Example The length of a list of natural numbers can be defined by induction, when we assume the set is defined by the first inductive definition given above, which is unambiguous.
Formally, we define a function \(\text{length} \colon L \to \mathbf N\) where $L$ denotes the set of all lists of natural numbers.
Base mapping:
- \(\text{length}(\emptyset) = 0\).
Inductive rule:
- If \(l\) is a list of natural numbers and \(a \in \mathbf N\), then \(\text{length}(\langle a, l\rangle) = \text{length}(l) + 1\).
Here is another example along the same lines.
Example The set of elements occurring in a list of natural numbers can be defined by induction, when we assume the set is defined by the first inductive definition given above, which is unambiguous.
Formally, we define a function \(\text{elems} \colon L \to \wp(\mathbf N)\) where $L$ denotes the set of all lists of natural numbers.
Base mapping:
- \(\text{elems}(\emptyset) = \emptyset\).
Inductive rule:
- If \(l \in L\) and \(a \in \mathbf N\), then \(\text{elems}(\langle a, l\rangle) = \text{elems}(l) \cup \{a\}\).
Inductive proofs
If a set is defined using the induction principle, one can easily prove that properties hold for all elements of this set. To this end, one shows that the property holds for the base elements and that it is preserved by the inductive rules.
The second step is somewhat more complicated: one assumes that the property holds for some elements; one then shows that the property holds for the elements obtained by applying inductive rules.
Example A very simple example is the claim that every even number is divisible by $2$.
Base cases: For the only base element, $0$, we have $0 = 0 \times 2$.
Indutive step: Assume $x$ is even and divisible by two. (To show: $x + 2$ is divisible by $2$.) Since $x$ is divisible by $2$ there is some $a$ such that $a \times 2 = x$. We obtain $(a+1) \times 2 = a \times 2 + 2 = x+2$, which proves the claim.
Here is a more complicated example.
Example Obviously, the number of natural numbers in a list of natural numbers is at most the length of the list. Formally, this means $\lvert\text{elems}(l)\rvert \leq \text{length}(l)$ for every list $l$ of natural numbers.
We prove this by induction.
Base cases: $\emptyset$ is the only base element. Then: \begin{array}{rcll} \lvert\text{elems}(\emptyset)\rvert & = & \lvert\emptyset\rvert & \text{definition of elems}\\ & = & 0 & \text{property of }\emptyset\\ & = & \text{length}(\emptyset) & \text{definition of length} \end{array}
Inductive step: Assume $l$ is a list of natural numbers, $a$ is a natural number, and \(\lvert\text{elems}(l)\rvert \leq \text{length}(l)\). Then: \begin{array}{rcll} \lvert\text{elems}(\langle a, l\rangle)\rvert & = & \lvert\text{elems}(l) \cup \{a\}\rvert & \text{definition of elems}\\ & \leq & \lvert\text{elems}(l)\rvert + 1 & \text{property of } \cup\\ & \leq & \text{length}(l) + 1 & \text{inductive assumption}\\ & = & \text{length}(\langle a, l\rangle) & \text{definition of length} \end{array}