primitive recursion in the lambda calculus

Question

I am having trouble finding out what a primitive subset of the lambda calculus would look like. I reference primitive recursion as shown here: "https://en.wikipedia.org/wiki/Primitive_recursive_function".

These are the three base axioms:

• Constant function: The 0-ary constant function 0 is primitive recursive.
• Successor function: The 1-ary successor function S, which returns the successor of its argument (see Peano postulates), is primitive recursive. That is, S(k) = k + 1.
• Projection function: For every n≥1 and each i with 1≤i≤n, the n-ary projection function Pin, which returns its i-th argument, is primitive recursive.

Here is my confusion. In the LC zero is represented as (λfx. x). Next the successor functions is defined as (λnfx. f (n f x)). Because they are both axioms both of these functions can be classified as primitive. But when I apply the function suc to zero I get the encoding of the number one. Which is represented as the function (λf.(λx.(f x))). Now this number is neither zero or the suc function but the result of application. As such I do not see how this result function (value of 1) fits into the rule set. But very clearly a program with the number 1 in it is still primitive recursive. What am I not understanding here? While 1 is the suc to zero, once suc is applied it is neither suc, nor zero.

Answer 1

As you mention, $1$ is primitive recursive according to the following proof:

• $0$ is primitive recursive (axiom)
• $\operatorname{suc}$ is primitive recursive (axiom)
• $1=\operatorname{suc}(0)$ is primitive recursive (composition)

Using this you can show that $1$ is admissible, that is if you add $1$ as an axiom, the resulting set of functions is still the primitive recursive functions.

Note that lambda calculus has absolutely nothing to do with the answer.