# A Proof that the Natural Numbers Form a pca?

It is known that the set of natural numbers with the operation ab = {a}b, where {a} represents the index of a recursive function, forms a partial combinatory algebra (pca). All the references I have so far consulted mention the set of natural numbers as an example of a pca with no proof. If possible, I would appreciate if someone could refer me to such proof.

-

For a formalization of Turing machines you could look at

Andrea Asperti and Wilmer Ricciotti: Formalizing Turing Machines. Lecture Notes in Computer Science Volume 7456, 2012, pp 1-25.

The book

Martin Davis. Computability and Unsolvability. Courier Dover Publications, 1982 (3rd reprint).

contains an amazing amount of detail about Turing machines.

Given these references, let us take as granted the details of the numbering $\varphi$ of partial computable maps, the s-m-n and u-t-m theorems from computability theory, and one bit of knowledge: if we fix one argument of a partial computable map of two arguments we obtain a partial computable map again.

With s-m-n and u-t-m theorems in hand, it is not hard to show that Kleene's first algebra is a partial combinatory algebra. We just need to construct the $\mathsf{K}$ and $\mathsf{S}$ combinators.

To get the $\mathsf{K}$ combinator, consider the partial computable map $$f(x, y) = x.$$ By the s-m-n theorem there exists $p$ such that $\varphi_{s(p, x)}(y) \simeq f(x,y)$ for all $x, y \in \mathbb{N}$. Here $s$ is the total computable map appearing in the s-m-n theorem and $\simeq$ is Kleene equality "if one side is defined then so it the other and they are equal". Now the map $x \mapsto s(p, x)$ is total and computable, hence there is $\mathsf{K}$ such that $\varphi_{\mathsf{K}}(x) = s(p, x)$ for all $x$. We now have (I write $a \cdot b$ for Kleene application, i.e., $a \cdot b = \lbrace a \rbrace b = \varphi_a(b)$): $$(\mathsf{K} \cdot x) \cdot y = \varphi_{\mathsf{K}}(x) \cdot y = s(p,x) \cdot y = \varphi_{s(p,x)}(y) = f(x,y) = x.$$

For the $\mathsf{S}$ combinator, let $u$ be the universal computable map from the u-t-m theorem. It has the property that, for all $t$ and $m$, $$u(t, m) \simeq \varphi_t(m).$$ In other words, $u(t,m) \simeq t \cdot m$ so the u-t-m theorem is just saying that Kleene application is computable. Consider the map $$g(x,y,z) = u(u(x, z), u(y,z)).$$ We have $$g(x,y,z) \simeq u(x,z) \cdot u(y,z) \simeq (x \cdot z) \cdot (y \cdot z).$$ We just need a code for $g$, which we get by appying the s-m-n theorem twice.

By the s-m-n theorem there is $p$ such that $\varphi_{s^{(2)}(p, x, y)}(z) \simeq g(x,y,z)$ for all $x,y,z$. Let $r$ be such that $\varphi_r(x,y) = s^{(2)}(p, x, y)$ for all $x, y$. Note that $\varphi_r$ is total because the map $s^{(2)}$ from the s-m-n theorem is total. By the s-m-n theorem there is $q$ such that $\varphi_{s(q,x)}(y) = \varphi_r(x,y)$ for all $x,y$. Let $\mathsf{S}$ be such that $\varphi_\mathsf{S}(x) = s(q,x)$ for all $x$. Now finally compute $$((\mathsf{S} \cdot x) \cdot y) \cdot z \simeq (s(q,x) \cdot y) \cdot z \simeq \varphi_{s(q,x)}(y) \cdot z \simeq \varphi_r(x,y) \cdot z \simeq$$

$$s^{(2)}(p,x,y) \cdot z \simeq \varphi_{s^{(2)}(p,x,y)}(z) \simeq g(x,y,z) = (x \cdot z) \cdot (y \cdot z).$$ Also, since $\mathsf{S} \cdot x \cdot y = s^{(2)}(p,x,y)$ we see that $\mathsf{S} \cdot x \cdot y$ is defined for all $x, y$, as required.

-
Thanks, Andrej Bauer. –  Jean Joseph Jun 6 '13 at 4:12
It was easier to write this than to find a reference. If there is one to be found, it's probably in original work of Kleene's. He didn't skip the details (and that's an understatement). –  Andrej Bauer Jun 6 '13 at 6:57

You may be interested in the following demonstration how natural numbers can be implemented within pca's: (see pages 19-20) http://www.mathematik.tu-darmstadt.de/~streicher/REAL/REAL.pdf

-
Please read the questions more carefully, this reference is not helpful because in Example 3.1 it assumed without proof precisely what the question asks for. We are looking for a proof of Example 3.1. –  Andrej Bauer Jun 5 '13 at 8:50
Thanks, Waldemar. –  Jean Joseph Jun 6 '13 at 4:12