\(n:\mathbb {N}\)を要素、\(f:\mathbb {N}\to \mathbb {N}\to \mathbb {N}\)を関数とする。原始再帰(primitive recursion)による関数\(\mathord {\textnormal {\textsf {prim-rec}}}(n,f):\mathbb {N}\to \mathbb {N}\)が\(\mathord {\textnormal {\textsf {prim-rec}}}(n,f,0)\equiv n\)と\(\mathord {\textnormal {\textsf {prim-rec}}}(n,f,\mathord {\textnormal {\textsf {succ}}}(m))\equiv f(m,\mathord {\textnormal {\textsf {prim-rec}}}(n,f,m))\)で定義される。形式的には\(\mathord {\textnormal {\textsf {prim-rec}}}(n,f)\equiv \lambda m.\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(m,\lambda x.\mathbb {N},n,\lambda (x,y).f(x,y))\)である。よって、いわゆる原始再帰的関数はすべて構成できる。