算术可表示性

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

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

PA 内的余数存在唯一性 ​

PA 能证明对每个正模数 $m$ 和被除数 $b$，存在唯一的 $u<m$ 使 $b=qm+u$（某个 $q\le b$）。存在性对 $b$ 归纳：$b=0$ 取 $q=u=0$；已有 $b=qm+u$ 时，若 $u+1<m$ 就保留 $q$ 并令余数为 $u+1$，否则由 $u<m$ 得 $u+1=m$，令新商 $q+1$、新余数零。两支都给出 $b+1$ 的分解，并保持商不超过被除数。

唯一性在 PA 中比较两种分解 $qm+u=q^{\prime }m+v$，其中 $u,v<m$。若 $q<q^{\prime }$，则

矛盾；对称排除 $q^{\prime }<q$，故 $q=q^{\prime }$，加法消去给出 $u=v$。所用自然数次序、乘法单调和消去律都可由 PA 的基本算术归纳得到。因为 $1+(i+1)c\ge 1$，代入便有统一定理

这是后续计算记录的一个局部算术引理，确实是统一存在唯一性；它不等于所有被编码递归函数的统一总性。尤其在唯一性证明中，$b,c$ 可以是任意模型元素，不必先证明它们是标准数码。

在元语言中编码任意有限列表 ​

给定标准有限列表 $a_0,\dots ,a_n$，取

$0!=1$，所以 $n=0$ 也可用；所有 $a_i<c<m_i$。模数 $m_i$ 两两互素：若素数 $p$ 同时整除 $m_i,m_j$，其中 $i<j$，则它整除差 $(j-i)c$。它不能整除 $c$，否则从 $m_i-(i+1)c=1$ 得矛盾；于是 $p\mid j-i$。但 $1\le j-i\le n$，每个这样的整数都整除 $n!$、进而整除 $c$，又迫使 $p\mid c$，矛盾。

由整数中国剩余定理公理库整数中国剩余定理Chinese remainder theorem for integers用最大公因数判定一般联立同余的相容性，并构造模最小公倍数唯一的解。，存在非负整数 $b$ 使 $b\equiv a_i(\mathrm{mod}{m}_i)$。具体可令 $D=\prod _i{m}_i$、$D_i=D/m_i$，选 $e_i$ 满足 $D_i{e}_i\equiv 1(\mathrm{mod}{m}_i)$，再取 $\sum _i{a}_i{D}_i{e}_i$ 模 $D$ 的非负代表；若 $n=0$，直接取 $b=a_0$ 也可以。因为 $0\le a_i<m_i$，就得到

这是外部自然数中的有限构造。它为每份已算出的标准记录提供实际数码，不声称已经在 PA 内证明“每个可能非标准长度的列表都能延长”。也不要求编码唯一；$n$ 作为另外的参数说明要读取多少项，$b,c$ 本身没有存储唯一的长度。[1, §15.2]

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

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

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

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

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

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

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

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

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

多元复合与初始函数 ​

零函数用 $y=0$ 表示，投影 ${\pi }_j(\overline{x})=x_j$ 用 $y=x_j$ 表示；后继已在上面处理。若 $h(\overline{x})=g(f_1(\overline{x}),\dots ,f_k(\overline{x}))$，则取

固定标准输入后，每个 $F_j$ 的唯一性先迫使 $u_j$ 等于实际的标准中间值数码，再用 $G$ 的唯一性确定 $y$；存在性使用这些数码作见证。因此前面的单元复合论证覆盖了原始递归定义所需的任意有限元复合。

原始递归的表示公式 ​

设

且 $G(\overline{x},a)$、$H(\overline{x},t,u,v)$ 已分别逐输入唯一表示 $g,h$。先把约束变量换新，定义

初始合取确认第零项，有限循环合取检查每一步递推，最后一个合取读取终项。此处 $\mathrm{\forall }i<n\theta$ 缩写为 $\mathrm{\forall }i(i<n\to \theta )$，不是把可变长度的公式串直接放进语法。

对每个标准输入构造值证明 ​

固定标准 $\overline{r},n$，在元语言算出 $a_0=g(\overline{r})$、$a_{i+1}=h(\overline{r},i,a_i)$，直到 $a_n=f(\overline{r},n)$。外部编码引理给出具体 $b_0,c_0$。每个商与余数都是确定自然数，因此 PA 可通过数码运算证明所有

$G,H$ 的表示假设给出初始值和各步实际值的公式实例。要把有限多个实例变成有界全称，使用 PA 的有限数码穷尽事实：对每个固定标准 $n>0$，

它由 $i<0$ 不可能以及 $i<Sz\leftrightarrow (i<z\vee i=z)$ 逐次展开得到。按这些分支作等号替换，就证明中间有界全称；$n=0$ 时它真空成立。最后用 $\overline{b_0},\overline{c_0}$ 作存在见证，得 $\mathrm{PA}⊢F(\bar{\overline{r}},\bar{n},\overline{a_n})$。

