Mathematical Induction

When we have a Base case $P(0)$
and a recurrence implication $P(k) \implies P(k + 1)$,
we may show any $P(n)$ by applying the recurrence implication $n$ times (starting from the Base case).

I.e., $P(0) \implies P(1) \implies P(2) \implies \dots \implies P(n)$

Mathematical Induction “automates” this repeated implication chain.

---

Like all other methods of proof, Proof by Induction only works because we defined it to work.
Think about, e.g., in Propositional Logic, how Modus Ponens, while seemingly obvious, is defined as an axiom.

More generally,
the validity of some formula can be proven in an inductively (recursively) defined structure by proving the base case and the validity of a the defining recurrence relation as an implication.

I.e., in recursive structures, we can do recursive proofs.

Another way to think about this is that Induction is valid in structures that are, by definition, inductive.

Types

Weak / Ordinary

$$\forall P: \quad \frac{ P(0), \quad \forall k : \big( P(k) \implies P(k + 1) \big) }{ \forall n : P(n) }$$

Strong / Complete

The Induction Hypothesis is “stronger” here.
$$\forall P: \quad \frac{ P(0), \quad \forall k : \big( \forall j \le k : P(j) \implies P(k + 1) \big) }{ \forall n : P(n) }$$

Note that a Base case might not be necessary because the implication could be vacuously true for the “base” under certain constructions.

Structural

eh, just structural, yk.

Prefix

Skipping steps.
$$\forall P: \quad \frac{ P(0), \quad \forall k : \big( P(k) \implies P(2k) \land P(2k + 1) \big) }{ \forall n : P(n) } \\[1.5em] \forall P: \quad \frac{ P(0), \quad \forall k : \big( P(\lfloor \sqrt{k} \rfloor) \implies P(k) \big) }{ \forall n : P(n) }$$

$n$-Step

Trivial variant of any of the above where instead of having 1 recurrence implication like $P(x) \implies P(x + 1)$, we have $n$ base cases and one (or up to $n$, should there require multiple cases) $P(x) \implies P(x + n)$.
Effectively, we splice up the domain into subsets and do induction on each.

There are many variations of this, but the idea is the same as any other induction:
we show $P(n)$ through implicit applications of a recurrence implication from a base case… except that there may be more than one “path” (the starting base case and the implication used), depending on $n$ (e.g., 2 cases for even and odd $n$).

Sometimes formulations “between” weak and strong induction (i.e., $P(k)$ requires all $P(k - 1), P(k-2), \dots, P(k-n)$ for some fixed $n$) is also called $n$-step induction.

Infinite Descent

This is not a form of induction (but of by contradiction), but it is similar and has equivalent inductive forms.
“Un-induction”.

$$\forall P: \quad \frac{ \forall k : \big( P(k) \implies \exists j < k : P(j) \big) }{ \forall n : \lnot P(n) }$$

This works because a recursive structure has a “bottom” / “base” / “infimum” (e.g., 0 for $\N$), so a proof that assumes a “bottomless”, infinitely “descendible” structure is contradictory.

Note how the ideas here are very similar to the Well-Ordering Principle

---

Weak (ordinary) Induction, Strong (complete) Induction, Structural Induction, Prefix Induction, and the Well-Ordering Principle are all equivalent.

Common Inductions

To work with an arbitrary member $x \in \mathbb{D}$ means to work with $x$ without assuming it any properties that cannot be assumed for all members of $\mathbb{D}$.

Here we illustrate schemata of induction proofs for some common structures.

Natural Numbers – $\N$

Most commonly enjoys weak induction, but also works nicely with strong induction and infinite descent.

Definition of $\N$ as a recursive datatype NnI:
NnI = 0 | NnI + 1

Definition of $\N$ as the inductive set of nonnegative whole numbers:
$0 \in \N,$
$n \in \N \implies \text{succ}(n) \in \N$
where we designate $1 \coloneqq \text{succ}(0)$, $2 \coloneqq \text{succ}(1)$, etc.

Base case

$P(0)$

