Examples

The two theorems just seen are among the most powerful in this book. They allow one to construct all the basic algebraic and order structure of $\mathbb{N}$:

• Addition: In RecDef0, let $X$ be $\mathbb{N}$, $x$ be any natural and $\varphi$ be the successor function $S$ itself. Then, the theorem says that to every such $x$ as above, there corresponds a unique function $A_x:\mathbb{N}\to\mathbb{N}$ such that $A_x(0)=x$ and $A_x(S(y))=S(A_x(y))$. Now, simply define the infix-function $+:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ to be $x+y=A_x(y)$ for any $x,y\in\mathbb{N}$. Using this function, the conditions $A_x(0)=x$ and $A_x(S(y))=S(A_x(y))$ become $x+0=x$ and $x+S(y)=S(x+y)$ respectively. Also, using the fact that $S$ maps equals to equals, it is easy to see that $x+S(0)=S(x+0)=S(x)$. Denoting $S(0)$ as $1$, this becomes $x+1=S(x)$.
• Multiplication: In RecDef1, choose $\mathbb{N}$, $0$ and addition ($+$) to be the raw materials for constructing multiplication. Then, the theorem says that to every $x\in\mathbb{N}$ there corresponds a unique function $M_x:\mathbb{N}\to\mathbb{N}$ such that $M_x(0)=0$ and $M_x(S(y))=M_x(y)+x$. Now, define the infix-function $\cdot:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ as $x \cdot y = M_x(y)$ for every $x,y\in\mathbb{N}$. Hence, $x \cdot 0 = 0$ and $x\cdot(y+1)=x \cdot y + x$ (assuming $\cdot$ has higher precedence than $+$ i.e. $x \cdot y + x=(x \cdot y) + x$).
• Exponentiation: In RecDef1, choose $\mathbb{N}$, $S(0)$ and multiplication ($\cdot$) as inputs. Then, to every $x\in\mathbb{N}$ one gets a unique function $E_x:\mathbb{N}\to\mathbb{N}$ such that $E_x(0)=S(0)$ and $E_x(S(y))=E_x(y) \cdot x$. Now, define the placeholder-function $\square^\square:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ as $x^y = E_x(y)$ for every $x,y\in\mathbb{N}$. Hence, $x^0 = 1$ and $x^{y+1}=x^y \cdot x$ (assuming $\square^\square$ has higher precedence than $\cdot$).
• Factorial: In RecDef1, choose $\mathbb{N}$, $S(0)$ and the placeholder-function $\square\cdot S(\square):\mathbb{N}\times\mathbb{N}\ni(n,n') \mapsto n \cdot S(n')\in\mathbb{N}$ as inputs. Then, one has a unique postfix-function $!:\mathbb{N}\to\mathbb{N}$ such that $0!=S(0)$ and $S(y)!=y! \cdot S(y)$.
• Canonical Order: The order that I am about to define comes about as a by-product of addition. Concretely, define the $\mathbb{N}$-relation (i.e. subset of $\mathbb{N}\times\mathbb{N}$), $\leq$, thus: $(x,y)\in\ \leq$ iff $\exists n\in\mathbb{N}\ [x+n=y]$. One often writes $(x,y)\in\ \leq$ in infix-form: $x \leq y$. One can see that this order is at least reflexive: $x \leq x$ since $x+0=x$. Verifying the other two properties of a partial order must wait.
• Order of Divisibility: I can also define an analogous order on the naturals based on multiplication. For this, define the $\mathbb{N}$-relation, $\ |\$, thus: $(x,y)\in \ |\$ iff $\exists n\in\mathbb{N}\ [x \cdot n=y]$. One often writes $(x,y)\in \ |\$ in infix-form: $x\ |\ y$ where $x$ is called a factor of $y$ while $y$ is called a multiple of $x$. Just like previous order, this is a partial order. However, verification of this fact must wait.
• The Family of Sets $\text{Fin}$: In RecDef1, choose $\mathcal{P}\mathbb{N}$, $\emptyset$ and the infix-function $\oplus:\mathcal{P}\mathbb{N}\times\mathbb{N}\ni(\Sigma,n)\mapsto\Sigma\cup\{n\}\in\mathcal{P}\mathbb{N}$ as inputs. Then, one gets a unique function $\text{Fin}:\mathbb{N}\to\mathcal{P}\mathbb{N}$ such that $\text{Fin}(0)=\emptyset$ and $\text{Fin}(S(n))=\text{Fin}(n) \oplus n$. Later, I show that $\text{Fin}(n)$ is precisely the set of all naturals strictly less than $n$.