Define $\mathbb{N}$ as the initial object in the following category:
Objects. Sets $X$ equipped with a function $S : X \rightarrow X$ and an element $0:X$.
Morphisms. Functions that preserves $S$ and $0$.
In words: "$\mathbb{N}$ is defined to be the initial pointed monounary algebra."
This raises the question: "How are we to define addition?" There's at least two possible ways of doing so:
Approach 0. (Recursion.) $+$ is the unique function $\mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ such that the following hold:
$$a + S(b) = S(a)+b, \qquad a+0 = a$$
For example, lets show that $2+2=4$.
$$S(S(0))+ S(S(0)) = S(S(S(0)))+S(0) = S(S(S(S(0))))+0 = S(S(S(S(0))))$$
Approach 1. (Substitution.) $+$ is the function $\mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ given as follows:
$$a+b = [0 \leftarrow a](b)$$
(Where $[0\leftarrow a]$ is the "substitution operator" that replaces each instance of $0$ with $a$.)
For example: $$S(S(0))+S(S(0)) = [0 \leftarrow S(S(0))]S(S(0)) = S(S(S(S(0))))$$
Question. Is it more than just a coincidence that we can define $+$ in two different ways like this? In particular, is there some kind of deep relationship between substitution and recursion that I'm not seeing?
Answers from a categorial / universal algebraic viewpoint are especially welcome.
Addendum. In the comment's section, it was requested that the substition operator be defined precisely. Here's one way of doing this. By a monounary algebra, I mean a set $X$ equipped with a function $S : X \rightarrow X$. Then $\mathbb{N}$ can be viewed as the monounary algebra freely generated by $\{0\}$. So for each $n \in \mathbb{N}$, there is a unique homomorphism of monounary algebras $\varphi_n : \mathbb{N} \rightarrow \mathbb{N}$ satisfying $\varphi_n(0) = n$. We can denote $\varphi_n$ by $[0 \leftarrow n]$.
We can construct the initial algebra $\mathbb{N}$ of the category you describe as the set of all terms built from a nullary constructor (operation symbol) $\mathsf{Z}$ and a unary constructor $\mathsf{S}$. The initiality means that for any diagram of sets and functions $1\xrightarrow{z} X\xrightarrow{s} X$, there is a unique function $f\colon\mathbb{N}\to X$ such that
This is a special form of recursive definitions, called a catamorphism or a “right fold” (in functional programming). At the same time, we can see this as a form of substitution: if we read the equations as evaluation rules, from left to right, the first replaces each occurrence of $\mathsf{Z}$ by $z$ and the second replaces each occurrence of $\mathsf{S}$ by $s$, so that a term $\mathsf{S}(\mathsf{S}\cdots (\mathsf{S}(\mathsf{Z}))\cdots)$ evaluates to $s(s\cdots (s(z))\cdots)$.
This works for addition: $m + -$ is the unique function $f$ such that:
It replaces each occurrence of $\mathsf{Z}$ by $m$ and each occurrence of $\mathsf{S}$ by $\mathsf{S}$, so that $m + \mathsf{S}(\mathsf{S}\cdots (\mathsf{S}(\mathsf{Z}))\cdots)$ evaluates to $\mathsf{S}(\mathsf{S}\cdots (\mathsf{S}(m))\cdots)$. This is the recursive definition of addition corresponding to your “substitutive” definition.
We can also put your recursive definition of addition into catamorphism form by defining $m + n$ as $f(n)(m)$ for the unique function $f\colon \mathbb{N}\to (\mathbb{N}\to\mathbb{N})$ such that:
so that $- + \mathsf{S}(\mathsf{S}\cdots (\mathsf{S}(\mathsf{Z}))\cdots)$ evaluates to $(\cdots(id\circ\mathsf{S})\cdots \circ \mathsf{S})\circ \mathsf{S}$.
As another example, $m^{-}$ is the unique function $f$ such that:
It replaces each occurrence of $\mathsf{Z}$ by $1$ and each occurrence of $\mathsf{S}$ by $m\cdot -$, so that $m^{\mathsf{S}(\mathsf{S}\cdots (\mathsf{S}(\mathsf{Z}))\cdots)}$ evaluates to $m\cdot(m\cdot\cdots (m\cdot 1)\cdots)$.
The relationship between recursion and substitution is perhaps clearer if we represents natural numbers by λ-terms, using Church encoding. I will use a typed version, since it’s more readable and the parallel with the discussion above is more visible. There are two kinds of λ-terms: application of a term $f$ of type $A\to B$ to a term $a\colon A$, noted $f\,a\colon B$, and λ-abstraction $(\lambda x\colon A. t)\colon A\to B$, where $t\colon B$ under the assumption that $x\colon A$. There is one evaluation rule, β-reduction: $(\lambda x\colon A. t) a$ evaluates to $t \{x\mapsto a\}$ ($t$ in which $a$ is substituted for $x$).
The type of natural numbers can be defined as $\mathbb{N}\triangleq \forall X. (X\to X)\to (X \to X)$, i.e. the type of functions mapping a type $X$, a function $s\colon X\to X$ and an element $z\colon X$ to an element of type $X$ (this is the Böhm-Berarducci encoding of the inductive type of natural numbers). Individual natural numbers can be defined using Church encoding (we will use $\Lambda X. t$ to represent functions on types, and $t\, [X]$ to represent type application):
Now, if we are given a type $X'$, with $z'\colon X'$ and $s'\colon X'\to X'$, the corresponding catamorphism $\mathbb{N}\to X'$ is very easy to define: it’s just $\lambda n\colon\mathbb{N}. n\,[X']\,s'\,z'$ (i.e. $n$ applied to the catamorphism data, since $n$ is precisely a function taking such data and returning an element of $X'$).
To evaluate $n\,[X']\, s'\, z'$ for a specific $n$ of the form $\Lambda X. \lambda s\colon X\to X. \lambda z\colon X. s\,(s\, \cdots (s\,z)\cdots)$, we apply the β-reduction rule for each application, i.e. we substitute $s'$ for $s$ and $z'$ for $z$, obtaining $s'\,(s'\, \cdots (s'\,z')\cdots)$.
This can be generalised to other kinds of algebras (lists, various kinds of trees).