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, 通用函数定理). 存在原始递归函数 与原始递归集 , 使得对任意的部分递归函数 都存在一个自然数 使得 .

进一步, 存在通用部分递归函数 , 使得对任何部分递归函数 都存在自然数 满足 .

证明. 这个 Kleene’s T 指的其实是 当且仅当程序 对输入 的计算过程的编码为 , 其中细节其实就是证明部分递归函数等价于图灵可计算函数的过程, 此处略.

定理 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. 对任意 , 以下 个数 两两互素.

以下神奇编码过程来自 Godel.

定理 9.3.19. 构造以下可表示函数:

1.

2.

3.

4.

5.

.

证明. 略.

我们就用这个编码证明最后一步.

定理 9.3.20. 经原始递归得到, 则 均可表示时 亦可表示.

证明. 表示, 表示, 则有可表示集 表示, 进而 可表示.

总结如下.

定理 9.3.21. 函数递归当且仅当可表示.

编码

这一小节, 我们要用 讨论自己的语法, 这是通过编码进行的. 我们的一切行为均在 上进行.

定义 9.3.22 (Godel 编码). 我们给每个语言中的符号 指定一个奇数 : , , , , , 左右括号是 , , , , 随后是可列个变元符号.

进一步, 我们给每个字符串 指定其 Godel 编码为 .

我们额外对每个 引入记号 , 则上式也可记为 .

我们的目标是探索编码后的逻辑关系是否是原始递归的. 对于语言中说出的一个东西, 我们用\underline东西代指 是这样的东西 . 我们采取前缀函数记法, 以尽量减少括号的使用.

定理 9.3.23. \underline变元是原始递归的.

证明. \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.

, 则 都有 .

lemma 最后, 我们单独引入一个定义.

定义 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 第一不完全性定理). 对包含 的递归可公理化理论 , 如果 一致, 则存在语句 , 满足 .

这其实是 Rosser 给出的强版本定理, 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 的强不可判定性). 任何算术理论 , 若 是完全且一致的, 则 是不可判定的.