Induction Hypothesis

$P(k) \space$ for arbitrary $k \in \N$

Inductive Step

$P(k+1)$

As a Rule of Inference:
$$\frac{ P(0), \quad P(k) \implies P(k+1) }{ \forall n \in \N : P(n) } \quad (\text{for arbitrary $k$})$$

Lists – $\mathscr{L}$

Example of structural induction.

Definition of $\mathscr{L}$ as a recursive datatype List:
List = [] | x::List
($::$ denotes element prepending)

Definition of $\mathscr{L}$ as the inductive set of all lists:
$\!\texttt{[]}\! \in \mathscr{L},$
$\ell \in \mathscr{L} \implies \forall x : x\!::\!\!\texttt{[]}\! \in \mathscr{L}$¹

Base case

$P(\!\texttt{[]}\!)$

Induction Hypothesis

$P(l) \space$ for arbitrary $l \in \mathscr{L}$

Inductive Step

$\forall x : P(x\!::\!l)$¹

As a Rule of Inference:
$$\frac{ P(\!\texttt{[]}\!), \quad P(l) \implies P(x\!::\!l) }{ \forall \ell \in \mathscr{L} : P(\ell) } \quad (\text{for arbitrary $l$, $x$})$$

Binary Trees – $\mathbb{T}$

Also structural induction, like most CS-style datatypes.

Definition of $\mathbb{T}$ as a recursive datatype Tree:
Tree = Null | Node x [Tree,Tree]

Definition of $\mathbb{T}$ as the inductive set of all binary trees:
$\varnothing \in \mathbb{T},$
$t_1, t_2 \in \mathbb{T} \implies \forall x : \mathrm{Node}(x, t_1, t_2) \in \mathbb{T}$²

Base case

$P(\varnothing)$

Induction Hypothesis

$P(t_1) \land P(t_2) \space$ for arbitrary $t_1, t_2 \in \mathbb{T}$

Inductive Step

$\forall x : P(\mathrm{Node}(x, t_1, t_2))$

As a Rule of Inference:
$$\frac{ P(\varnothing), \quad P(t_1) \land P(t_2) \implies P\big(\mathrm{Node}(x, t_1, t_2)\big) }{ \forall \tau \in \mathbb{T} : P(\tau) } \quad (\text{for arbitrary $x$, $t_1$, $t_2$})$$

Propositional Formulas – $\mathcal{L}_0$

Structural induction over syntax (!).
Note that this is easily generalizable to any recursive formal grammar.

Okay actually, we’re just going to talk about “OR-form” / $(\lnot, \lor)$-formulas.

Definition of $\mathscr{L}_{(\lnot, \lor)}$ as a grammar in BNF (F):
F ::= Q | ¬F | F ∨ F

Definition of $\mathscr{L}_{(\lnot, \lor)}$ as a a grammar in set-notation:
im sure you can find it on the internet :)

Base case

$P(Q) \space$ (for all propositions $Q$)

Induction Hypotheses

$P(A) \space$ for arbitrary $A \in \mathscr{L}_{(\lnot, \lor)}$

$P(A) \land P(B) \space$ for arbitrary $A, B \in \mathscr{L}_{(\lnot, \lor)}$

Inductive Steps

$P(\lnot A)$

$P(A \lor B)$

As a Rule of Inference:
$$\frac{ P(Q), \quad P(A) \implies P(\lnot A), \quad P(A) \land P(B) \implies P(A \lor B) }{ \forall F \in \mathscr{L}_{(\lnot, \lor)} : P(F) } \quad (\text{for arbitrary $A$, $B$})$$

Note that this is the first form so far were we have two “cases” in the IH and steps. I.e., we are establishing two recurrence implications here for the two branches in the recursive definition of $\mathscr{L}_{(\lnot, \lor)}$.

Elsethings

…

---

1. Of course, there needs to be a domain defined for $x$ to limit the possible contents of a list. In CS-terms, the list is of a (specified) homogeneous type. ↩︎ ↩︎ ↩︎

2. same as¹ ↩︎