语法的哥德尔编码

编码相当于给语法树一种可逆的存储格式。数字大小没有逻辑意义：换一种合法编码，某句的编号可能完全改变，绑定结构与证明仍可被追踪。真正有用的是“读出构造符号、取得子树、重新组装”的操作有明确算法。

尤其不能把公式 $A(z)$ 的输入位置理解为可以放进任意元语言记号。$A(\overline{q(\phi )})$ 是合法的对象语言公式；单写 $A(q(\phi ))$ 若没有声明缩写，就把外部编码函数误当成了语言符号。PA 的签名没有 $q$、$\mathrm{num}$ 或下面的 $d$。

一次真正受绑定约束的数字替换 ​

取

计算得 $c(v_0)=1$，$c(S0)=2$，$c(SS0)=12$，而 $q(v_0=0)=6C(1,0)+1=7$。左支的代码为

故整个公式代码是

现在仅把自由出现的 $v_0$ 换成 $\bar{2}=SS0$。左支遇到 $\mathrm{\forall }{v}_0$ 后停止向内替换，仍为 $215$；右支变成 $SS0=0$，代码是 $6C(12,0)+1=469$。重组得

解码得到 $(\mathrm{\forall }{v}_0(v_0=0))\wedge (SS0=0)$。若连左支也改掉，结果会是 $\mathrm{\forall }{v}_0(SS0=0)$，那是改写了受约束出现，并非自由变量替换。若把输入数 $2$ 当成项代码，则它解码为 $S0$，同样会算错；应先计算 $\mathrm{num}(2)=12$。

全定义约定与原始递归性的理由 ​

本页只需闭项替换。定义 $\mathrm{sub}(a,i,t)$：当 $a$ 是合法公式代码、$t$ 是合法闭项代码时，输出将其中自由 $v_i$ 换成该项后的公式代码；其余输入一律返回 $q(0=0)=1$。这个默认值使函数全定义。一般开放项的捕获规避替换还需绑定变量改名；这里的闭项接口已足够完成后面的数码代入。

解码 $C$ 可在 $a,b\le n$ 内有界搜索 $C(a,b)=n$；除法、余数、配对与有限条件分支都是原始递归的。每个真子项、真子公式代码严格小于父节点代码。因而可按 $0,1,\dots ,a$ 依次建立合法性和变量出现信息表；每次只查询已建立的条目。表可以用迭代配对编码，取第 $j$ 个条目只需有界次解码。这样，“使用所有较小参数的递归”便落实为普通原始递归。

固定参数 $i,t$ 后，同样建立替换结果表：原子式调用项替换；联结词组合子公式结果；量词绑定 $v_i$ 时直接保留该量词节点及其整个原有子树，绑定其他变量时重建量词。由于 $t$ 闭合，不会发生变量捕获。虽然新代码可能远大于输入，每轮更新仍由已知原始递归运算组成。数码代码满足 $\mathrm{num}(0)=0$、$\mathrm{num}(n+1)=5\mathrm{num}(n)+2$，也有直接递归构造。

若 $a$ 编码一个自由变量至多为 $v_0$ 的公式，定义

其他输入规定 $d(a)=1$。自由变量检查、数码构造和替换的复合说明 $d$ 是总的原始递归函数。它把模板的代码送回模板的自由位置；算术可表示性公理库算术可表示性Arithmetical representability用算术公式逐个输入证明函数值及其唯一性，连接外部计算和理论内推导。负责将这项外部计算转成理论内公式，对角引理公理库对角引理Diagonal lemma · Arithmetical fixed-point lemma对任意一个自由变量的算术公式，构造与该公式作用于自身编码可证等价的句子。再用它制造可证等价。

这与复杂性理论的多项式算术化公理库算术化Arithmetization把布尔关系嵌入有限域低次多项式，使离散正确性声明可由随机代数恒等式检查。任务不同：后者在有限域中把布尔函数扩展为低次多项式，以支持随机检查；本页把语法对象与语法操作编码为自然数，不靠低次数或有限域概率保证。编码也不是语义真理判定器：能机械判断“这是一份合式公式”，并不意味着能判断公式在标准自然数中是否为真。

验收练习。 不看算例重算 $148563\mapsto 1408437$，分别写出数 $2$、数码 $SS0$、项代码 $12$，并说明为何左支不变。三个对象和绑定分支都正确，才完成了这项替换任务。