Recursion, multiplication and exponential The set $F_{n}$ of primitive recursive function symbols of arty $n$ can be defined inductively as \begin{array}[lr]
& Z, \text{Succ} \in F_{1} & \\ \pi_{j}^{n} \in F_{n} \quad \text{for each} \quad j=1,\dots, n \\ &\text{if} \quad f \in F_{n} \quad \text{and} g_{1},\dots, g_{n} \in F_{m}, \text{then} \circ_{n}^{m}[f,g_{1},\dots,g_{n}]\in F_{m} & \\ &\text{if} \quad f \in F_{n+2} \quad \text{and} \quad g \in F_{n}, \text{then} \quad \text{Rec}^{n}[f,g]\in F_{n} &
\end{array}
Given the interpretation $f \in F_{n}$, $[[f]]:\mathbb{N}^{n} \to \mathbb{N}$
\begin{array}[lr]
[[Z]](k)&=& 0 \\ [[\text{Succ}]](k) &= &k+1 \\ [[\pi_{j}^{n}]](k_{1},\dots,k_{n}) &= &k_{j} \\ [[\circ_{n}^{m}[f,g_{1},\dots,g_{n}]]](k_{1},\dots,k_{m}) &= &[[f]]([[g_{1}]](k_{1},\dots,k_{m}),\dots, [[g_{n}]](k_{1},\dots, k_{m})) \\ [[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},0) &= & [[g]](k_{1},\dots,k_{n}) \\ [[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},m+1) &= & [[f]](k_{1},\dots,k_{n},m,[[\text{Rec}^{n}[f,g]]](k_{1},\dots,k_{n},m)
\end{array}
find functions $A,B \in F_{2}$ that yields $[[A]](x,y)=xy$ and $[[B]](x,y)=x^{y}$. 
Note $[[0]]=0$,$[[S(a)]]=[[a]]+1$, and $[[f(a_{1},\dots,a_{n})]]=[[f]]([[a_{1}]],\dots,[[a_{n}]])$ for $f \in F_{n}$
 A: (Throughout I will assume that we already have a perfectly good symbol $\newcommand{\FUN}[1]{[[\, #1 \,]]}
\newcommand{\Z}{\mathsf{Z}}
\newcommand{\F}{\mathsf{f}}
\newcommand{\G}{\mathsf{g}}
\newcommand{\Add}{\mathsf{Add}}
\newcommand{\Mult}{\mathsf{Mult}}
\newcommand{\Succ}{\mathsf{Succ}}
\newcommand{\Rec}{\mathsf{Rec}}
\newcommand{\naturals}{\mathbb{N}}
\newcommand{\Comp}[2]{\mathord{\circ}^{#1}_{#2}}
\Add \in F_2$ such that $\FUN{\Add} ( x , y ) = x + y$. I will also only handle multiplication.)
Note that multiplication on $\naturals$ is defined "recursively" by


*

*$x \cdot 0 = 0$;

*$x \cdot (y+1) = (x \cdot y ) + x$


Looking at the form of this function, it is a good guess that we are looking for a function definition in $F_2$ of the form $\Rec^1 [ \F , \G ]$ for some $\F \in F_3$ and some $\G \in F_1$.  So let us assume that we already have function definitions $\F , \G$ such that $\Mult := \Rec^1 [ \F , \G ]$ defines multiplication.  We'll use this assumption that actually find definitions for $\F$ and $\G$.


*

*$\G$ is actually a lot easier, so we begin with it.  Note that for any $k_1 \in \naturals$, since $\Mult$ defines multiplication we have that $$0 = k_1 \cdot 0 = \FUN{\Mult}(k_1,0) = \FUN{ \Rec^1 [ \F , \G ] } (k_1,0) = \FUN{\G} (k_1 ),$$ and so $\FUN{\G} (k_1) = 0$ for all $k_1 \in \naturals$.  Since $\FUN{\Z}(k_1) = 0$ for all $k_1 \in \naturals$ it seems like we can simply take $\G$ to be $\Z$.

*Now let's try to find an appropriate $\F$.  Again assuming that $\Mult$ is correct, for any $k_1 , m \in \naturals$ we have that $$\begin{align}
( k_1 \cdot m ) + k_1 
&= k_1 \cdot ( m + 1 ) \\
&= \FUN{\Mult}(k_1,m+1) \\
&= \FUN{ \Rec^1 [ \F , \G ] } (k_1 , m+1) \\
&= \FUN{ \F } (\;k_1 , m , \FUN{\Rec^1 [ \F , \G ]} (k_1,m)\;) \\
&= \FUN{ \F } (\;k_1 , m , \FUN{\Mult} (k_1,m)\;) \\
&= \FUN{ \F } ( k_1 , m , k_1 \cdot m ).\end{align}$$ It would therefore be nice if $\F$ was defined so that $\FUN{\F}(k_1,k_2,k_3) = k_1 + k_3$.  As we have $\Add$ around, if we take the composition it with projection function symbols thusly:
$$\Comp{3}{2} [ \Add , \pi^3_1 , \pi^3_3 ], \tag{1}$$ it is easy to show that $\FUN{\Comp{3}{2} [ \Add , \pi^3_1 , \pi^3_3 ]} ( k_1 , k_2 , k_3 ) = k_1 + k_3$, as desired.  So we should be able to take $\F$ to be the function definition from (1).


Putting the above together, our (educated) guess is that $$\mathsf{Mult} := \Rec^1 [ \F , \G ] =  \Rec^1 [ \Comp{3}{2} [ \Add , \pi^3_1 , \pi^3_3 ] , \Z ]$$ will be an appropriate function definition in $F_2$.  (And, indeed, a relatively straightforward induction on $y$ will show that $\FUN{\mathsf{\Mult}}(x,y) = xy$ for all $x,y \in \mathbb{N}$.)

Proceeding similarly you should be able to find an appropriate formula for exponentiation, which is given "recursively" by 


*

*$x^0 = 1$;

*$x^{y+1} = x^y \cdot x$.

A: I will try to mimic your wonderful answer, hoping you don't mind. As Oscar Wilde so succinctly put it: Imitation is the sincerest form of flattery that mediocrity can pay to greatness. 
We start with the recursive definition of exponentiation.


*

*$x^{0}=1$

*$x^{y+1}=x^{y}\cdot x$


Observing this, we note that 


*

*$Z,\text{Succ} \in F_{1}$ and $[[\text{Succ}]]([[Z]](k_{1}))=1$ for all $k_{1} \in \mathbb{N}$

*Now, if Exp were an an appropriate function definition in $F_{2}$, defined using $\text{Rec}^{1}$, then,
\begin{multline} k_{1}^{m}\cdot k =k_{1}^{m+1}=[[\text{Exp}]](k_{1},m+1) \\ =[[F]](k_{1},m+1,[[\text{Exp}]](k_{1},m))=[[f]](k_{1},m+1,k_{1}^{m}) \end{multline} for some $f \in F_{3}$. Thus, I am now in a position where I want to determine an $f$ with the property that $[[f]](k_{1},k_{2},k_{3})=k_{1}\cdot k_{3}$. But, that is exactly what you have just derived, namely $\text{Mult}$. So, if I again use this function and compose it with the right projection function symbols I end up with: $$\text{Exp}:=\text{Rec}^{1}[\circ_{2}^{3}[\text{Mult},\pi_{1}^{3},\pi_{3}^{3}],\text{Succ}(Z)]$$ 


Does this look right to you?
A: Inspired by the progress I achieved, due to the help from this forum, I decided to tackle a more demanding problem, namely to determine a function $R \in F_{2}$ such that: $$[[R]](x,y)=\text{min}(x,y)$$
I realize that in order to obtain such a recursive function I first need a function $S \in F_{2}$ that satisfy
\begin{equation}
[[S]](x,y)= \begin{cases} & x-y \quad \text{if} \quad x \geq y \\&0 \quad \quad \text{otherwise} \end{cases} \tag{1}
\end{equation}
Nevertheless, to achieve this I also need another function, the so-called predecessor function, $P \in F_{1}$. Now, I have managed to obtained the following function $P$
\begin{equation} P=\circ_{2}^{1}[\text{Rec}^{1}[Z,\pi_{2}^{3}],Z,\pi_{1}^{1}]  \end{equation}
which satisfies the criteria $[[P(0)]]=0$, and $[[P(k+1)]]=k$. The next stage then is to find a primitive recursive function for (1). Now, we see from (1) that 
\begin{equation} x-(y+1)= \begin{cases} 0   &\text{if} \quad n-m=0 \\ (x-y)-1  &\text{if} \quad x-y >0\end{cases}\end{equation}
Thus we can repress (1) as:
\begin{equation}x-y= \begin{cases} x  &\text{if} \quad y=0\\ P(x-(y-1)) &\text{if} \quad y>0\end{cases} \tag{2}\end{equation}
Now, our concerns turn to determine such a function. 
\begin{align}
k_{1} &=k_{1}-0 \\ &=[[S]](k_{1},0) \\&=[[\text{Rec}^{1}[f,g]]](k_{1},0) \\ &=[[g]](k_{1})
\end{align}
and so $[[g]](k_{1})=k_{1}$ for all $k_{1} \in \mathbb{N}$; which is satisfied by $\pi_{1}^{1}$.
But it is here, when I'm trying to do the inductive case, that my argument seems to fall apart. I have 
\begin{align} (k_{1}-m)-1&=k_{1}-(m+1) \\ &=[[\text{Rec}^{1}[f,g]]](k_{1},m+1) \\ &=[[f]](\;k_1 , m , \FUN{\Rec^1 [ \F , \G ]} (k_1,m)\;) \\ &=[[f]](\;k_1 , m , \FUN{S} (k_1,m))\; \\&=[[f]](k_{1},m,k_{1}-m) \\ &=? \end{align}
It would be very much appreciated if anyone would care to help me out. Thanks!
