# 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!) • Oh, I see it now. Numeral system by definition has to have$S$and$isZ$, so the only thing missing is$P\$ to be used in the definition of primitive recursion. Thanks! Sep 13 '18 at 1:05
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}