cover.png#代数结构与数理逻辑学习笔记8

定义 18.1 带等词的谓词演算

设谓词演算 \(K\) 的语言中有一个特殊的二元谓词符号 \(R_1^2\)，把它写成 \[ \approx \] 并读作“等词”。在带等词的谓词演算中，除原来的逻辑公理和推理规则外，再加入以下等词公理

定义 18.1.1 等词公理

等词公理分为三类。

第一类是自反性： \[ \text{(E1)}\qquad t\approx t \]

第二类是函数符号中的替换性。若 \(f_i^n\) 是 \(n\) 元函数符号，则 \[ \text{(E2)}\qquad t_k\approx u\to f_i^n(t_1,\dots,t_k,\dots,t_n) \approx f_i^n(t_1,\dots,u,\dots,t_n) \]

第三类是谓词符号中的替换性。若 \(R_i^n\) 是 \(n\) 元谓词符号，则 \[ \text{(E3)}\qquad t_k\approx u\to \bigl( R_i^n(t_1,\dots,t_k,\dots,t_n) \to R_i^n(t_1,\dots,u,\dots,t_n) \bigr) \]

其中 \(t,t_1,\dots,t_n,u\) 都是任意项，\(k=1,\dots,n\)

这三类公理共同表达的是：相同的对象可以在函数项和谓词公式中互相替换。

注意，等词公理本身一般不是普通谓词逻辑的有效式。若解释域中把 \(\approx\) 解释成一个任意二元关系，它不一定满足自反性和替换性。只有当 \(\approx\) 被解释为真正的相等关系时，这些等词公理才都为真

命题 18.1.2 等词解释为相等时等词公理为真

设解释域 \(M\) 中 \(\approx\) 被解释为真正的相等关系 \(=\)，则 \(M\) 是等词公理集 \(E\) 的模型

证明： 点击查看证明

任取赋值 \(\varphi\)

对 (E1)，任意项 \(t\) 的解释都是 \(M\) 中的一个对象，当然有 \[ \varphi(t)=\varphi(t) \] 所以 \[ |t\approx t|(\varphi)=1 \]

对 (E2)，若 \[ |t_k\approx u|(\varphi)=1 \] 则 \[ \varphi(t_k)=\varphi(u) \] 函数解释保持输入相等时输出相等，于是 \[ \varphi\bigl(f_i^n(t_1,\dots,t_k,\dots,t_n)\bigr) = \varphi\bigl(f_i^n(t_1,\dots,u,\dots,t_n)\bigr) \] 所以 (E2) 在 \(M\) 中为真。

对 (E3)，若 \(t_k\) 与 \(u\) 的解释相等，并且 \[ R_i^n(t_1,\dots,t_k,\dots,t_n) \] 为真，那么把第 \(k\) 个解释对象换成相等对象后，元组不变，故 \[ R_i^n(t_1,\dots,u,\dots,t_n) \] 仍为真。

因此所有等词公理在把 \(\approx\) 解释为真正相等关系的解释域中都为真

命题 18.1.3 等词推出对称性和传递性

在等词公理集 \(E\) 中，对任意项 \(t,u,v\)，有： \[ E\vdash t\approx u\to u\approx t \] \[ E\vdash t\approx u\to (u\approx v\to t\approx v) \]

也就是说，虽然等词公理只显式列出自反性和替换性，但对称性、传递性可以推出

证明： 点击查看证明

先证明对称性。

由 (E3) 用公式 \(x\approx t\) 作替换性质，可得 \[ t\approx u\to (t\approx t\to u\approx t) \] 又由 (E1) 有 \[ t\approx t \] 所以用 MP 得 \[ t\approx u\to u\approx t \]

再证明传递性

已知刚证明的对称性： \[ t\approx u\to u\approx t \] 由 (E3) 对公式 \(u\approx v\) 替换，可得 \[ u\approx t\to (u\approx v\to t\approx v) \] 把两式用假言三段论连接，即得 \[ t\approx u\to (u\approx v\to t\approx v) \]

命题 18.1.4 等项替换

若 \(t(u)\) 是含有项 \(u\) 的项，\(t(v)\) 是把其中某一处 \(u\) 替换为 \(v\) 后得到的项，则 \[ E\vdash u\approx v\to t(u)\approx t(v) \]

若 \(p(u)\) 是含有项 \(u\) 的公式，\(p(v)\) 是把其中某一处自由出现的 \(u\) 替换为 \(v\) 后得到的公式，并且替换不导致变元受约束，则 \[ E\vdash u\approx v\to (p(u)\to p(v)) \]

证明： 点击查看证明

第一式对项 \(t(u)\) 的构造层次归纳

若 \(t(u)\) 本身就是 \(u\)，则结论是 \[ u\approx v\to v\approx v \] 或 \[ u\approx v\to u\approx v \] 这些由等词公理和命题逻辑立即得到

若 \[ t(u)=f(t_1,\dots,t_k(u),\dots,t_n) \] 则归纳假设给出 \[ u\approx v\to t_k(u)\approx t_k(v) \] 再由 (E2) 得 \[ t_k(u)\approx t_k(v)\to f(t_1,\dots,t_k(u),\dots,t_n) \approx f(t_1,\dots,t_k(v),\dots,t_n) \] 合并即得项替换

第二式对公式 \(p(u)\) 的层次归纳

原子公式情形由 (E3) 和第一部分的项替换得到。否定、蕴涵等联结词情形由命题逻辑规则处理。量词情形要注意：只有当被替换项中的自由变元不会被量词捕获时，才能把替换推进到量词内部

所以等词系统不仅能处理 \(u=v\) 的基本性质，也能处理“相等对象在任意上下文中可以替换”的形式化规则

这一节的作用在于给形式算术提供等式推理工具。后面证明 \[ \bar m+\bar n\approx \overline{m+n} \] 或者从 \[ p(\bar n,t) \] 推出 \[ t\approx \overline{f(n)} \] 时，实际都在使用这些等词推理

定义 18.2 形式算术 \(K_N\)

把形式算术 \(K_N\) 看成一种特殊的带等词谓词演算。它的语言只有描述自然数算术所需的符号：

