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

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top