Why does existence of predecessor imply adequacy of a numeral system?

I encountered this result when working with $\lambda$-calculus (so every element I mention here was a $\lambda$-expression there [1]), but I will express everything with, more understandable to broader audience, notions of functions.

Intro

Definition 1

A numeral system is a sequence $d = d_0,d_1,\ldots$ such that there exist functions $S$ (successor) and $isZ$ (test for zero) such that
$$S(d_n) = d_{n+1},$$
$$isZ(d_0) = T,\ \ isZ(d_{n+1}) = F.$$
where $T$ and $F$ are notions of true and false.

Definition 2

A numeric function $\varphi : \mathbb{N}^p \to \mathbb{N}$ is definable with respect to $d$ if there exists $f$ such that
$$\forall (n_1,\ldots,n_p)\in \mathbb{N}^p\ \ f(d_{n_1},\ldots,d_{n_p}) = d_{\varphi(n_1,\ldots,n_p)}.$$

Definition 3

A numeral system $d$ is adequate if and only if all partial recursive functions are definable with respect to $d$.

My question (intro)

Proposition 1 (Proposition 6.4.3 in [1])

Let $d$ be a numeral system. $d$ is adequate if and only if there exists $P$ (predecessor) such that
$$\forall n \in \mathbb{N}\ \ P(d_{n+1}) = d_n.$$

For the $\Rightarrow$ direction, it is sufficient to observe that predecessor is a partial recursive function. Specifically, it is a primitive recursion of zero function and first coordinate projection.

My question

How would one prove a $\Leftarrow$ direction? How is it even possible to have such a powerful result, that existence of one function leads to definability of all partial recursive functions?

[1] Hendrik Pieter Barendregt, The Lambda Calculus, 1984.

Recall that the set of partial recursive functions $\mathcal{R}$ is defined inductively by the following rules:

• (zero) $\dfrac{}{\zeta : n \mapsto 0 \in \mathcal{R}}$

• (successor) $\dfrac{}{\sigma : n \mapsto n + 1 \in \mathcal{R}}$

• (projection) $\dfrac{}{\Pi_m^i : (n_1, \cdots n_m) \mapsto n_i \in \mathcal{R}}$

• (composition) $\dfrac{\chi : \mathbb{N}^m \to \mathbb{N}, \psi_i : \mathbb{N}^k \to \mathbb{N} \in \mathcal{R} }{\phi : (n_1, \cdots n_k) \mapsto \chi(\psi_1(n_1, \cdots, n_k), \cdots \psi_m(n_1, \cdots, n_k)) \in \mathcal{R}}$

• (primitive recursion) $\dfrac{\chi : \mathbb{N}^m \to \mathbb{N}, \psi : \mathbb{N}^{n+2} \to \mathbb{N} \in \mathcal{R} }{\phi : (k,n_1, \cdots n_m) \mapsto \begin{cases}

\chi(n_1, \cdots n_m) & \text{ if } k=0 \\
\psi(\phi(k-1, n_1, \cdots, n_m),k-1, n_1 \cdots n_m ) & \text{ if } k > 0\\
\end{cases} \in \mathcal{R}}$

• (minimalization) $\dfrac{\chi : \mathbb{N}^{m+1} \to \mathbb{N} \in \mathcal{R} }{\phi : (n_1, \cdots n_m) \mapsto k \text{, the least integer with } \chi(k,n_1, \cdots n_m) =0

\in \mathcal{R}}$

So we will prove the result by structural induction on $\mathcal{R}$.

• Initial functions.

It is clear that $\zeta$ is defined by $\lambda x. d_0$, $\sigma$ by $S$, and $\Pi_m^i$ by $\lambda x_1 \cdots x_m . x_i$.

• Composition

Suppose $\chi$ is defined by $f$ and $\psi_i$ by $g_i$.

Let $h$ be the term $\lambda x_1 \cdots x_k.f (g_1x_1 \cdots x_k) \cdots (g_mx_1 \cdots x_k)$. Then $h$ defines the function $\phi : (n_1, \cdots n_k) \mapsto \chi(\psi_1(\vec{n}), \cdots \psi_m(\vec{n}))$

• Primitive recursion.

Suppose $\chi$ is defined by $f$ and $\psi$ by $g$.

Let's define the combinator $\textbf{r} = \lambda nfg.isZ\:n\:f\:(g \:(P\:n))$, with the property that:

$$
\textbf{r} \: d_n \:f \: g = \begin{cases} f & \text{ if } n = 0 \\
g \: (d_{n-1}) & \text{ if } n > 0
\end{cases}
$$

Now let $h$ be the term $\textbf{y} \: (\lambda s y x_1 \cdots x_m . \textbf{r} \: y(f x_1\cdots x_m)(\lambda z.g (s z x_1 \cdots x_m)z x_1 \cdots x_m )$. Then $h$ defines $\phi: (k,n_1, \cdots n_m) \mapsto \begin{cases}
\chi(n_1, \cdots n_m) & \text{ if } k=0 \\
\psi(\phi(k-1, n_1, \cdots, n_m),k-1, n_1 \cdots n_m ) & \text{ if } k > 0\\
\end{cases}$.

• Minimalization

Suppose $\chi$ is defined by $f.

Let $g$ be the term $\textbf{y} (\lambda syx_1 \cdots x_m.isZ \: (f\: y\: x_1\cdots x_m) \: y\: (s\: (S \: y)\: x_1 \cdots x_m))$. Then take $h$ to be the term $g \: d_0$, and $h$ defines the function $\phi : (n_1, \cdots n_m) \mapsto k \text{, the least integer with } \chi(k,n_1, \cdots n_m) =0$.

By induction, every function in $\mathcal{R}$ is definable.

(I leave the proving the fact that the terms $h$ define the stated functions as an exercise!)

StackExchange Computer Science Q#97264, answer score: 4