chx$$\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}$$
令 $\T:=\bb{\uc\A:\A\in\th(\mathfrak N)}$ , 则 $\T\notin\Delta$ .
若不然, 由于 $\Delta=\Delta_\infin$ , 故存在 $m\in\N$ 使得 $\T\in\Sigma_m\cup\Pi_m$ . 由 I.8.72 可得 $\Sigma_m\cup\Pi_m\subsetneq\Delta_{m+1}$ , 因此可以取 $\l\xn.R\in\Delta_{m+1}$ 满足它不在 $\Sigma_m\cup\Pi_m$ 中. 再由 I.9.30 可得存在 $L_\n$ 上的公式 $\R(\xn)$ 在 $\n$ 中定义 $R$ , 为导出矛盾, 我们考虑证明如下的引理.
对于 $L_\n$ 上的项 $t[\vec v_n]$ , 函数 $q_t:=\l\xn.\uc{t[v_1\inp\widetilde{x}_1,...,v_n\inp\widetilde{x}_n]}$ 是原始递归的.
我们对项的复杂度施以归纳. 当 $t$ 是闭项时, 显然 $q_t$ 是一个常函数, 则显然是原始递归的. 当 $t$ 是单个变元时, 根据 I.9.26 , 函数 ${\rm u}:=\l n.\uc{\widetilde n}$ 是原始递归的, 假定 $t$ 的那个变元是 $v_i$ , 则 $q_t(\xn)={\rm u}(u^n_i(\xn))$ 显然是原始递归的, 故是递归的.
当 $t=f(s_1,...,s_k)$ 时, 根据规定 $\uc{t[\vec v_n\inp\widetilde\x_n]}=\la{\uc f,\uc{s_1[\vec v_n\inp\widetilde\x_n]},...,\uc{s_k[\vec v_n\inp\widetilde\x_n]}}$ , 从而由函数的复合可以得出 $q_t(\xn)=\la{\uc f,q_{s_1}(\xn),...,q_{s_k}(\xn)}$ , 而我们知道固定长度的编码函数 $\l\xn.\la{\xn}$ 时原始递归的, 同时由 I.H. 可得 $q_{s_i}$ 均是原始递归的, 故 $q_t$ 也是原始递归的.
对于 $L_\n$ 上的公式 $\Q[\vec v_n]$ , 函数 $q_{\Q}:=\l\xn.\uc{\Q[v_1\inp\widetilde{x}_1,...,v_n\inp\widetilde{x}_n]}$ 是原始递归的.
我们对公式的复杂度施以归纳.
当 $\Q$ 是原子公式时, 语言中只有 $s=t$ 和 $s<t$ 的情形, 由函数复合和 Lem 1 我们可以立即得出 $q_\Q$ 是原始递归的.
对于逻辑联词的情形, 当 $\Q\eq\neg\A$ 时, 显然 $\uc{\Q[\vec v_n\inp\widetilde\x_n]}=\la{\uc\neg,\uc{\A[\vec v_n\inp\widetilde\x_n]}}$ 即 $q_\Q(\xn)=\la{\uc\neg,q_\A(\xn)}$ , 从而由 I.H. 可得 $q_\Q$ 时原始递归的; 当 $\Q\eq\A\or\B$ 时, 同理由函数复合可以得到 $q_\Q$ 的原始递归性.
对于存在量词的情形, 假定 $\Q\eq (\ex y)\A$ , 无论我们的替换是否囊括了 $y$ , 我们可以对 $\A$ 的替换函数进行一些修改(比如放弃掉对于某些变元的替换)从而使得我们可以由 $\A$ 的替换函数中平凡地通过函数复合导出 $\Q$ 的替换函数, 因而 $q_\Q$ 亦是原始递归的.
由于 $\R(\vec v_n)$ 在 $\n$ 中定义了 $R$ , 故对于任意 $\xn\in\N$ , 我们有
$$\bl \xn\in R&\iff\R(\overline\x_n)^\n=\t\\ &\iff \n\vDash \R[v_1\inp\widetilde x_1,...,v_n\inp\widetilde x_n]\\ &\iff \uc{\R[v_1\inp\widetilde x_1,...,v_n\inp\widetilde x_n]}\in\T \el$$故有 $R(\xn)\lra\T(q_\R(\xn))$ , 而根据 I.8.63 , 由于 $q_\R$ 是原始递归的, 故 $R\in\Sigma_m\cup\Pi_m$ , 与前提矛盾.