• 个体常元：\(c_1\)，以后写作 \(\bar 0\)
• 一元函数符号：\(f_1^1\)，以后写作后继 \('\)
• 二元函数符号：\(f_1^2\)，以后写作 \(+\)
• 二元函数符号：\(f_2^2\)，以后写作 \(\times\)
• 等词：\(\approx\)

因此项可以写成： \[ \bar 0,\quad x,\quad t',\quad t_1+t_2,\quad t_1\times t_2 \]

在标准自然数解释域 \[ \mathbb N=\{0,1,2,\dots\} \] 中，\(\bar 0\) 解释为 \(0\)，\(t'\) 解释为后继，\(+\) 解释为加法，\(\times\) 解释为乘法，\(\approx\) 解释为相等

自然数 \(n\) 对应的闭项称为 \(K_N\) 的数字或数码： \[ \bar n=\underbrace{\bar0''\cdots'}_{n\text{ 个 }'} \] 例如 \[ \bar1=\bar0',\qquad \bar2=\bar0'',\qquad \bar3=\bar0''' \]

定义 18.2.1 算术公理

\(K_N\) 的算术公理记作公理集 \(N\)。除等词公理外，核心算术公理模式如下

后继不为零： \[ \text{(N1)}\qquad t'\not\approx \bar0 \]

后继单射： \[ \text{(N2)}\qquad t_1'\approx t_2'\to t_1\approx t_2 \]

加法对零的归约： \[ \text{(N3)}\qquad t_1+\bar0\approx t_1 \]

加法对后继的归约： \[ \text{(N4)}\qquad t_1+t_2'\approx (t_1+t_2)' \]

乘法对零的归约： \[ \text{(N5)}\qquad t_1\times\bar0\approx \bar0 \]

乘法对后继的归约： \[ \text{(N6)}\qquad t_1\times t_2'\approx t_1\times t_2+t_1 \]

归纳公理模式： \[ \text{(N7)}\qquad p(\bar0)\to \bigl(\forall x(p(x)\to p(x'))\to \forall x\,p(x)\bigr) \] 其中 \(p(x)\) 是任意公式

这七类公理的含义分别对应 Peano 算术中关于 \(0\)、后继、加法、乘法和归纳法的基本性质

注意，(N7) 不是一条公理，而是一个公理模式。每取一个公式 \(p(x)\)，就得到一条归纳公理

命题 18.2.2 标准解释使算术公理为真

在自然数标准解释域 \(\mathbb N\) 中，\(N\) 中所有算术公理都为真

证明： 点击查看证明

(N1) 表示任何自然数的后继都不是 \(0\)，这在 \(\mathbb N\) 中成立

(N2) 表示若 \[ n+1=m+1 \] 则 \[ n=m \] 这就是后继函数的单射性

(N3)、(N4) 是加法的递归定义： \[ n+0=n \] \[ n+(m+1)=(n+m)+1 \]

(N5)、(N6) 是乘法的递归定义： \[ n\cdot0=0 \] \[ n\cdot(m+1)=n\cdot m+n \]

(N7) 是自然数归纳法的形式化。若某性质对 \(0\) 成立，且对任意 \(x\)，从 \(x\) 成立能推出 \(x'\) 成立，则该性质对所有自然数成立

所以标准自然数解释是 \(K_N\) 算术公理的模型

命题 18.2.3 数字加法可证

对任意自然数 \(m,n\)， \[ N\vdash \bar m+\bar n\approx \overline{m+n} \]

证明： 点击查看证明

对 \(n\) 作普通自然数归纳

当 \(n=0\) 时，由 (N3) 得 \[ \bar m+\bar0\approx \bar m \] 而 \[ \overline{m+0}=\bar m \] 所以结论成立

设 \[ N\vdash \bar m+\bar n\approx \overline{m+n} \] 则由 (N4) 得 \[ \bar m+\bar n'\approx (\bar m+\bar n)' \] 由归纳假设和等项替换得 \[ (\bar m+\bar n)'\approx \overline{m+n}' \] 即 \[ (\bar m+\bar n)'\approx \overline{m+n+1} \] 用传递性合并： \[ N\vdash \bar m+\overline{n+1}\approx \overline{m+n+1} \]

所以对所有 \(n\) 成立

这里的归纳是元语言中的归纳，即我们在证明关于所有自然数 \(n\) 的命题，而不是在 \(K_N\) 内部使用 (N7)

命题 18.2.4 数字乘法可证

对任意自然数 \(m,n\)， \[ N\vdash \bar m\times\bar n\approx \overline{mn} \]

证明： 点击查看证明

对 \(n\) 作普通自然数归纳

当 \(n=0\) 时，由 (N5) 得 \[ \bar m\times\bar0\approx \bar0 \] 而 \[ \overline{m\cdot0}=\bar0 \] 结论成立

设 \[ N\vdash \bar m\times\bar n\approx \overline{mn} \] 由 (N6) 得 \[ \bar m\times\bar n'\approx \bar m\times\bar n+\bar m \] 由归纳假设、等项替换和命题 18.2.3 得 \[ \bar m\times\bar n+\bar m \approx \overline{mn}+\bar m \approx \overline{mn+m} \] 而 \[ mn+m=m(n+1) \] 所以 \[ N\vdash \bar m\times\overline{n+1}\approx \overline{m(n+1)} \]

命题 18.2.5 左加零可证

虽然 (N3) 只给出 \[ t+\bar0\approx t \] 但在 \(N\) 中可以证明 \[ N\vdash \bar0+t\approx t \]

证明： 点击查看证明

对公式 \[ p(x)\equiv \bar0+x\approx x \] 使用 (N7)。

基础步： \[ \bar0+\bar0\approx \bar0 \] 由 (N3) 得到

归纳步需要证明 \[ \bar0+x\approx x\to \bar0+x'\approx x' \] 由 (N4) 有 \[ \bar0+x'\approx(\bar0+x)' \] 若 \(\bar0+x\approx x\)，则由等项替换得 \[ (\bar0+x)'\approx x' \] 于是由传递性得 \[ \bar0+x'\approx x' \]

所以 \[ N\vdash \forall x(\bar0+x\approx x) \] 再用全称实例化得到 \[ N\vdash \bar0+t\approx t \]

命题 18.2.6 不同数字不等

若 \(m\neq n\)，则 \[ N\vdash \bar m\not\approx \bar n \]

证明： 点击查看证明

不妨设 \(m>n\)。则 \[ \bar m=\overline{m-n}\text{ 个后继作用在 }\bar n\text{ 上} \] 若假设 \[ \bar m\approx \bar n \] 连续使用 (N2) 可以把两边共同的后继剥掉，最后得到某个项的后继等于 \(\bar0\)

例如 \[ \bar3\approx \bar1 \] 即 \[ \bar0'''\approx \bar0' \] 由 (N2) 得 \[ \bar0''\approx \bar0 \] 但 \(\bar0''\) 是某项的后继，由 (N1) 得矛盾

一般情形同理，所以 \[ N\vdash \bar m\not\approx\bar n \]

形式算术 \(K_N\) 的意义是为后面“用公式表达自然数函数和关系”提供了一个形式系统

定义 18.3 可表示函数与可表示关系

开始讨论 \(K_N\) 对自然数性质的表达能力，注意区分：

• 数论函数和数论关系属于元语言中的自然数对象
• \(K_N\) 公式属于形式语言

“可表示”就是把前者翻译成后者

定义 18.3.1 可表示函数

设 \[ f:\mathbb N^k\to\mathbb N \] 是 \(k\) 元数论函数。若存在含有 \(k+1\) 个自由变元的 \(K_N\) 公式 \[ p(x_1,\dots,x_k,y) \] 使得对任意 \(n_1,\dots,n_k,m\in\mathbb N\)：

若 \[ f(n_1,\dots,n_k)=m \] 则 \[ N\vdash p(\bar n_1,\dots,\bar n_k,\bar m) \]

若 \[ f(n_1,\dots,n_k)\neq m \] 则 \[ N\vdash \neg p(\bar n_1,\dots,\bar n_k,\bar m) \]

并且对任意在 \(p\) 中代替 \(y\) 的项 \(t\)，有 \[ N\vdash p(\bar n_1,\dots,\bar n_k,t) \to t\approx \overline{f(n_1,\dots,n_k)} \]

则称 \(f\) 在 \(K_N\) 中可表示，或称 \(p\) 表示 \(f\)

第三个条件表达“输出唯一性”：如果 \(p\) 声称某个项 \(t\) 是输出，那么 \(t\) 必须等于实际输出

第二个条件在有第三个条件时可以推出，但为了后面使用方便，定义中仍把它列出来。

命题 18.3.2 可表示函数的等价判定

函数 \(f\) 可由公式 \(p(x_1,\dots,x_k,y)\) 表示的充分条件是：对任意 \(\vec n=(n_1,\dots,n_k)\)， \[ N\vdash p(\bar n_1,\dots,\bar n_k,\overline{f(\vec n)}) \] 并且 \[ N\vdash p(\bar n_1,\dots,\bar n_k,t)\to t\approx \overline{f(\vec n)} \]

证明： 点击查看证明

只需要从这两个条件推出定义中的“错误值可证否定”

设 \[ f(\vec n)\neq m \] 由命题 18.2.6， \[ N\vdash \bar m\not\approx\overline{f(\vec n)} \]

又由第二个条件，把 \(t\) 取成 \(\bar m\)，有 \[ N\vdash p(\bar n_1,\dots,\bar n_k,\bar m) \to \bar m\approx \overline{f(\vec n)} \]

由换位律和命题逻辑推理可得 \[ N\vdash \neg p(\bar n_1,\dots,\bar n_k,\bar m) \]

所以定义中的错误值条件成立

注记 18.3.3 不是每个公式都表示函数

公式要表示函数，必须对每个输入有唯一输出。例如公式 \[ x_1\approx x_1\wedge y\not\approx y \] 不可能表示任何函数，因为对任意 \(n,m\)， \[ N\vdash \neg(\bar n\approx\bar n\wedge \bar m\not\approx \bar m) \] 它没有输出。

一个公式也不可能表示两个不同函数。若同一公式 \(p\) 同时表示 \(f_1\) 和 \(f_2\)，且存在 \(\vec n\) 使 \[ f_1(\vec n)\neq f_2(\vec n) \] 则由 \(p\) 表示 \(f_1\) 得 \[ N\vdash p(\bar{\vec n},\overline{f_1(\vec n)}) \] 由 \(p\) 表示 \(f_2\) 得 \[ N\vdash \neg p(\bar{\vec n},\overline{f_1(\vec n)}) \] 这会导致 \(N\) 矛盾

这也说明，公式和函数之间不是一一对应

\(K_N\) 的公式只有可数多个，而自然数上的数论函数有不可数多个，所以大量数论函数不能被 \(K_N\) 公式表示

后面真正重要的结论是：凡是递归函数都可表示

定义 18.3.4 投影函数

\(k\) 元投影函数 \(p_i^k\) 定义为 \[ p_i^k(n_1,\dots,n_k)=n_i \qquad (i=1,\dots,k) \]

投影函数在 \(K_N\) 中由公式 \[ x_1\approx x_1\wedge\cdots\wedge x_k\approx x_k\wedge y\approx x_i \] 表示。

命题 18.3.5 加法、乘法和投影函数可表示

二元加法、二元乘法和所有投影函数都在 \(K_N\) 中可表示

证明： 点击查看证明

加法由公式 \[ x_1+x_2\approx y \] 表示。

若 \(n_1+n_2=m\)，由命题 18.2.3 得 \[ N\vdash \bar n_1+\bar n_2\approx\bar m \] 即 \[ N\vdash p(\bar n_1,\bar n_2,\bar m) \]

若 \(n_1+n_2\neq m\)，则由命题 18.2.6 得 \[ N\vdash \bar m\not\approx \overline{n_1+n_2} \] 又由 \[ N\vdash \bar n_1+\bar n_2\approx\overline{n_1+n_2} \] 和等词推理推出 \[ N\vdash \neg(\bar n_1+\bar n_2\approx\bar m) \]

输出唯一性来自等词传递性

乘法用公式 \[ x_1\times x_2\approx y \] 表示，证明同理，用命题 18.2.4

投影函数由定义中的公式表示。若 \(y\) 等于第 \(i\) 个输入，公式可证；若不等，由不同数字不等可证否定；输出唯一性由等词传递性得到

定义 18.3.6 可表示关系

设 \[ R\subseteq\mathbb N^k \] 是 \(k\) 元数论关系。若存在含有 \(k\) 个自由变元的公式 \[ p(x_1,\dots,x_k) \] 使得对任意 \(n_1,\dots,n_k\in\mathbb N\)：

若 \[ (n_1,\dots,n_k)\in R \] 则 \[ N\vdash p(\bar n_1,\dots,\bar n_k) \]

若 \[ (n_1,\dots,n_k)\notin R \] 则 \[ N\vdash \neg p(\bar n_1,\dots,\bar n_k) \]

则称 \(R\) 在 \(K_N\) 中可表示

相等关系可由公式 \[ x_1\approx x_2 \] 表示。

小于等于关系可由公式 \[ \exists z(z+x_1\approx x_2) \] 表示，因为 \(n_1\le n_2\) 当且仅当存在 \(z\) 使 \[ z+n_1=n_2 \]

小于关系可由 \[ \exists z(z'+x_1\approx x_2) \] 表示。

定义 18.3.7 特征函数

关系 \(R\subseteq\mathbb N^k\) 的特征函数 \(C_R\) 定义为 \[ C_R(n_1,\dots,n_k)= \begin{cases} 1, & (n_1,\dots,n_k)\in R\\ 0, & (n_1,\dots,n_k)\notin R \end{cases} \]

特征函数把关系问题转化成函数问题

命题 18.3.8 关系可表示当且仅当特征函数可表示

\(k\) 元关系 \(R\) 可表示，当且仅当它的特征函数 \(C_R\) 可表示。

证明： 点击查看证明

先设 \(R\) 由公式 \(p(x_1,\dots,x_k)\) 表示。定义公式 \[ q(x_1,\dots,x_k,y) \equiv \bigl(p(x_1,\dots,x_k)\wedge y\approx\bar1\bigr) \vee \bigl(\neg p(x_1,\dots,x_k)\wedge y\approx\bar0\bigr) \]

若 \(\vec n\in R\)，则 \(N\vdash p(\bar{\vec n})\)，并且 \[ C_R(\vec n)=1 \] 所以 \[ N\vdash q(\bar{\vec n},\bar1) \]

若 \(\vec n\notin R\)，则 \(N\vdash\neg p(\bar{\vec n})\)，并且 \[ C_R(\vec n)=0 \] 所以 \[ N\vdash q(\bar{\vec n},\bar0) \] 错误输出的否定和输出唯一性由 \(\bar0\not\approx\bar1\) 以及等词推理得到。因此 \(C_R\) 可表示

反过来，若 \(C_R\) 由公式 \(q(x_1,\dots,x_k,y)\) 表示，则 \(R\) 由公式 \[ q(x_1,\dots,x_k,\bar1) \] 表示

若 \(\vec n\in R\)，则 \(C_R(\vec n)=1\)，所以 \[ N\vdash q(\bar{\vec n},\bar1) \]

若 \(\vec n\notin R\)，则 \(C_R(\vec n)=0\)，由错误值条件得 \[ N\vdash \neg q(\bar{\vec n},\bar1) \]

所以 \(R\) 可表示

定义 18.4 复合与 \(\mu\) 算子保持可表示性

先证明两个技术结论：函数复合保持可表示性，最小数算子 \(\mu\) 保持可表示性

定理 18.4.1 函数复合保持可表示性

设 \(j\) 元函数 \(g\) 和 \(j\) 个 \(k\) 元函数 \[ h_1,\dots,h_j \] 都在 \(K_N\) 中可表示。定义 \[ f(\vec n)=g(h_1(\vec n),\dots,h_j(\vec n)) \] 则 \(f\) 也在 \(K_N\) 中可表示。

证明： 点击查看证明

设 \(g\) 由公式 \[ q(y_1,\dots,y_j,y) \] 表示，\(h_i\) 由公式 \[ r_i(x_1,\dots,x_k,y_i) \] 表示。

定义公式 \[ P(\vec x,y)\equiv \exists y_1\cdots\exists y_j \left( \bigwedge_{i=1}^{j}r_i(\vec x,y_i) \wedge q(y_1,\dots,y_j,y) \right) \]

若 \[ f(\vec n)=m \] 令 \[ a_i=h_i(\vec n) \] 则由 \(h_i\) 可表示性， \[ N\vdash r_i(\bar{\vec n},\bar a_i) \] 又由 \(g\) 可表示性， \[ N\vdash q(\bar a_1,\dots,\bar a_j,\bar m) \] 所以逐次使用存在引入得 \[ N\vdash P(\bar{\vec n},\bar m) \]

若 \(P(\bar{\vec n},t)\) 成立，由各 \(r_i\) 的输出唯一性可推出 \[ y_i\approx \overline{h_i(\vec n)} \] 再由 \(q\) 的输出唯一性推出 \[ t\approx \overline{g(h_1(\vec n),\dots,h_j(\vec n))} \] 即 \[ t\approx\overline{f(\vec n)} \]

由命题 18.3.2，\(P\) 表示 \(f\)

定义 18.4.2 最小数算子 \(\mu\)

设 \(g(\vec n,x)\) 是 \(k+1\) 元函数。若对每个 \(\vec n\) 都存在自然数 \(x\) 使 \[ g(\vec n,x)=0 \] 则定义 \[ f(\vec n)=\mu x[g(\vec n,x)=0] \] 为使 \(g(\vec n,x)=0\) 成立的最小 \(x\)

这个 \(x\) 称为方程 \[ g(\vec n,x)=0 \] 的根，而且有最小性： \[ g(\vec n,f(\vec n))=0 \] 并且 \[ g(\vec n,x)=0\to f(\vec n)\le x \]

若不要求根总是存在，则 \(\mu\) 算子可能产生部分函数。汪芳庭在定义递归函数时先讨论处处有定义的函数，因此使用 \(\mu\) 算子时常附带“根存在性条件”

定理 18.4.3 \(\mu\) 算子保持可表示性

若 \(g(\vec n,x)\) 在 \(K_N\) 中可表示，并且对每个 \(\vec n\) 都存在 \(x\) 使 \[ g(\vec n,x)=0 \] 则 \[ f(\vec n)=\mu x[g(\vec n,x)=0] \] 也在 \(K_N\) 中可表示。

证明： 点击查看证明

设 \(g\) 由公式 \[ q(x_1,\dots,x_k,z,y) \] 表示，其中 \(y\) 是函数值位置。也就是说， \[ q(\vec x,z,\bar0) \] 表达 \[ g(\vec x,z)=0 \]

定义公式 \[ P(\vec x,z)\equiv q(\vec x,z,\bar0) \wedge \forall u\bigl(q(\vec x,u,\bar0)\to z\le u\bigr) \] 其中 \[ z\le u \] 用已经可表示的小于等于公式表示。

若 \[ f(\vec n)=r \] 则 \(g(\vec n,r)=0\)，且对任意 \(u\)，若 \(g(\vec n,u)=0\)，则 \(r\le u\)。由 \(g\) 和 \(\le\) 的可表示性得 \[ N\vdash P(\bar{\vec n},\bar r) \]

若 \(P(\bar{\vec n},t)\) 成立，则 \(t\) 是一个根，并且不大于任何根。由于 \(f(\vec n)\) 是最小根，\(t\) 必须等于 \[ \overline{f(\vec n)} \] 这个等式可在 \(N\) 中由数字大小关系的可表示性推出。

所以 \(P\) 表示 \(f\)

定义 18.5 递归函数

暂时离开形式系统 \(K_N\)，在自然数函数本身上建立“递归函数”的概念。为后面证明“递归函数都能在 \(K_N\) 中表示”做准备

定义 18.5.1 递归函数的一般定义

递归函数从三个基本函数出发。

零函数： \[ z(n)=0 \]

后继函数： \[ s(n)=n+1 \]

投影函数： \[ p_i^k(n_1,\dots,n_k)=n_i \]

然后允许有限次使用以下三条规则

规则 I：复合。若 \[ g,\ h_1,\dots,h_j \] 已经得到，则 \[ f(\vec n)=g(h_1(\vec n),\dots,h_j(\vec n)) \] 也得到

规则 II：递归。若 \(g\) 是 \(k\) 元函数，\(h\) 是 \(k+2\) 元函数，则定义 \(k+1\) 元函数 \(f\)： \[ f(n_1,\dots,n_k,0)=g(n_1,\dots,n_k) \] \[ f(n_1,\dots,n_k,n+1)= h(n_1,\dots,n_k,n,f(n_1,\dots,n_k,n)) \]

规则 III：\(\mu\) 算子。若 \(g\) 是 \(k+1\) 元函数，并且对任意 \(n_1,\dots,n_k\) 都存在 \(x\) 使 \[ g(n_1,\dots,n_k,x)=0 \] 则定义 \[ f(n_1,\dots,n_k)=\mu x[g(n_1,\dots,n_k,x)=0] \]

由基本函数经过有限次规则 I、II、III 得到的函数称为递归函数或一般递归函数

若只允许规则 I 和规则 II，不允许规则 III，则得到的函数称为原始递归函数

若去掉规则 III 中的根存在性要求，则可能得到不处处有定义的函数，这类函数称为递归偏函数或部分递归函数

例 18.5.2 常值函数

\(k\) 元常值函数 \[ c_m(n_1,\dots,n_k)=m \] 是递归函数

证明： 点击查看证明

先构造 \(c_0\)： \[ c_0(n_1,\dots,n_k)=z(p_1^k(n_1,\dots,n_k)) \] 这是零函数和投影函数的复合。

若 \(c_m\) 已经得到，则 \[ c_{m+1}=s\circ c_m \] 也得到

所以对 \(m\) 作归纳，所有常值函数都是递归函数

例 18.5.3 加法和乘法是递归函数

加法由递归规则定义： \[ n_1+0=p_1^1(n_1) \] \[ n_1+(n+1)=s(p_3^3(n_1,n,n_1+n)) \]

换成更熟悉的写法就是： \[ n_1+0=n_1 \] \[ n_1+(n+1)=(n_1+n)+1 \]

乘法由递归规则定义： \[ n_1\times0=z(n_1) \] \[ n_1\times(n+1)=p_3^3(n_1,n,n_1\times n)+p_1^3(n_1,n,n_1\times n) \] 即 \[ n_1\times0=0 \] \[ n_1\times(n+1)=n_1\times n+n_1 \]

因为加法已经递归，所以乘法也递归

例 18.5.4 前驱函数和截差函数

前驱函数定义为 \[ p^{-}(n)= \begin{cases} 0, & n=0\\ n-1, & n>0 \end{cases} \]

它递归，因为 \[ p^{-}(0)=0 \] \[ p^{-}(n+1)=n=p_1^2(n,p^{-}(n)) \]

截差函数定义为 \[ n_1\mathbin{\dot-} n_2= \begin{cases} n_1-n_2, & n_1\ge n_2\\ 0, & n_1<n_2 \end{cases} \]

它递归，因为 \[ n_1\dotminus0=n_1 \] \[ n_1\dotminus(n+1)=p^{-}(n_1\dotminus n) \]

前驱函数还可以写成 \[ p^{-}(n)=n\dotminus1 \]

例 18.5.5 符号函数

定义 \[ \operatorname{sg}(n)= \begin{cases} 0, & n=0\\ 1, & n>0 \end{cases} \]

以及 \[ \overline{\operatorname{sg}}(n)= \begin{cases} 1, & n=0\\ 0, & n>0 \end{cases} \]

\(\operatorname{sg}\) 是递归的，因为 \[ \operatorname{sg}(0)=0 \] \[ \operatorname{sg}(n+1)=1 \]

而 \[ \overline{\operatorname{sg}}(n)=1\dotminus \operatorname{sg}(n) \] 所以 \(\overline{\operatorname{sg}}\) 也是递归函数。

这两个函数常用来构造关系的特征函数。例如 \[ C_{=}(n_1,n_2)=\overline{\operatorname{sg}}(|n_1-n_2|) \]

命题 18.5.6 变元重排、减元和增元

若 \(f\) 是 \(k\) 元递归函数，则由 \[ g(n_1,\dots,n_l)=f(n_{m_1},\dots,n_{m_k}) \] 定义的 \(l\) 元函数也是递归函数，其中每个 \(m_i\) 满足 \[ 1\le m_i\le l \]

证明： 点击查看证明

因为 \[ n_{m_i}=p_{m_i}^{\,l}(n_1,\dots,n_l) \] 所以 \[ g(\vec n)=f(p_{m_1}^{\,l}(\vec n),\dots,p_{m_k}^{\,l}(\vec n)) \] 是 \(f\) 与投影函数的复合。

投影函数递归，递归函数对复合封闭，所以 \(g\) 递归。

这个命题常用来“减元”“换元”和“增元”。例如三元函数 \(f\) 可以得到： \[ u(n_1,n_2)=f(n_1,n_2,n_2) \] \[ g(n_1,n_2)=f(n_1,n_1,n_2) \] \[ h(n_1,n_2,n_3,n_4)=f(n_3,n_1,n_4) \] 这些都仍是递归函数。

例 18.5.7 常用递归函数

绝对差： \[ |n_1-n_2|=(n_1\dotminus n_2)+(n_2\dotminus n_1) \] 所以递归。

最小值： \[ \min(n_1,n_2)=n_1\dotminus(n_1\dotminus n_2) \] 多元最小值递归地定义为 \[ \min(n_1,\dots,n_k)=\min(\min(n_1,\dots,n_{k-1}),n_k) \] 最大值同理可由 \[ \max(n_1,n_2)=n_1+(n_2\dotminus n_1) \] 得到。

指数函数可递归定义为 \[ n^0=\overline{\operatorname{sg}}(n) \] 这里约定 \(0^0=0\)，并且 \[ n^{m+1}=n^m\times n \]

余数函数 \(\operatorname{rem}(n_1,n_2)\) 表示用 \(n_1\) 除 \(n_2\) 后所得余数，约定 \(n_1=0\) 时余数为 \(0\)。它可用递归定义： \[ \operatorname{rem}(n_1,0)=0 \] \[ \operatorname{rem}(n_1,n+1)= (\operatorname{rem}(n_1,n)+1)\, \operatorname{sg}\bigl(n_1\dotminus(\operatorname{rem}(n_1,n)+1)\bigr) \] 这表示余数每次加一；若已经达到除数，就回到 \(0\)。

命题 18.5.8 有界求和和有界求积保持递归性

设 \(f(\vec n,i)\) 是 \(k+1\) 元递归函数。定义 \[ g(\vec n)=\sum_{i\le n_k}f(n_1,\dots,n_{k-1},i) \] 和 \[ h(\vec n,m)=\sum_{i\le m}f(\vec n,i) \] 则 \(g,h\) 都是递归函数。

类似地，有界求积 \[ \prod_{i\le m}f(\vec n,i) \] 也是递归函数。

证明： 点击查看证明

以有界求和为例。

定义 \[ h(\vec n,0)=f(\vec n,0) \] \[ h(\vec n,m+1)=h(\vec n,m)+f(\vec n,m+1) \] 因为加法和 \(f\) 都递归，所以由递归规则可知 \(h\) 递归。

再令 \[ g(n_1,\dots,n_k)=h(n_1,\dots,n_{k-1},n_k) \] 由复合可知 \(g\) 递归。

有界求积把基础步改为 \[ h(\vec n,0)=f(\vec n,0) \] 递推步改为 \[ h(\vec n,m+1)=h(\vec n,m)\times f(\vec n,m+1) \] 即可。

定义 18.6 递归关系与递归集

汪芳庭第 3.4.2 节用特征函数定义递归关系。

定义 18.6.1 递归关系

设 \[ R\subseteq\mathbb N^k \] 是 \(k\) 元关系。若它的特征函数 \(C_R\) 是递归函数，则称 \(R\) 是递归关系。

一元递归关系也称为 \(\mathbb N\) 的递归子集，简称递归集。

例 18.6.2 基本递归关系

关系 \(\le\)、\(=\)、\(<\) 都是递归关系。

事实上： \[ C_{\le}(n_1,n_2)=\overline{\operatorname{sg}}(n_1\mathbin{\dot-} n_2) \]

因为 \(n_1\le n_2\) 当且仅当 \(n_1\mathbin{\dot-} n_2=0\)

相等关系可写为 \[ C_{=}(n_1,n_2)= \overline{\operatorname{sg}}(|n_1-n_2|) \]

小于关系可写为 \[ C_{<}(n_1,n_2)=C_{\le}(n_1+1,n_2) \]

命题 18.6.3 递归关系的闭包性质

若 \(R,R_1,R_2\) 是 \(k\) 元递归关系，则：

• 补关系 \(\overline R\) 是递归关系
• 并关系 \(R_1\cup R_2\) 是递归关系
• 交关系 \(R_1\cap R_2\) 是递归关系

证明： 点击查看证明

由特征函数计算： \[ C_{\overline R}(\vec n)=1\mathbin{\dot-} C_R(\vec n) \]

并关系： \[ C_{R_1\cup R_2}(\vec n) = \operatorname{sg}(C_{R_1}(\vec n)+C_{R_2}(\vec n)) \]

交关系： \[ C_{R_1\cap R_2}(\vec n) = C_{R_1}(\vec n)\times C_{R_2}(\vec n) \]

右边都是递归函数的复合，所以仍递归。

命题 18.6.4 有界量词保持递归性

设 \(R(\vec n,x)\) 是 \(k+1\) 元递归关系。定义 \[ Q(\vec n,m)\iff \exists x<m\,R(\vec n,x) \] 则 \(Q\) 是递归关系。

同理， \[ P(\vec n,m)\iff \forall x<m\,R(\vec n,x) \] 也是递归关系。

证明： 点击查看证明

存在量词情形： \[ C_Q(\vec n,m)= \operatorname{sg}\left(\sum_{x<m}C_R(\vec n,x)\right) \] 有界求和保持递归性，所以 \(C_Q\) 递归。

全称量词情形可用补关系和有界存在表示： \[ \forall x<m\,R(\vec n,x) \iff \neg\exists x<m\,\neg R(\vec n,x) \] 由递归关系对补和有界存在封闭，得 \(P\) 递归。

例 18.6.5 有限集、整除关系和素数集

空集、全集、单点集和有限集都是递归集。比如 \[ C_{\{a\}}(n)=C_{=}(n,a) \] 有限集 \[ \{a_1,\dots,a_l\} \] 是若干单点集的并。

整除关系 \[ \operatorname{Divi}(n_1,n_2) \iff n_1=0\text{ 或 }n_1\text{ 能整除 }n_2 \] 也是递归关系。可用余数函数写为 \[ C_{\operatorname{Divi}}(n_1,n_2) = \overline{\operatorname{sg}}(\operatorname{rem}(n_1,n_2)) \]

素数集 \(\operatorname{Prm}\) 也是递归集。一个数 \(n>1\) 是素数，当且仅当在不大于 \(n\) 的数中，它的因子只有 \(1\) 和自身。可用有界求和表达“因子个数不超过两个”。因此素数的特征函数是递归函数

第 \(n\) 个素数函数 \(p(n)\) 也递归： \[ p(0)=2 \] \[ p(n+1)=\mu x\,[\,p(n)<x\wedge x\in \operatorname{Prm}\,] \] 这里右边的条件是递归关系，并且根存在，所以由 \(\mu\) 算子得到递归函数。

定义 18.7 递归函数的可表示性

回到数论函数与 \(K_N\) 公式的关系。

\[ \mathrm{REP}=\{f\mid f\text{ 在 }K_N\text{ 中可表示}\} \]

\[ \mathrm{REC}=\{f\mid f\text{ 是递归函数}\} \]

还定义一个辅助类 \(\mathrm{REC}^\ast\)：从加法、乘法、投影函数、关系 \(\le\) 的特征函数出发，经过有限次复合和 \(\mu\) 算子得到的函数全体

使用 \(\mathrm{REC}^\ast\) 的原因是：加法、乘法、投影函数和 \(\le\) 的特征函数已经容易证明可表示；而复合和 \(\mu\) 又保持可表示性

命题 18.7.1 \(\mathrm{REC}^\ast\subseteq \mathrm{REC}\)

辅助类 \(\mathrm{REC}^\ast\) 中的每个函数都是递归函数

证明： 点击查看证明

加法、乘法和投影函数已经在 18.5 中证明递归

关系 \(\le\) 的特征函数 \[ C_{\le}(n_1,n_2)=\overline{\operatorname{sg}}(n_1\mathbin{\dot-} n_2) \] 也是递归函数。

递归函数对复合封闭，对满足根存在条件的 \(\mu\) 算子封闭

所以由这些函数有限次构造出的 \(\mathrm{REC}^\ast\) 函数都递归

命题 18.7.2 \(\mathrm{REC}^\ast\subseteq \mathrm{REP}\)

辅助类 \(\mathrm{REC}^\ast\) 中的每个函数都在 \(K_N\) 中可表示。

证明： 点击查看证明

加法、乘法和投影函数可表示，见命题 18.3.5。

关系 \(\le\) 可表示，故其特征函数可表示，见命题 18.3.8。

由定理 18.4.1，复合保持可表示性。

由定理 18.4.3，\(\mu\) 算子保持可表示性。

因此从这些初始函数出发有限次构造出的函数都可表示，即 \[ \mathrm{REC}^\ast\subseteq \mathrm{REP} \]

命题 18.7.3 \(\mathrm{REC}\subseteq \mathrm{REC}^\ast\)

每个递归函数都属于 \(\mathrm{REC}^\ast\)

证明： 点击查看证明

关键在于说明递归定义可以用 \(\mathrm{REC}^\ast\) 中允许的构造模拟

设 \(f\) 由原始递归给出： \[ f(\vec n,0)=g(\vec n) \] \[ f(\vec n,y+1)=h(\vec n,y,f(\vec n,y)) \]

要计算 \(f(\vec n,y)\)，只需知道有限序列 \[ a_0,a_1,\dots,a_y \] 其中 \[ a_0=g(\vec n) \] \[ a_{i+1}=h(\vec n,i,a_i) \] 最后输出 \(a_y\)

有限序列可以用素数幂编码为一个自然数： \[ \langle a_0,\dots,a_y\rangle = 2^{a_0+1}3^{a_1+1}\cdots p_y^{a_y+1} \] 序列长度、取第 \(i\) 项、检查某数是否为这样的计算过程编码，都是可以由加法、乘法、\(\le\)、复合和 \(\mu\) 表达出来的函数或关系，因此属于 \(\mathrm{REC}^\ast\)

于是可定义一个 \(\mathrm{REC}^\ast\) 关系： \[ H(\vec n,y,s) \] 表示“\(s\) 编码了从 \(0\) 到 \(y\) 的正确计算过程”。再用 \(\mu\) 找到某个这样的 \(s\)，最后取出第 \(y\) 项

这说明原始递归规则可以在 \(\mathrm{REC}^\ast\) 中模拟

基本函数也都属于 \(\mathrm{REC}^\ast\)：零函数可由 \[ z(n)=C_{\le}(n+1,n) \] 得到，后继函数可由 \[ s(n)=n+1 \] 得到，投影函数本来就是初始函数。

因此所有递归函数都属于 \(\mathrm{REC}^\ast\)

定理 18.7.4 递归函数可表示性定理

每个递归函数都在 \(K_N\) 中可表示。

也就是 \[ \mathrm{REC}\subseteq \mathrm{REP} \]

证明： 点击查看证明

由命题 18.7.3， \[ \mathrm{REC}\subseteq \mathrm{REC}^\ast \] 由命题 18.7.2， \[ \mathrm{REC}^\ast\subseteq \mathrm{REP} \] 所以 \[ \mathrm{REC}\subseteq \mathrm{REP} \]

这就是 Gödel 不完备性定理所需的重要桥梁：凡是递归可计算的数论函数，都能变成 \(K_N\) 中的公式

推论 18.7.5 递归关系可表示

每个递归关系都在 \(K_N\) 中可表示

证明： 点击查看证明

若 \(R\) 是递归关系，则它的特征函数 \(C_R\) 是递归函数

由递归函数可表示性定理，\(C_R\) 在 \(K_N\) 中可表示

由命题 18.3.8，\(R\) 可表示

定义 18.8 对 \(K_N\) 的递归分析

对 \(K_N\) 自身的语法做递归分析。前面已经知道递归关系可表示，现在要证明：关于 \(K_N\) 公式、项、替换、证明的许多语法关系本身就是递归关系

这一步把形式系统变成自然数对象。完成之后，“某个数是公式的 Gödel 数”“某个数是证明的 Gödel 数”“某个公式可证”都能写成算术公式

定义 18.8.1 前置式与唯一读法

为了方便分析，把项和公式先写成前置式。例如：

\[ t_1+t_2 \] 写成 \[ +t_1t_2 \]

\[ t_1\times t_2 \] 写成 \[ \times t_1t_2 \]

\[ t_1\approx t_2 \] 写成 \[ \approx t_1t_2 \]

\[ p\to q \] 写成 \[ \to pq \]

前置式的好处是括号可以省略，但仍然能唯一恢复结构

给字母规定权重： \[ w(x_i)=w(\bar0)=1 \] \[ w(')=w(\neg)=0 \] \[ w(+)=w(\times)=w(\approx)=w(\to)=w(\forall)=-1 \]

字母串 \(u_1\cdots u_n\) 的权重定义为 \[ w(u_1\cdots u_n)=w(u_1)+\cdots+w(u_n) \]

命题 18.8.2 唯一读法引理

在 \(K_N\) 的前置式中：

1. 若字母串构成项或公式，则其总权重为 \(1\)
2. 一个项或公式的任一真前段都不是项或公式
3. 若一个字母串可由两个项或两个公式拼接而成，则拼接方式唯一

证明： 点击查看证明

第一点对项和公式的构造作归纳

基本项 \(x_i\) 和 \(\bar0\) 的权重都是 \(1\)

若 \(t\) 是项，则 \(t'\) 的权重为 \[ w(t')=w(')+w(t)=0+1=1 \]

若 \(t_1,t_2\) 是项，则 \[ w(+t_1t_2)=-1+1+1=1 \] 乘法项同理

若 \(t_1,t_2\) 是项，则原子公式 \[ \approx t_1t_2 \] 权重为 \[ -1+1+1=1 \]

否定公式 \(\neg p\) 权重为 \[ 0+1=1 \] 蕴涵公式 \(\to pq\) 权重为 \[ -1+1+1=1 \] 全称公式 \(\forall x_i p\) 中，\(\forall\) 的权重为 \(-1\)，\(x_i\) 的权重为 \(1\)，\(p\) 的权重为 \(1\)，总和仍为 \(1\)

第二点也对构造归纳。直观上，前置式的开头符号已经决定后面需要几个完整成分；在完整成分没有读完以前，权重不会回到 \(1\)。例如 \(+t_1t_2\) 的真前段要么还没读完 \(t_1\)，要么读完 \(t_1\) 但还没读完 \(t_2\)，都不可能是完整项

第三点由第二点推出。若同一字母串既能分为 \(t_1t_2\)，又能分为 \(s_1s_2\)，且 \(t_1\) 与 \(s_1\) 长度不同，那么较短者就是较长者的真前段，但二者都是项或公式，矛盾。因此第一段相同，第二段也相同

所以前置式具有唯一读法

唯一读法引理保证我们可以机械判定一个有限字母串是不是项或公式，并且能机械地拆出它的组成部分

定义 18.8.3 Gödel 数

Gödel 数是把符号串编码为自然数的方法。

汪芳庭给每个基本字母分配一个奇数编码：

\[ \begin{array}{c|ccccccccc} u&'&+&\times&\neg&\to&\forall&\approx&\bar0&x_i\\ \hline g(u)&1&3&5&7&9&11&13&15&15+2i \end{array} \]

不同字母有不同的 Gödel 数，而且全是奇数

若字母串为 \[ u_0u_1\cdots u_k \] 则定义其 Gödel 数为 \[ g(u_0u_1\cdots u_k) = 2^{g(u_0)}3^{g(u_1)}\cdots p_k^{g(u_k)} \] 其中 \(p_k\) 是第 \(k+1\) 个素数

由于自然数素因子分解唯一，不同字母串的 Gödel 数不同

反过来，给定一个自然数，只需分解它的素因子，就能判断它是否是某个字母串的 Gödel 数，并恢复该字母串

如果要编码一个字母串的有限序列 \[ s_0,s_1,\dots,s_n \] 则再用同样方式编码： \[ g(s_0,\dots,s_n)= 2^{g(s_0)}3^{g(s_1)}\cdots p_n^{g(s_n)} \]

这里要注意两个层次：

• 一个公式作为字母串有 Gödel 数
• 一个公式序列作为有限序列也有 Gödel 数

同一个形式对象在不同层次出现时，编码方式不同，但每次使用时都能从上下文判断其身份

定义 18.8.4 过程值递归

为了处理公式序列和证明序列，需要能递归地操作有限序列的编码。常用操作包括：

• 判断 \(n\) 是否为某个有限序列的编码
• 取序列长度
• 取序列第 \(i\) 项
• 把两个序列拼接
• 在项或公式中进行替换

这些都基于素数幂编码。

例如，若 \[ s=2^{a_0+1}3^{a_1+1}\cdots p_k^{a_k+1} \] 则“第 \(i\) 项为 \(a_i\)”可以通过判断 \(p_i\) 在 \(s\) 的素因子分解中的指数得到。素数集、第 \(i\) 个素数、整除关系、余数函数都已经是递归对象，所以取项函数也是递归的。

过程值递归的基本形式是：若某函数的计算过程可以写成有限序列，并且每一步是否正确可递归检查，那么整个函数可由“寻找一个正确过程编码，再读取最后一项”得到。

这正是前面证明原始递归能被 \(\mathrm{REC}^\ast\) 模拟的技术基础。

命题 18.8.5 语法对象的 Gödel 数集合是递归集

以下集合都是递归集：

• \(\mathrm{VS}\)：个体变元作为独立字母串的 Gödel 数集合
• \(\mathrm{TM}\)：所有 \(K_N\) 项的 Gödel 数集合
• \(\mathrm{YF}\)：所有原子公式的 Gödel 数集合
• \(\mathrm{FM}\)：所有 \(K_N\) 公式的 Gödel 数集合

证明： 点击查看证明

\(\mathrm{VS}\) 最简单。由编码表， \[ g(x_i)=15+2i \] 作为独立字母串的 Gödel 数为 \[ 2^{15+2i} \] 因此 \[ n\in\mathrm{VS} \iff \exists i<n\, (n=2^{15+2i}) \] 这是有界存在形式，故递归。

\(\mathrm{TM}\) 可按项的构造给出递归判定：

• \(\bar0\) 是项
• 变元是项
• 若 \(x\) 是项，则 \('x\) 是项
• 若 \(x,y\) 是项，则 \(+xy\) 和 \(\times xy\) 是项

由于前置式唯一读法保证一个串的最外层构造可以唯一判定，所以“\(n\) 是项的 Gödel 数”可递归判定。

\(\mathrm{YF}\) 只有原子公式 \[ \approx t_1t_2 \] 所以只需检查最外层符号是否为 \(\approx\)，并递归检查后面两个成分是否为项。

\(\mathrm{FM}\) 按公式构造判定：

• 原子公式是公式
• 若 \(p\) 是公式，则 \(\neg p\) 是公式
• 若 \(p,q\) 是公式，则 \(\to pq\) 是公式
• 若 \(x_i\) 是变元且 \(p\) 是公式，则 \(\forall x_i p\) 是公式

同样由唯一读法，最外层构造可机械拆分，所以 \(\mathrm{FM}\) 是递归集。

定义 18.8.6 替换关系和 Sub 函数

后面构造自指公式时，需要把一个公式中的自由变元替换为某个数字。设 \[ \mathrm{Sub}(n_1,n_2,n_3) \] 表示如下函数关系：

\(n_1\) 是某个变元的 Gödel 数，\(n_2\) 是某个项或公式的 Gödel 数，\(n_3\) 是替换进去的项的 Gödel 数，输出是把 \(n_2\) 中自由出现的 \(n_1\) 全部替换为 \(n_3\) 后所得对象的 Gödel 数。

汪芳庭先分析一个三元递归关系 \(\mathrm{SBS}\)，表示“替换结果正确”。其证明按项和公式的构造分类型：

• 若对象本身就是要替换的变元，则替换结果就是新项
• 若对象是其他变元或常元，则替换结果不变
• 若对象是 \(t'\)、\(\neg p\)，则递归替换内部对象
• 若对象是 \(t_1+t_2\)、\(t_1\times t_2\)、\(t_1\approx t_2\)、\(p\to q\)，则分别替换两个子对象
• 若对象是 \(\forall x_i p\)，则当 \(x_i\) 正是被替换变元时不进入量词内部，否则替换公式 \(p\)

因为唯一读法保证这些情形互不混淆，并且每个子对象的 Gödel 数都小于整体 Gödel 数，所以该替换关系是递归关系。

于是替换函数 \[ \mathrm{Sub}(n_1,n_2,n_3) \] 也是递归函数。

特别地，令 \[ \mathrm{Num}(n)=g(\bar n) \] 表示自然数 \(n\) 的数码 \(\bar n\) 的 Gödel 数，则 \[ \mathrm{Num} \] 也是递归函数。

命题 18.8.7 证明关系是递归关系

设 \(\mathrm{PRF}(x,y)\) 表示：

\(x\) 是 \(K_N\) 中公式 \(y\) 的一个证明的 Gödel 数。

则 \(\mathrm{PRF}\) 是递归关系。

证明： 点击查看证明

给定 \(x,y\)，先把 \(x\) 解码为一个有限公式序列： \[ A_0,A_1,\dots,A_m \] 若解码失败，则不是证明。

若解码成功，逐项检查：

1. 每个 \(A_i\) 是否是公式，即其 Gödel 数是否在 \(\mathrm{FM}\) 中。
2. 最后一项是否等于 \(y\)。
3. 每个 \(A_i\) 是否是逻辑公理、等词公理、算术公理，或是否能由前面若干项按 MP、Gen 等规则推出。

逻辑公理模式、等词公理模式、算术公理模式的 Gödel 数集合都是递归集。推理规则只涉及有限位置的公式匹配，也可递归检查。

所以 \(\mathrm{PRF}(x,y)\) 是递归关系。

推论 18.8.8 可证公式集递归可枚举

令 \[ \mathrm{PA}=\{y\mid \exists x\,\mathrm{PRF}(x,y)\} \] 即 \(K_N\) 中可证公式的 Gödel 数集合。则 \(\mathrm{PA}\) 是递归可枚举集。

证明： 点击查看证明

枚举自然数 \[ x=0,1,2,\dots \] 对每个 \(x\)，检查它是否是某个证明的 Gödel 数。若是，并且其最后公式的 Gödel 数为 \(y\)，就输出 \(y\)。

由于 \(\mathrm{PRF}\) 是递归关系，每一步检查有限完成。

所有可证公式都有某个有限证明，因此最终会被枚举出来。

定义 18.9 Gödel 不完备性定理

第 4 章开始讨论不完备性。汪芳庭书先明确两个概念：完备性和 \(\omega\)-无矛盾。

一个公式集 \(\Gamma\) 称为完备的，若对任意闭式 \(p\)，都有 \[ \Gamma\vdash p \] 或 \[ \Gamma\vdash \neg p \]

也就是说，每个句子都能被 \(\Gamma\) 判定。

定义 18.9.1 \(\omega\)-无矛盾

公式集 \(\Gamma\) 称为 \(\omega\)-无矛盾，若不存在只含一个自由变元 \(x\) 的公式 \(p(x)\)，使得下面两件事同时成立：

对每个自然数 \(n\)， \[ \Gamma\vdash p(\bar n) \]

同时 \[ \Gamma\vdash \neg\forall x\,p(x) \]

直观地说，\(\omega\)-无矛盾排除了这种情况：系统逐个证明 \[ p(\bar0),p(\bar1),p(\bar2),\dots \] 却又证明“并非所有 \(x\) 都满足 \(p(x)\)”。

命题 18.9.2 \(\omega\)-无矛盾推出无矛盾

若 \(\Gamma\) 是 \(\omega\)-无矛盾的，则 \(\Gamma\) 是无矛盾的。

证明： 点击查看证明

反证。若 \(\Gamma\) 有矛盾，则在经典逻辑中，任意公式都可由 \(\Gamma\) 证明。

取任意公式 \(p(x)\)。因为 \(\Gamma\) 有矛盾，所以对每个 \(n\)， \[ \Gamma\vdash p(\bar n) \] 同时也有 \[ \Gamma\vdash \neg\forall x\,p(x) \]

这正是 \(\omega\)-矛盾。

所以若 \(\Gamma\) 是 \(\omega\)-无矛盾，它必定无矛盾。

定义 18.9.3 Gödel 关系 \(W\)

为了构造自指句，定义二元关系 \(W\)： \[ W=\{(n_1,n_2)\mid n_1\text{ 是某公式 }p(x_1)\text{ 的 Gödel 数，且 } n_2\text{ 是 }p(\bar n_1)\text{ 从 }N\text{ 的证明的 Gödel 数} \} \]

换句话说，\(W(n_1,n_2)\) 表示：

“\(n_2\) 是把 \(n_1\) 所编码公式自代入后所得公式的一个证明。”

利用上一节的递归分析，可以写成： \[ (n_1,n_2)\in W \iff n_1\in \mathrm{FM} \wedge \mathrm{PRF}\bigl(n_2,\mathrm{Sub}(g(x_1),n_1,\mathrm{Num}(n_1))\bigr) \]

其中 \(g(x_1)\) 是变元 \(x_1\) 的 Gödel 数，\(\mathrm{Num}(n_1)\) 是数码 \(\bar n_1\) 的 Gödel 数。

因此 \(W\) 是递归关系。由递归关系可表示性，存在 \(K_N\) 公式 \[ w(x_1,x_2) \] 表示 \(W\)。

定义 18.9.4 Gödel 句

令 \[ p(x_1)\equiv \forall x_2\,\neg w(x_1,x_2) \]

设 \(p(x_1)\) 的 Gödel 数为 \[ m=g(p(x_1)) \]

把自己的 Gödel 数代入，得到闭式 \[ p(\bar m) \] 即 \[ \forall x_2\,\neg w(\bar m,x_2) \]

它的直观含义是：

不存在自然数 \(x_2\)，使 \(x_2\) 是 \(p(\bar m)\) 从 \(N\) 的证明的 Gödel 数。

也就是说，\(p(\bar m)\) 在说：

\[ \text{“我在 }N\text{ 中不可证。”} \]

定理 18.9.5 Gödel 第一不完备性定理

设 \(N\) 是形式算术 \(K_N\) 的算术公理集。

1. 若 \(N\) 无矛盾，则 \[ N\not\vdash p(\bar m) \]

2. 若 \(N\) 是 \(\omega\)-无矛盾的，则 \[ N\not\vdash \neg p(\bar m) \]

因此若 \(N\) 是 \(\omega\)-无矛盾的，则 \(N\) 不完备。

证明： 点击查看证明

先证明第一点。

反设 \[ N\vdash p(\bar m) \] 设 \(n\) 是这个证明的 Gödel 数。由 \(W\) 的定义， \[ (m,n)\in W \] 因为 \(w\) 表示 \(W\)，所以 \[ N\vdash w(\bar m,\bar n) \]

另一方面，由 \[ p(\bar m)\equiv \forall x_2\,\neg w(\bar m,x_2) \] 和 \[ N\vdash p(\bar m) \] 可用全称实例化推出 \[ N\vdash \neg w(\bar m,\bar n) \]

于是 \(N\) 同时证明 \[ w(\bar m,\bar n) \] 和 \[ \neg w(\bar m,\bar n) \] 与无矛盾性矛盾。

所以 \[ N\not\vdash p(\bar m) \]

再证明第二点。

反设 \[ N\vdash \neg p(\bar m) \] 即 \[ N\vdash \neg\forall x_2\,\neg w(\bar m,x_2) \]

由第一点，\(p(\bar m)\) 在 \(N\) 中没有证明。所以对任意自然数 \(n\)，\(n\) 都不是 \(p(\bar m)\) 的证明的 Gödel 数，即 \[ (m,n)\notin W \] 因为 \(w\) 表示 \(W\)，所以对每个 \(n\)， \[ N\vdash \neg w(\bar m,\bar n) \]

现在令 \[ q(x_2)\equiv \neg w(\bar m,x_2) \] 则对每个 \(n\)， \[ N\vdash q(\bar n) \] 但同时 \[ N\vdash \neg\forall x_2\,q(x_2) \]

这说明 \(N\) 是 \(\omega\)-矛盾的。

所以若 \(N\) 是 \(\omega\)-无矛盾的，就不可能证明 \[ \neg p(\bar m) \]

因此 \(p(\bar m)\) 和它的否定都不可证，\(N\) 不完备。

这个证明的关键如下：

第一，证明关系 \(\mathrm{PRF}\) 可递归分析

第二，递归关系可在 \(K_N\) 中表示

第三，把“我没有证明”这个语法事实算术化，并把自己的 Gödel 数代入

定义 18.10 Gödel-Rosser 定理、Church 问题和第二不完备性

Gödel 原始定理中，为了证明 \(\neg p(\bar m)\) 不可证，需要 \(\omega\)-无矛盾，Rosser 改进把这个条件降为普通无矛盾

定义 18.10.1 Rosser 关系

设 \(N^\ast\) 是 \(N\) 的一个递归无矛盾扩张。定义两个关系：

\[ W(n_1,n_2) \] 表示 \(n_2\) 是 \(p(\bar n_1)\) 从 \(N^\ast\) 的证明的 Gödel 数。

\[ W^\ast(n_1,n_2) \] 表示 \(n_2\) 是 \(\neg p(\bar n_1)\) 从 \(N^\ast\) 的证明的 Gödel 数。

由于 \(N^\ast\) 的公理集合可递归判定，两个证明关系仍然是递归关系，故可由公式 \[ w(x_1,x_2),\qquad w^\ast(x_1,x_2) \] 表示。

定义 Rosser 公式： \[ r(x_1)\equiv \forall x_2 \left( w(x_1,x_2)\to \exists y(y\le x_2\wedge w^\ast(x_1,y)) \right) \]

设 \[ m=g(r(x_1)) \] 则 Rosser 句为 \[ r(\bar m) \]

它的直观含义是：

若我有一个证明，那么我的否定也有一个不长于它的证明

定理 18.10.2 Gödel-Rosser 定理

若 \(N^\ast\) 是 \(N\) 的递归无矛盾扩张，则 \(N^\ast\) 不完备。更具体地说，存在闭式 \(r(\bar m)\)，使得 \[ N^\ast\not\vdash r(\bar m) \] 且 \[ N^\ast\not\vdash \neg r(\bar m) \]

证明： 点击查看证明

这里只写证明主线。

先反设 \[ N^\ast\vdash r(\bar m) \] 取 \(r(\bar m)\) 的最小证明 Gödel 数为 \(n\)。则 \[ W(m,n) \] 成立，故 \[ N^\ast\vdash w(\bar m,\bar n) \]

由 Rosser 句 \[ r(\bar m) \] 可推出 \[ \exists y(y\le \bar n\wedge w^\ast(\bar m,y)) \] 即存在一个不超过 \(n\) 的 \(\neg r(\bar m)\) 的证明。

这与 \(N^\ast\) 无矛盾矛盾。

再反设 \[ N^\ast\vdash \neg r(\bar m) \] 取 \(\neg r(\bar m)\) 的最小证明 Gödel 数为 \(n\)。则 \[ W^\ast(m,n) \] 成立。

如果存在 \(y\le n\) 使 \(W(m,y)\) 成立，那么 \(N^\ast\) 同时证明 \(r(\bar m)\) 和 \(\neg r(\bar m)\)，与无矛盾性矛盾。因此对所有 \(y\le n\)，都有 \[ \neg W(m,y) \] 这些都是有限多个具体事实，可在 \(N^\ast\) 中逐个证明对应的 \[ \neg w(\bar m,\bar y) \]

结合 \[ W^\ast(m,n) \] 可推出 Rosser 句本身 \[ r(\bar m) \] 从而又与 \[ N^\ast\vdash \neg r(\bar m) \] 矛盾。

所以 \(r(\bar m)\) 与其否定都不可证

Rosser 改进的意义在于：普通无矛盾就足以推出形式算术的不可完备性，不需要 \(\omega\)-无矛盾

定义 18.10.3 Church 问题

Church 问题问的是：是否存在一个机械方法，能够判定任意一阶谓词逻辑公式是否为有效式，或者判定任意形式算术公式是否可证

不完备性和递归论结果给出的回答是否定的。

如果存在一个算法能判定所有足够强的形式算术定理，那么就可以把可证性作为递归关系表示出来，再构造一个说“我不可证”的句子。这个句子会导致与 Gödel 构造同类的矛盾。

因此，足够强的形式算术不存在判定其全部定理的算法。

定理 18.10.4 Gödel 第二不完备性定理

设 \[ \mathrm{Con}(N) \] 是“\(N\) 无矛盾”的算术化公式。例如可以写成： \[ \neg\exists x\,\mathrm{PRF}(x,\ulcorner \bar0'\approx\bar0\urcorner) \] 表示不存在一个证明推出明显矛盾 \[ \bar0'\approx\bar0 \]

若 \(N\) 无矛盾，则 \[ N\not\vdash \mathrm{Con}(N) \]

证明： 点击查看证明

这里只说明证明思想。

第一不完备性定理的证明可以在 \(N\) 内部形式化：在 \(N\) 中可以证明 \[ \mathrm{Con}(N)\to p(\bar m) \] 也就是说，如果 \(N\) 能证明自己无矛盾，那么 \(N\) 就能证明 Gödel 句。

若又有 \[ N\vdash \mathrm{Con}(N) \] 则由 MP 得 \[ N\vdash p(\bar m) \] 这与第一不完备性定理中“若 \(N\) 无矛盾，则 \(N\not\vdash p(\bar m)\)”矛盾。

所以在 \(N\) 真正无矛盾时，\(N\) 不能证明自身无矛盾。

第二不完备性不是说我们永远不能证明 \(N\) 无矛盾，而是说不能在 \(N\) 自身内部完成这样的证明。较强系统可以证明较弱系统的无矛盾性，但足够强且无矛盾的系统不能完全依赖自身证明自身无矛盾

定义 18.11 形式算术的不可判定性

一个形式系统称为可判定的，是指存在算法，对任意公式 \(p\)，都能在有限步内判断 \[ N\vdash p \] 是否成立

定理 18.11.1 形式算术不可判定

若 \(N\) 无矛盾，则 \(K_N\) 的定理集合不是递归集。也就是说，不存在算法判定任意 \(K_N\) 公式是否可证

证明： 点击查看证明

证明思想如下

若 \(N\) 的定理集是递归集，则“\(p\) 在 \(N\) 中不可证”也是递归关系。由递归关系可表示性，可以在 \(K_N\) 内部构造一个公式表示 \[ \text{“编号为 }x\text{ 的公式不可证”} \]

再把这个公式自己的 Gödel 数代入，就得到一个更强的自指句 \(G\)： \[ G\leftrightarrow \text{“}G\text{ 不可证”} \] 并且由于“不可证”此时被假定为递归关系，若 \(G\) 真的不可证，\(N\) 反而能证明表示这个事实的公式，从而证明 \(G\)。

若 \(N\vdash G\)，则与 \(G\) 的含义和无矛盾性冲突。

若 \(N\not\vdash G\)，由于不可证性关系被假定可判定并可表示，\(N\) 又能证明 \(G\)。

两种情况都矛盾。

所以 \(N\) 的定理集不可判定。

形式算术的定理集虽然不可判定，但它是递归可枚举的：枚举所有证明，输出每个证明的末公式即可。这种“可枚举但不可判定”的现象是递归论和数理逻辑中的核心现象

定义 18.12 递归可枚举集与算术集

第 4.3 节继续讨论递归可枚举集和算术可定义性。

定义 18.12.1 递归可枚举集

集合 \(A\subseteq\mathbb N\) 称为递归可枚举集，若存在递归关系 \(R(x,y)\)，使得 \[ x\in A\iff \exists y\,R(x,y) \]

等价地说，可以用机械过程列出 \(A\) 的所有元素。若 \(x\in A\)，它最终会被列出；若 \(x\notin A\)，过程可能永远不会给出否定回答。

命题 18.12.2 递归集与递归可枚举集

集合 \(A\) 是递归集，当且仅当 \(A\) 和它的补集 \(\overline A\) 都是递归可枚举集。

证明： 点击查看证明

若 \(A\) 是递归集，则可以依次检查 \[ 0,1,2,\dots \] 是否属于 \(A\)。属于就列入 \(A\)，不属于就列入 \(\overline A\)，所以二者都递归可枚举。

反过来，若 \(A\) 和 \(\overline A\) 都递归可枚举。给定 \(x\)，同时运行两个枚举过程：

• 一个枚举 \(A\)
• 一个枚举 \(\overline A\)

由于 \(x\) 必在其中一个集合中，它最终会出现在其中一个枚举里。若出现在 \(A\) 的枚举中，判定 \(x\in A\)；若出现在 \(\overline A\) 的枚举中，判定 \(x\notin A\)。

所以 \(A\) 递归。

命题 18.12.3 可证公式集递归可枚举

\(K_N\) 中可证公式的 Gödel 数集合 \[ \mathrm{PA}=\{y\mid \exists x\,\mathrm{PRF}(x,y)\} \] 是递归可枚举集。

证明： 点击查看证明

因为 \(\mathrm{PRF}(x,y)\) 是递归关系，所以 \[ y\in \mathrm{PA} \iff \exists x\,\mathrm{PRF}(x,y) \] 正是递归可枚举集的定义形式。

也可以直接理解为：枚举所有自然数作为候选证明编码，凡是合法证明，就输出它证明的公式。

定义 18.12.4 算术集

集合 \(A\subseteq\mathbb N\) 称为算术集，若存在 \(K_N\) 语言中的公式 \[ p(x) \] 使得对每个自然数 \(n\)： \[ n\in A \iff \mathbb N\models p(\bar n) \]

这里的 \(\mathbb N\models\) 表示在标准自然数模型中为真。注意这不是说 \(N\vdash p(\bar n)\)，而是说公式在标准模型中为真。

定理 18.12.5 递归可枚举集都是算术集

若 \(A\) 是递归可枚举集，则 \(A\) 是算术集。

证明： 点击查看证明

因为 \(A\) 递归可枚举，存在递归关系 \(R(x,y)\)，使 \[ x\in A\iff \exists y\,R(x,y) \]

递归关系可在 \(K_N\) 中表示，所以存在公式 \[ r(x,y) \] 表示 \(R\)。

令 \[ p(x)\equiv \exists y\,r(x,y) \]

则在标准模型中， \[ \mathbb N\models p(\bar n) \] 当且仅当存在自然数 \(m\) 使 \[ R(n,m) \] 成立，也就是 \[ n\in A \]

所以 \(A\) 是算术集。

定理 18.12.6 真公式集不是算术可定义的

设 \[ \mathrm{TRUE}= \{\ulcorner p\urcorner\mid p\text{ 是在标准自然数模型中为真的闭式}\} \] 则 \(\mathrm{TRUE}\) 不是算术集。

这就是 Tarski 真理不可定义定理在算术中的形式。

证明： 点击查看证明

反证。假设存在公式 \[ T(x) \] 定义真理，即对每个闭式 \(p\)， \[ \mathbb N\models T(\ulcorner p\urcorner) \iff \mathbb N\models p \]

考虑公式 \[ \neg T(x) \] 用自指构造得到闭式 \(G\)，满足 \[ \mathbb N\models G\leftrightarrow \neg T(\ulcorner G\urcorner) \]

若 \(G\) 真，则由 \(T\) 定义真理，\(T(\ulcorner G\urcorner)\) 真；但由上式，\(\neg T(\ulcorner G\urcorner)\) 真，矛盾。

若 \(G\) 假，则 \(T(\ulcorner G\urcorner)\) 假，于是 \(\neg T(\ulcorner G\urcorner)\) 真，由上式得 \(G\) 真，也矛盾。

所以标准算术真理不能由算术公式定义。

这个结论比不完备性还强：不完备性说某些真句在给定系统中不可证；真理不可定义定理说，所有真算术句构成的集合甚至不能在算术内部整体定义出来

定义 18.13 Turing 机与 Turing 论题

递归函数是一种形式化的可计算性定义，Turing 机是另一种形式化定义。二者最终给出同一类可计算函数

定义 18.13.1 Turing 机

一台 Turing 机包含：

• 一条向两端无限延伸的纸带，纸带分成格子
• 有限符号表，其中包含空白符号
• 有限状态集合，其中有初始状态和停机状态
• 一个读写头，每次扫描一个格子
• 有限条指令

每条指令规定：在当前状态和当前读到的符号下，

• 写入一个符号
• 向左或向右移动一格，或保持不动
• 进入一个新状态

机器的某一时刻完整情况称为瞬时描述，包括：

• 当前状态
• 纸带上非空白部分的内容
• 读写头所在位置

一次计算就是瞬时描述的有限或无限序列

定义 18.13.2 Turing 可计算函数

函数 \[ f:\mathbb N^k\to\mathbb N \] 称为 Turing 可计算，若存在一台 Turing 机，对每个输入 \(\vec n\)：

• 若 \(f(\vec n)\) 有定义，则机器最终停机并输出 \(f(\vec n)\)
• 若 \(f(\vec n)\) 无定义，则机器不停机

若只讨论处处有定义的函数，则机器对每个输入都必须停机

定理 18.13.3 Turing 可计算函数等于部分递归函数

一个数论函数是 Turing 可计算的，当且仅当它是部分递归函数

证明： 点击查看证明

这里只写证明思路。

先看从递归函数到 Turing 机。

零函数、后继函数、投影函数都可以直接由 Turing 机计算。函数复合对应机器程序的串接：先计算内部函数，再把输出交给外部函数。原始递归对应有限循环。\(\mu\) 算子对应依次搜索 \[ 0,1,2,\dots \] 直到找到满足条件的最小值。若找不到，就不停机

所以部分递归函数都 Turing 可计算。

再看从 Turing 机到递归函数。

把一台机器的瞬时描述编码成自然数，包括状态、纸带内容和读写头位置。机器从一个瞬时描述到下一个瞬时描述的转移是有限表控制的，所以是递归函数

设 \[ C_M(x,t) \] 表示机器 \(M\) 在输入 \(x\) 上运行 \(t\) 步后的瞬时描述编码。这个函数可由原始递归定义

“\(M\) 在 \(t\) 步时停机”是递归关系。若机器最终停机，则停机时间可写成 \[ \mu t[\text{$M$ 在 $t$ 步停机}] \] 输出也可由停机瞬时描述递归读出

因此 Turing 机计算的函数是部分递归函数

定义 18.13.4 Turing 论题

Turing 论题，也称 Church-Turing 论题：

一切直观上能机械计算的函数，正是 Turing 可计算函数，也就是递归函数

定理 18.13.5 停机问题不可判定

不存在一台 Turing 机能判定任意机器在任意输入上是否停机。

证明： 点击查看证明

反证。假设存在判定机 \(D\)，对任意机器 \(M\) 和输入 \(x\)： \[ D(M,x)= \begin{cases} 1, & M(x)\text{ 停机}\\ 0, & M(x)\text{ 不停机} \end{cases} \]

构造新机器 \(E\)，输入一台机器 \(M\) 的编码：

• 若 \(D(M,M)=1\)，即 \(M(M)\) 停机，则 \(E(M)\) 进入死循环
• 若 \(D(M,M)=0\)，即 \(M(M)\) 不停机，则 \(E(M)\) 立即停机

现在考察 \(E(E)\)

若 \(E(E)\) 停机，则按 \(E\) 的定义，必须有 \(D(E,E)=0\)，即 \(E(E)\) 不停机，矛盾

若 \(E(E)\) 不停机，则按 \(E\) 的定义，必须有 \(D(E,E)=1\)，即 \(E(E)\) 停机，矛盾

所以停机判定机不存在

推论 18.13.6 存在递归可枚举但非递归的集合

停机集合 \[ K=\{\langle M,x\rangle\mid M(x)\text{ 停机}\} \] 是递归可枚举集，但不是递归集

证明： 点击查看证明

\(K\) 递归可枚举：枚举所有机器输入对，并逐步模拟运行。只要某个机器在某个输入上停机，就输出对应编码

\(K\) 不是递归集：若 \(K\) 是递归集，就存在算法判定任意 \(M(x)\) 是否停机，这正是停机问题的判定算法，与停机问题不可判定矛盾

18.14 人与机器

从 Turing 论题看，只要一种过程能被明确写成机械规则，它就应当可以由 Turing 机模拟。因此“机械可计算”有一个非常稳定的数学刻画

但 Gödel 不完备性说明：对足够强的形式算术系统来说，总存在该系统无法判定的算术句。若一个人站在系统外部承认系统无矛盾，就能看出 Gödel 句在标准模型中为真；但系统内部不能证明它

这不应被简单理解成“人一定超过机器”。更准确的说法是：任何固定的、递归给出的形式系统，只要它足够强且无矛盾，就不能穷尽全部算术真理。若把人的推理也完全固定为某个递归形式系统，那么同样会受到不完备性限制