chx$$\def\s{\mathrm{s}} \def\lra{\leftrightarrow} \def\inp{\leftarrow} \def\fa{\forall} \def\ex{\exists} \def\bl{\begin{aligned}} \def\el{\end{aligned}} \def\t{ {\bf t} } \def\f{ {\bf f} } \def\T{\mathbf{T}} \def\eq{\equiv} \def\la#1{\langle #1\rangle} \def\ov#1{\overline{#1}} \def\l{\lambda} \def\xn{{\vec x_n}} \def\x{\vec x} \def\if{\mathbf{if}\quad} \def\oth{\mathbf{otherwise}} \def\bb#1{\{#1\}} \def\th{\mathscr{T}} \def\A{\mathcal{A}} \def\B{\mathcal{B}} \def\P{\mathcal{P}} \def\Q{\mathcal{Q}} \def\R{\mathcal{R}} \def\p{\mathfrak{P}} \def\r{\mathfrak{R}} \def\uc#1{\ulcorner #1\urcorner} \def\n{\mathfrak N}$$
对于任意 $\lambda xy.f\in\frak P$ , 存在 $e$ 使得 $\lambda x.f(e,x)=\{e\}$ .
构造与证明
令函数 $h:=\l xy. f(\s^1_1(x,x),y)$ , 显然 $h\in\p$ , 故取其编码 $q$ , 之后令 $e:=\s^1_1(q,q)$ 即可. 接下来我们证明这个 $e$ 就是我们想要的, 根据构造有
$$\bl \bb e&=\bb{\s^1_1(q,q)}\\ &=\l y.\bb q(q,y)\\ &=\l y.h(q,y)\\ &=\l y.f(\s^1_1(q,q),y)\\ &=\l y.f(e,y) \el$$为什么要这么构造?
核心的原理是自指涉, 我们希望这个 $e$ 是被某个参数 $d$ 用某种范式 $F$ 构造出来的, 并且在 $e$ 中这个参数 $d$ 可以再次被输入到这个范式 $F$ 中再生成一次 $e$ , 为此我们需要用到 s-m-n 引理来帮助我们把 $d$ 的函数信息以及 $d$ 这个数字本身压缩在一起, 于是令 $e:=\s^1_1(d,d)$ . 故对于输入 $y$ , 我们有 $\bb e(y)=\bb{d}(d,y)$ . 而另一方面我们又希望 $\bb e(y)=f(e,y)$ , 这就是要求
$$\bb d(d,y)=f(\s^1_1(d,d),y)$$到这里已经给了我们很强的暗示性了, 由于 $\bb d$ 和 $d$ 一个是函数一个是数字, 本质上是很不同的东西, 所以我们可以令 $\bb d$ 就是这个范式 $F$ 本身, 即令 $\bb d=\l xy.f(\s^1_1(x,x),y)$ , 从而在 $e$ 中它会再次把参数 $d$ 解压出来然后调用 $F$ 来生成自己.
能行性与统一构造
上述的过程之所以可以被称为范式是因为我们可以把 $f\mapsto e$ 的这个过程从元层次拉到对象层次里. 对于函数 $f$ 的编码 $\uc f$ , 首先我们获取 $\l x.\s^1_1(x,x)$ 和投影函数 $u^2_2:(x,y)\mapsto y$ 的编码 $a_0,a_1$ (它们是常数), 之后我们可以用复合得到 $h$ 的编码 $\uc h=\la{1,2,\uc f,a_0,a_1}$ , 之后再令 $e=\s_1^1(\uc h,\uc h)$ 即可.
因此定理被强化为, 存在原始递归函数 $\l x.{\rm R}$ 使得对于任意的 $i\in\N$ , 若 $\bb i$ 是二元函数, 那么 $\l x.\bb{i}({\rm R}(i),x)=\bb{{\rm R}(i)}$ .