9. 递归与公理
9.1原始递归函数
本节与下节介绍基础的递归论知识, 以应用于不完备性定理的证明. 为了简便, 我们略去与图灵机有关的全部内容.
定义 9.1.1 (原始递归函数). 我们先来定义最简单的一类 上的可定义函数. 首先, 我们指定以下三个函数为初始函数:
1. | 零函数 |
2. | 后继函数 |
3. | 投射函数 |
对 , 我们称 与 经原始递归得到 , 若它满足:
1. |
|
2. |
|
包括所有初始函数, 且对函数复合和原始递归两种操作封闭的最小的全函数类中的元素称作原始递归函数.
注 9.1.2. 不难证明, 每个原始递归函数都对应不唯一的一个有限函数列, 其中每个函数都是初始函数, 或由之前的函数复合而成, 或由之前的函数原始递归而成. 这称为它的生成序列.
我们首先指出, 许多常见的函数都是原始递归的.
定理 9.1.3. 以下函数均为原始递归函数:
1. | 常函数 |
2. | 前驱 , 的前驱仍为 . |
3. | 加法 |
4. | 乘法 |
5. | 指数 |
6. | 阶乘 |
7. | 截断减法 , 小数减去大数全作为 处理. |
8. | 取商 , 这是小学学的带余除法的商. |
9. | 取余数 |
10. | 零特征函数 , 它只在 处取 , 在别的地方均取 . |
上面列举的最后一个原始递归函数的名字给予我们一些想法.
定义 9.1.4 (原始递归集合). 对一个集 , 我们称 为其特征函数, 它在 上恒为 , 在别处恒为 .
一个集合 称作原始递归集合, 若其特征函数是原始递归函数.
定理 9.1.5. 原始递归集合对取补集、有限并集和有限交集封闭.
同样, 许多常见的关系作为集合都是原始递归的.
定理 9.1.6. 以下谓词/关系作为集合是原始递归的:
1. | 等于 |
2. | 小于等于 |
3. | 整除 |
4. | 素数判断 |
5. | 合数判断 |
推论 9.1.7. 是原始递归函数, 它对 给出第 个素数.
我们还可以有分段定义函数.
定理 9.1.8. 若 与 均为原始递归函数, 是原始递归集合, 则 也是原始递归函数, 它在 上取值为 的值, 在 之外取值为 的值.
最后, 我们指出两种操作, 原始递归函数类对这两者封闭.
定义 9.1.9 (有界极小算子). 对一个 , 我们定义 是最小的满足 的不大于 的 ; 如果这样的 不存在, 则此式取值为 . 这个 读作最小的.
定理 9.1.10. 若 是原始递归集合, 则 是原始递归函数, 和 是原始递归集合.
证明. 只需注意以下引理.
引理 9.1.11. 若 原始递归, 则 与 也都是原始递归的.
定义 9.1.12 (强递归). 对 , 我们称 为 的历史函数.
如果我们称 是由 和 经强递归得到的, 若:
1. |
|
2. |
|
定理 9.1.13. 原始递归函数强递归得到的函数也是原始递归的.
9.2递归函数
现在, 我们要考虑比原始递归函数更广义的两类可计算函数, 分别是递归全函数与部分递归函数.
定义 9.2.1 (正则极小算子). 对全函数 , 若 , 则称 有正则性条件. 我们对有正则条件的 定义 为 经过正则极小算子 得到的函数, 它是最小的使得 的 .
定义 9.2.2 (递归全函数). 包含全体初始函数, 且对复合、原始递归与正则极小化封闭的最小的全函数类中的函数称作递归全函数.
定义 9.2.3 (极小算子). 对部分函数 , 我们称 是 经过极小算子得到的函数, 这里 指的是 在此时有定义, 仍然读作最小的.
定义 9.2.4 (部分递归函数). 包含全体初始函数, 且对复合、原始递归与极小化封闭的最小的部分函数类中的函数称作部分递归函数.
考察部分递归函数而非递归全函数的好处是, 部分函数存在通用函数, 而全函数不存在.
定理 9.2.5 (Kleene, 通用函数定理). 存在原始递归函数 与原始递归集 , 使得对任意的部分递归函数 都存在一个自然数 使得 .
进一步, 存在通用部分递归函数 , 使得对任何部分递归函数 都存在自然数 满足 .
定理 9.2.6. 不存在通用递归全函数.
定理 9.2.7. 函数的递归全函数当且仅当它是全的部分递归函数.
证明. : 对生成序列做归纳.
递归全函数自然地给出递归集的定义.
定义 9.2.8 (递归集). 如果一个集的特征函数是递归全函数, 则称这个集是递归集.
定理 9.2.9 (递归可枚举集). 对 , 以下命题等价:
1. | 是一个部分递归函数的值域. |
2. | 是空集或 是一个递归全函数的值域. |
3. | 是空集或 是一个原始递归函数的值域. |
4. | 是一个部分递归函数的定义域. |
5. | 存在原始递归集 , 使得 . |
6. | 的部分特征函数是部分递归的, 这个部分特征函数 在 上取值为 , 在别处无定义. |
它满足这些条件中的任意一个 (也就是全部) 时, 称它为一个递归可枚举集.
进一步, 我们可以定义 上的递归可枚举集.
定理 9.2.10. 递归可枚举集对有限交、有限并、存在量化封闭, 但不对取补封闭. 其模糊集类 (对取补封闭的子类) 恰为递归集.
9.3编码与表示
接下来, 我们要在算术语言 上讨论 Godel 著名的两个不完全性定理. 第一不完全性定理要求较弱, 我们取一个相当简单的理论来证明.
定义 9.3.1 (Robinson 算术). 以下理论称作 Robinson 算术, 记作 Q:
1. |
|
2. |
|
3. |
|
4. |
|
5. |
|
6. |
|
7. |
|
为了区分, 以上列举的各式将被记为 (Q1) 到 (Q7).
可表示性
我们这一小节的任务是证明递归全函数就是可表示函数.
定义 9.3.2 (可表示集). 称 是理论 中可表示的, 若存在其表示公式 , 使得 , 且 .
注 9.3.3. 注意, 否定情况是 而非 , 后面的只不过是不可证明, 前者才是证明为假.
定义 9.3.4 (可表示函数). 称 是理论 中可表示的, 若存在其表示公式 , 使得 .
注 9.3.5. 可表示函数的表示公式是比函数作为集合是可表示集的表示公式, 但反过来则不一定.
定理 9.3.6. 集合 在理论 中被公式 表示, 当且仅当它在 中被公式 定义.
定理 9.3.7. 可表示集对有限交、有限并和取补集封闭, 且在一致理论扩张下不变.
定理 9.3.8. 可表示集是递归集.
定理 9.3.9. 函数可表示当且仅当它作为集合可表示.
证明. 向右显然, 向左注意到其实我们只需要加上一层正则极小化算子, 我们其实就是在证明以下引理.
引理 9.3.10. 若 被 表示, 且 , 则公式 表示了函数 .
推论 9.3.11. 可表示函数的正则极小化是可表示函数.
定理 9.3.12. 项 诱导出的函数 都是可表示的.
.
推论 9.3.13. 初始函数都是可表示函数.
定理 9.3.14. 若 到 都可表示, 也可表示, 则 可表示.
推论 9.3.15. 可表示函数对复合封闭.
定理 9.3.16 (Bezout). 互素当且仅当存在 使得 .
定理 9.3.17. 中国剩余定理如果有限个 两两互素, 则 是满射.
引理 9.3.18. 对任意 , 以下 个数 两两互素.
定理 9.3.19. 构造以下可表示函数:
1. |
|
2. |
|
3. |
|
4. |
|
5. |
|
则 .
定理 9.3.20. 若 由 和 经原始递归得到, 则 与 均可表示时 亦可表示.
定理 9.3.21. 函数递归当且仅当可表示.
编码
这一小节, 我们要用 讨论自己的语法, 这是通过编码进行的. 我们的一切行为均在 上进行.
定义 9.3.22 (Godel 编码). 我们给每个语言中的符号 指定一个奇数 : 是 , 是 , 是 , 是 , 是 , 左右括号是 和 , 是 , 是 , 是 , 随后是可列个变元符号.
进一步, 我们给每个字符串 指定其 Godel 编码为 .
我们额外对每个 引入记号 , 则上式也可记为 .
定理 9.3.23. \underline变元是原始递归的.
定理 9.3.24. \underline项是原始递归的.
证明. \underline项有以下的递归定义, 如果以下之一成立:
1. | \underline变元 |
2. | \underline项 |
3. | \underline项 |
注 9.3.25. 指的是把 还原成字符串 .
定理 9.3.26. \underline原子公式是原始递归的.
定理 9.3.27. \underline公式是原始递归的.
定理 9.3.28. 逻辑连接词与量词都是原始递归函数.
定理 9.3.29. 变元替换是原始递归函数.
定理 9.3.30. 是原始递归的.
定理 9.3.31. 二元关系 \underline自由出现 是原始递归的.
定理 9.3.32. \underline语句是原始递归的.
定理 9.3.33. 三元关系 \underline无冲突替换 是原始递归的.
定理 9.3.34. 二元关系 \underline全称概括 是原始递归的.
定理 9.3.35. \underline逻辑公理是原始递归的.
定义 9.3.36. 称 公理化了理论 , 若 是一个递归集, 且 当且仅当 .
定理 9.3.37. 对可公理化的理论 , 谓词 \underlineT 中的证明序列 是递归的.
定义 9.3.38. 定义谓词 \underlineT 中的证明序列 这里 是 的长度, 这个谓词读作 在 中证明 .
注 9.3.39. 其实是 作为证明序列解码得到 的证明序列.
定理 9.3.40. 是递归的.
推论 9.3.41. 存在算术语言中可定义的谓词 , 使得它在结构 上恰为 .
引理 9.3.42. 对可公理化的理论 ,
1. | , 则 满足 . |
2. | , 则 都有 . |
定义 9.3.43. 定义 为 .
推论 9.3.44. 是递归可枚举的, 且 可推出 .
注 9.3.45. 然而, 却并不能推出 .
不动点
我们给出最后一个重要的引理, 它具有相当的暗示性. 我们先给出一个常见简记法.
定义 9.3.46. 对公式 , 我们用 代指 . 对自然数 , 我们用 代指 .
定理 9.3.47 (不动点引理). 存在递归的算法, 任给单自由变元公式 , 这算法都给出一个句子 , 满足 .
注 9.3.48. 换言之, 这个函数 是递归的.
9.4第一不完全性
现在, 我们来叙述并证明大名鼎鼎的 Godel 第一不完全性定理.
定理 9.4.1 (Godel 第一不完全性定理). 对包含 的递归可公理化理论 , 如果 一致, 则存在语句 , 满足 且 .
定理 9.4.2 (Godel 第一不完全性定理, 原始版本). 对包含 的递归可公理化理论 , 如果 是 一致的, 则存在语句 , 满足 且 .
定义 9.4.3. 对语言 上的理论 , 我们有以下两种不一致的概念:
1. | 不一致: 存在 使得 , 但 均有 . |
2. | 不一致: 存在 使得 而且 . |
不是 不一致就称 一致, 不是不一致就称一致.
注 9.4.4. 不一致显然会指出自然数标准模型不是这个理论的模型, 但不一致则指出它没有模型, 可见其强度差异. 显然, 非标准模型的理论都是一致却非 一致的.
证明. 考虑单自由变元公式 的不动点 , .
如果 , 则 , 换言之 不一致, 进而 是 不一致的, 矛盾.
然而, 由于 一致性严格强于一致性, 我们需要引入 Rosser 的一个技巧来证明第一个版本的更强的不完全性定理.
证明. 我们考虑另一个谓词, 它在 里面就是 , 但在一般情形下却比后者更容易证明. (恰好像是 一致与一致的区别)
定义 9.4.5. 令 为 .
引理 9.4.6. 比 更好的是, 同时具有以下性质:
1. | 推出 |
2. | 推出 |
定理 9.4.7 (Tarski 真不可定义定理). 是作为 结构的 的不可定义集.
定理 9.4.8 (Q 的强不可判定性). 任何算术理论 , 若 是完全且一致的, 则 是不可判定的.