任意记录的输出为什么仍然唯一 ​

仍固定这些标准输入，但在 PA 内假设 $F(\bar{\overline{r}},\bar{n},y)$，取任意的存在见证 $b,c$。初始合取的 $G$ 由逐输入唯一性迫使初值等于 $\overline{a_0}$，故可推出 $B(b,c,0,\overline{a_0})$。

假设已经推出 $B(b,c,\bar{i},\overline{a_i})$，其中 $i<n$ 是固定标准数。中间合取在 $\bar{i}$ 处给出某个 $u,v$。余数唯一性使 $u=\overline{a_i}$；把它替换进 $H$ 后，输入 $\bar{\overline{r}},\bar{i},\overline{a_i}$ 都是标准数码，故 $H$ 的逐输入唯一性给出 $v=\overline{a_{i+1}}$。消去临时存在见证，便得到下一项的 $B$ 公式。

这样在元语言安排恰好 $n$ 次有限推导，最后得到 $B(b,c,\bar{n},\overline{a_n})$。与末项 $B(b,c,\bar{n},y)$ 再用一次余数唯一性，得 $y=\overline{a_n}$。$b,c,y$ 始终是任意模型元素，因此完成的是真正的理论内结论

不是只排除错误的标准输出。零函数、后继、投影、复合与递归的构造分支现已全部闭合，按函数的有限原始递归定义树归纳，就证明了本页定理。[1, §17.3]

1394与6编码1、3、7 ​

取 $f(0)=1$、$f(t+1)=2f(t)+1$。前三项为 $1,3,7$，代码 $b=1394,c=6$ 给出模数 $7,13,19$：

三个余数都小于相应模数。编码引理中的 $c>max{a}_i$ 是一种方便的充分选择，不是任何有效编码的必要条件；本例 $6<7$ 仍完全合法。

在公式中可取 $G(a)\equiv a=1$、$H(t,u,v)\equiv v=u+u+1$。表中商给出三条 $B$ 的数码证明，两条等式 $3=1+1+1$、$7=3+3+1$ 给出步骤证明，故 $F(\bar{2},\bar{7})$ 可证。反过来，对任何 $F(\bar{2},y)$ 的代码见证，初值先被迫为一，第一步被迫为三，第二步被迫为七，末项唯一性再迫使 $y=\bar{7}$。这说明数码算例与一般唯一性论证承担不同工作。

表示性与统一总性的边界 ​

上述证明固定每个标准递归长度，外部算出一份有限记录，再在 PA 内证明任意代码见证的输出唯一。它没有把外部编码引理当作 PA 内关于任意长度的序列延长定理。因此不能仅凭本证明最后一句，就声称已经给出 $\mathrm{PA}⊢\mathrm{\forall }\overline{x},n\mathrm{\exists }!yF(\overline{x},n,y)$ 的统一总性推导。原始递归函数确实可在 PA 中获得合适的统一总性证明，但那还需内化有限序列延长等步骤，本页终点是明确的逐输入唯一表示。

更弱的 Robinson 算术 $Q$ 也有原始递归可表示性结果，见 Smith Theorem 17.1；其证明要调整余数图公式以取得足够的唯一性。本页使用 PA 的归纳证明余数引理，没有把这一证明直接降到没有归纳模式的 $Q$。

语法编码的接口 ​

用于语法编码公理库语法的哥德尔编码Gödel coding of syntax · Arithmetization of syntax把有限项、公式和自由变量替换编码为自然数运算，为算术内部表达语法提供接口。时，数码生成及闭项自由替换都是原始递归函数。于是对角代入函数 $d$ 有一个公式 $D(x,y)$：一旦在元语言算出 $d(b)=g$，即可取得理论内的值实例 $D(\bar{b},\bar{g})$ 和逐输入唯一性。这是对角引理公理库对角引理Diagonal lemma · Arithmetical fixed-point lemma对任意一个自由变量的算术公式，构造与该公式作用于自身编码可证等价的句子。的实际输入，不要求先证明 $\mathrm{\forall }x\mathrm{\exists }!yD(x,y)$。

验收练习。 先按三条除法等式核对 $1394,6$ 的编码，并指出代码没有携带唯一长度。再对 $H(x,y)=\mathrm{\exists }u(u=Sx\wedge y=Su)$ 完成输入 $3$ 的值与唯一性证明，并指出从 $u=S\bar{3}$ 到 $u=\bar{4}$ 用的是数码展开。再解释为什么“对每个标准 $k\ne 5$ 都证明 $\mathrm{\neg }H(\bar{3},\bar{k})$”本身还不等于 $\mathrm{\forall }y(H(\bar{3},y)\to y=\bar{5})$；关键差别是后式的 $y$ 遍历任意模型元素。