Why does existence of predecessor imply adequacy of a numeral system?
-
05-11-2019 - |
Question
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.
No correct solution