Theorem. Given a function $f: \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ and a constant $c \in \mathbb{N}$. Then there is a unique function $a:\mathbb{N} \rightarrow \mathbb{N}$ s.t. $a(0) = c \wedge (\forall n \in \mathbb{N}) \: a(n++) = f(n, a(n))$.

Proof. We prove by induction that the theorem $$(\exists! a:\{ n \in \mathbb{N}: n \le N \} \rightarrow \mathbb{N}) \: \underbrace{a(0) = c}_{(i)} \wedge \underbrace{(\forall n \in \mathbb{N} : n < N) \: a(n++) = f(n, a(n))}_{(ii)}.$$ holds for each $N \in \mathbb{N}$.

"$N = 0$": $a(0) = c$ is a function from $\{0\}$ to $\mathbb{N}$ and satisfies property (i). Property (ii) holds vacuously since there are no natural numbers which are smaller than 0. The function $a$ is unique since if there was another function $a' \neq a$ such that $a'(0) = a(0) = c$, $a$ and $a'$ would, by definition of equality of functions, be equal. A contradiction.

"$N \rightarrow N++$": Assume the theorem holds for $N$ and define a new object $a'$ s.t. $$a'(n) = \begin{cases} a(n) & \text{if } n \le N \\ f(N, a(N)) & \text{if } n = N++. \end{cases}$$ It turns out that $a'$ is a function from $\{ n \in \mathbb{N} : n \le N++ \}$ to $\mathbb{N}$, since for each $n$ in the domain there's exactly one $a(n) \in \mathbb{N}$: By the induction hypothesis this is given for $n=0$ up to $N$. For $f$ being a function, it also holds for $n = N++$. Uniqueness: the induction hypothesis requires that $a(n):\{n \in \mathbb{N} : n \le N \} \rightarrow \mathbb{N}$ is unique whereas if there are two function $f, f': \{ (N, a(N)) \} \rightarrow \mathbb{N}$ such that $f(N, a(N)) = f'(N, a(N)) = a'(N++)$ they are equal. Finally, the induction hypothesis implies (i) and (ii) for $n < N$, where $a'(N++) = f(N, a(N))$ satisfies (ii) if $n < N++$.
$\Box$

2015 FEB 19 (v1.0)
Contact me: m.herrmann followed by an -at- followed by blaetterundsterne.org.

This document created with the help of MathJax (Thank you guys!)