算术可表示性 | Codeboy's Blog

形式陈述

一个函数在自然数上可计算，怎样变成算术理论能够使用的事实？固定皮亚诺算术 PA，以 $\overline n=S^n0$ 表示标准自然数 $n$ 的数码。总函数 $f:\mathbb N^k\to\mathbb N$ 的一个逐输入唯一图表示是公式 $F(\mathbf x,y)$ ，自由变量仅在所列变量中，满足：对每组标准输入 $\mathbf n$ ，若 $f(\mathbf n)=m$ ，则

\mathrm{PA}\vdash F(\overline{\mathbf n},\overline m),\qquad \mathrm{PA}\vdash\forall y\bigl(F(\overline{\mathbf n},y)\to y=\overline m\bigr).

这里 $\vdash$ 是语法可推导关系。两式合起来等价于

\mathrm{PA}\vdash\forall y\bigl(F(\overline{\mathbf n},y)\leftrightarrow y=\overline m\bigr).

“对每组标准输入”在元语言中量化：每给定一组实际自然数，就有相应有限证明；并未把这一族证明直接换成一个以 $\mathbf x$ 为变量的统一定理。

对于关系 $R(\mathbf n)$ ，通常另称公式 $\rho$ 逐数值表示 $R$ ，若真实例可证 $\rho(\overline{\mathbf n})$ ，假实例可证 $\neg\rho(\overline{\mathbf n})$ 。只把函数图看成这种关系，条件会弱于上面的逐输入唯一性：排除每个错误的标准输出，并不自动排除模型中任意非标准见证。后续对角证明使用的是明确写出的唯一图表示。

直觉

表示公式像一份可在算术内部核验的计算记录。外部先算出答案 $m$ ；内部不仅能确认该答案，还能证明任何满足这份记录的输出都等于 $\overline m$ 。第二步允许在证明中取出一个未指定的存在见证，再将它替换为已知数码。

必须区分三个层次。 $\mathbb N\models F(\overline n,\overline m)$ 是标准模型中的语义断言； $\mathrm{PA}\vdash F(\overline n,\overline m)$ 要求一份形式证明； $\mathrm{PA}\vdash\forall x\exists!yF(x,y)$ 则是关于全部输入的统一存在唯一性定理。逐输入表示固定的是标准输入；统一总性则在理论的每个模型中量化所有输入元素，需要单独证明。

例子与边界

后继：表示式没有隐藏算法

取 $s(n)=n+1$ ，令 $F_s(x,y)$ 为 $y=Sx$ 。给定标准 $n$ ， $S\overline n$ 按数码定义就是 $\overline{n+1}$ ，所以 PA 由等号逻辑证明

F_s(\overline n,\overline{n+1}),\qquad \forall y(F_s(\overline n,y)\to y=\overline{n+1}).

在这个例子中还可直接证明统一总性：以 $Sx$ 作见证，等号给出唯一性。这是由 $y=Sx$ 的具体形式得到的额外性质。

复合：唯一性怎样传给下一步

设 $f,g:\mathbb N\to\mathbb N$ 分别由 $F(x,u),K(u,y)$ 表示，先改名避免变量捕获。对 $h=g\circ f$ 定义

H(x,y):=\exists u\bigl(F(x,u)\land K(u,y)\bigr).

固定标准 $n$ ，设 $f(n)=r$ 、 $g(r)=s$ 。两个表示式给出 $F(\overline n,\overline r)$ 与 $K(\overline r,\overline s)$ ，因此以 $\overline r$ 作见证证明 $H(\overline n,\overline s)$ 。

反过来，若 $H(\overline n,y)$ ，取其见证 $u$ 。 $F$ 的逐输入唯一性给出 $u=\overline r$ ；等号替换后得到 $K(\overline r,y)$ ，再由 $K$ 的唯一性推出 $y=\overline s$ 。所有步骤都在 PA 内进行，故 $H$ 表示复合函数。只知道每个错误标准输出都被否定，便不能在这一步消去任意的 $u$ 。

例如把两个后继复合，得到

H(x,y)=\exists u(u=Sx\land y=Su).

输入 $\overline3$ 时，见证为 $\overline4$ ，输出为 $\overline5$ ；任何见证先被迫等于 $\overline4$ ，输出再被迫等于 $\overline5$ 。这已经展示了后面对角证明所需的“取见证—唯一性—等号替换”机制。

推论与应用

原始递归可表示性定理。 每个有限元原始递归函数都有上述逐输入唯一图表示，甚至在弱于 PA 的 Robinson 算术 $Q$ 中便可得到，因此 PA 也可使用。这里引用完整定理；前面的后继与复合例子展示了其中两个构造分支。原始递归分支还要在算术中编码任意有限计算序列并验证相邻状态，标准证明使用序列编码或 $\beta$ 函数技术，见 Smith 的 Theorem 17.1。

用于语法编码时，数码生成及闭项自由替换都是原始递归函数。于是对角代入函数 $d$ 有一个公式 $D(x,y)$ ：一旦在元语言算出 $d(b)=g$ ，即可取得理论内的值实例 $D(\overline b,\overline g)$ 和逐输入唯一性。这是对角引理的实际输入，不要求先证明 $\forall x\exists!yD(x,y)$ 。

验收练习。 对 $H(x,y)=\exists u(u=Sx\land y=Su)$ 完成输入 $3$ 的值与唯一性证明，并指出从 $u=S\overline3$ 到 $u=\overline4$ 用的是数码展开。再解释为什么“对每个标准 $k\ne5$ 都证明 $\neg H(\overline3,\overline k)$ ”本身还不等于 $\forall y(H(\overline3,y)\to y=\overline5)$ ；关键差别是后式的 $y$ 遍历任意模型元素。

参考资料

Peter Smith，An Introduction to Gödel’s Theorems，corrected second edition，§16.1 与 Theorem 17.1，印刷119、124–127页：函数的逐输入表示及原始递归可表示性完整结果。
Open Logic Project，The Open Logic Text: Incompleteness，rev. 9620cc7，Definition 1.12、Theorem 3.27：值实例、唯一性与更一般的可计算函数表示。

形式陈述 ​

后继：表示式没有隐藏算法 ​

复合：唯一性怎样传给下一步 ​

反向链接

形式陈述

后继：表示式没有隐藏算法

复合：唯一性怎样传给下一步