Let's go back to induction and wrap up our examination with the inductive case.. Here, we have a sentence $\forall k (P(k) \rightarrow P(\operatorname{succ}(k)))$. What we need to do then is to show for an arbitrary element, say $t$, that $P(t) \rightarrow P(\operatorname{succ}(t))$. So now, we are left with an implication that we need to come up with a proof for. Then our inference rule says that we need to assume $P(t)$ and use that assumption to construct a proof for $P(\operatorname{succ}(t))$.
We can now put all of this together.
A common use for induction is for proving properties of sums or sequences of integers. The following is a common example.
For every $n \in \mathbb N$, $\sum \limits_{i=0}^n i = \frac{n(n+1)}2$.
If you've been taught this formula before, then you've probably been told the story of Gauss solving this problem when he was a child—a story which has been embellished over the last century and a half. However, his teachers in this story, in assigning $n = 100$, gave him an easy out since he only needed to consider one instance of the problem, so his solution does not use induction. We don't have that luxury, since we want to prove that this formula holds for all $n$.
We will prove this by induction on $n$.
Base case. If $n = 0$, then $\sum \limits_{i=0}^0 i = 0$ and $\frac{0 \cdot (0+1)}2 = 0$. Therefore, $\sum \limits_{i=0}^n i = \frac{n(n+1)}2$ holds for $n = 0$.
Inductive case. Let $k \in \mathbb N$ be arbitrary and assume that $\sum \limits_{i=0}^k i = \frac{k(k+1)}2$. We will show that $\sum \limits_{i=0}^{k+1} i = \frac{(k+1)(k+2)}2$. Then, we have the following: \begin{align*} \sum_{i=0}^{k+1} i &= \sum_{i=0}^k i + (k+1) \\ &= \frac{k(k+1)}2 + (k+1) & \text{by ind. hyp.} \\ &= (k+1) \cdot \left(\frac k 2 + 1 \right) \\ &= (k+1) \cdot \left(\frac k 2 + \frac 2 2 \right) \\ &= \frac{(k+1)(k+2)}2 \end{align*}
Thus, $\sum \limits_{i=0}^n i = \frac{n(n+1)}2$ holds for $n = k+1$. Therefore, $\sum \limits_{i=0}^n i = \frac{n(n+1)}2$ holds for all $n \in \mathbb N$.
Notice that even though we were proving a fact about a series, we were really performing induction on the structure of the natural numbers. This is typically how induction is learned—as a property of the natural numbers. But recall that the structure of the proof mirrors the structure of the recursive definition of the natural numbers. This suggests that induction can be applied to other recursive structures, beyond just the natural numbers.
Now, we'll take a trip back to grade school and think about division again. When we divide two integers, we may not get an integer as a result. That is, the integers may not divide evenly. So we either give up or keep working with the rational number that we get.
However, there is a way to define a notion of division for integers that produces integers in a meaningful way. Recall that if we divide two numbers $a$ by $b$, if $a$ is a multiple of $b$ (if $b \mid a$), we get an integer $q$ which we call the quotient. But if $a$ isn't a multiple of $b$, we get a remainder $r$.
The following theorem, the Division Theorem, formally states that whenever we divide two numbers $a$ and $b$, we will always be able to "get" the integers $q$ and $r$ (they exist) and that they're unique (that when we do division we always get the same answer).
For all integers $n$ and $d \gt 0$, there exist unique integers $q$ and $r$ such that $n = d \cdot q + r$ and $0 \leq r \lt d$.
What might this theorem look like in first-order logic? \[\forall n,d (d \gt 0 \rightarrow \exists q,r (n = d \cdot q + r \wedge 0 \leq r \wedge r \lt d)).\] Here's an example of how to express the idea that you only want to consider certain elements of the domain. Many mathematicians would write something like $\forall n, d \gt 0$ as shorthand, but here, we write more formally that we consider all $n$ and $d$ and condition the rest of the statement on $d \gt 0$. This is exactly what we're saying when we say "for all integers $d \gt 0$", that we really care about integers $d$ if they are greater than 0.
Now, this is not quite what we want since we only state that $q$ and $r$ exist. How do we express the idea that they are unique—that they're the only elements in our domain for which this property holds?
Suppose we have $P(x)$ and we want to argue that there is only one element for which $P(x)$ holds. We may jump to trying to show that this has to be the case, but that's not where we're headed yet. All we want to do is express this idea.
One way to think about this is to consider the question of what happens if there is an element, say $y$, such that $P(y)$ holds. Well, if $x$ is really unique, then it has to be the case that $y$ is really $x$. So our expression looks like the following: \[\exists x (P(x) \wedge \forall y (P(y) \rightarrow x = y)).\]
This says that there exists an element $x$ such that $P(x)$ holds and if $P(y)$ holds for any $y$, it must be the case that $x = y$.
This means that to prove this theorem, we can break it down into two steps:
So first, we need to show that these integers exist. This means we need to exhibit such integers. The obvious way to do this is to show how to find them. We will devise an algorithm for computing $q$ and $r$. Such a proof is also called a constructive proof, since we show how to "construct" the object we're trying to prove exists.
First, we'll need the following definition.
The function $\operatorname{divmod} : \mathbb N \times \mathbb N \rightarrow \mathbb N \times \mathbb N$ is defined inductively on $n$ by: \begin{align*} \operatorname{divmod}(0,d) &= (0,0) \\ \operatorname{divmod}(n+1,d) &= \begin{cases} (q', r' + 1) & \text{if $r'+1 \neq d$, where $(q',r') = \operatorname{divmod}(n,d)$,} \\ (q' + 1, 0) & \text{otherwise.} \end{cases} \end{align*}
This looks complicated, but we can easily turn it into a fairly simple function:
def divmod(n: int, d: int) -> tuple[int,int]:
if n == 0:
return (0,0)
else:
(q1,r1) = divmod(n-1,d)
if r1 + 1 != d:
return (q1, r1 + 1)
else:
return (q1 + 1, 0)We can try to trace through the code here to see what is being computed. Observe that in the recursive case, $n$ ever only decreases by one and both $q$ and $r$ increase by one. So what's going on here? Basically, this algorithm counts down from $n$, increasing the remainder counter $r$. If $r$ ever hits $d$, we know that we've counted a multiple of $d$, so we increase our quotient counter $q$ by one and reset $r$ to 0.
Note that divmod is a built-in function. Helpfully, the Python documentation tells us that the result of divmod(n,d) is supposed to be (n // d, n % d), which is what we want. Of course, the difficult part is proving that this is the case. Like many algorithms you'll prove correctness for in the future, this will be done by induction.
For all natural numbers $n$ and $d$, if $\operatorname{divmod}(n,d) = (q,r)$, then $n = q \cdot d + r$ with $d \neq 0$ and $r \lt d$.
We will prove this by induction on $n$. Let $d$ be an arbitrary nonzero natural number.
Base case. Let $n = 0$. By definition, we have $\operatorname{divmod}(0,d) = (0,0)$. Then we have $0 = 0 \cdot d + 0$ and $d \gt 0 = r$.
Inductive case. Let $k$ be an arbitrary natural number. Assume that if $\operatorname{divmod}(k,d) = (q',r')$, then $k = q' \cdot d + r'$ with $r' \lt d$. We will consider $n = k+1$. Note that we have two cases to deal with: when $r'+1 \neq d$ and when it doesn't.
First, we consider the case when $r'+1 \neq d$. In this case, we have $(q,r) = (q',r'+1)$ by definition. This gives us: \begin{align*} q \cdot d + r &= q' \cdot d +(r' + 1) &\text{definition} \\ &= k+1 &\text{ind. hyp.} \end{align*} so this case holds for $k+1$. Now, we need to show that $r \lt d$. Since $r = r' + 1 \neq d$ by our assumption and $r' \lt d$ by our inductive hypothesis, we can conclude that $r \lt d$.
Our second case is when $r'+1 = d$, so we have $(q,r) = (q'+1,0)$ by definition. We then have: \begin{align*} q \cdot d + r &= (q'+1) \cdot d + 0 &\text{definition} \\ &= q' \cdot d + d \\ &= q' \cdot d + (r' + 1) &\text{assumption} \\ &= k + 1 &\text{ind. hyp.} \end{align*} and so this case also holds for $k+1$. And since $r = 0$, we have $r \lt d$.
We've now shown that $k+1 = q \cdot d + r$ with $r \lt d$ if $(q,r) = \operatorname{divmod}(k+1,d)$ and therefore, this must hold for all $n \in \mathbb N$.
This gets us almost all the way there, except that we've only defined $\operatorname{divmod}$ on $\mathbb N$. Since the claim of the Division Theorem is for integers, we will need to somehow extend our definition to $\mathbb Z$.
To see how to do this, we consider an integer $n$ that isn't a natural number. Then $-n$ is a natural number and we have that $-n = q \cdot d + r$ by what we've just proved. This gives us $n = -q \cdot d - r$. Now, we need to make the remainder a positive integer between $0$ and $d$. We can do this simply by adding $d$ to it: \[-q \cdot d - r = (-q-1) \cdot d + (d-r).\] So we have for $n \lt 0$ that $\operatorname{divmod}(n,d) = (-q-1, d-r)$ where $-n = q \cdot d + r$.