1.3. 哲学注记
以上两节答辩主要是为了解决一个常见的疑难问题: 先有集合论还是先有一阶逻辑. 这个问题的知乎编码是 28776730.
对于柏拉图主义者而言, 集合是一种完成的、确切的、实在的 (概念) 对象, 而逻辑是我们认识概念世界的一种方法, 一阶逻辑是逻辑中的一种. 它也是一种完成的、确切的、实在的 (概念) 对象, 因此并不存在谁先谁后或者谁建立谁的问题.
然而, 对于对集合宇宙保有怀疑态度的人而言, 以上论述是相当值得怀疑的. 后退到形式主义者的立场, 我们说 公理系统是一阶逻辑公理系统的扩张, 然后在 公理系统里演绎出一些符号串. 至于这些符号串是不是表达关于一阶逻辑或 公理系统本身的一些事情, 严格的形式主义者根本不关心.
然而, 我们甚至还可以试着向下退, 认为符号串这个概念都不够基本, 一定要把所有东西编码成自然数, 这样退的结果是碰到 Godel 不完全性定理. 我们也可以试着向外退, 认为我们需要澄清集合论与一阶逻辑在何等系统中运作. 这一章大概是笔者向外退的过程中产生的想法.
一个更加美好的建议是使用类型论, 然后将集合论与一阶逻辑都实现到某个给定的类型论中, 类型论运行在电脑上, 这样就有相当坚实的基础; 然而这操作毕竟与本书希望关心的内容相去甚远, 因此笔者选择自己造轮子, 提取了一阶逻辑中长得最像是计算机可操作的、最不依赖集合实在性的那一部分内容, 斗胆起名为朴素逻辑.
这里面藏匿了许多未加探讨和证明的细节: 例如各种归纳定义的对象的编码集究竟是原始递归的、递归的还是递归可枚举的, 每一次证明使用的归纳法究竟是不是递归能行的证明枚举序列, 诸如此类. 笔者本人其实也没有真正地一一验证过, 因此完全有可能以上内容不是真正的符合这样强的计算主义要求的. 请读者海涵.
目前看来, ZF 集合论在这个基础上运作良好, 我们可以继续用 ZF 集合论建造通常意义下的一阶逻辑系统, 并完整的讨论其语法与语义, 这将是下一章的工作, 或者是讨论更强或更弱的逻辑系统. 再在此之后, 我们可以将 ZF 集合论的理论作为 dlc 加入这个一阶逻辑系统中, 得到完整的集合论, 或者是考虑更强的例如二阶的集合论.
然而无论如何, 我们只是允许在这个朴素逻辑下使用 ZF 来讨论别的东西. 如果我们想要继续讨论诸如 需要多弱的算术系统来编码并证明的时候, 我们用以讨论这个算术系统的符号系统仍然是用 ZF 解释的, 因此严格来说这本书里讨论的这些内容都不是真的弱算术系统. 然而, 我们总是可以相信有一个足够强悍的人, 他真的可以按照我们给出的证明大纲在那个弱算术系统能承载的证明系统中证明出这种话的形式化版本, 所以我们就姑且信之.
事实上, 使用完整的 ZF 是无必要的; 我们完全可以在 ZF 公理化集合论之前再开一章写朴素集合论, 这个朴素集合论可以很弱很弱, 因为完整的定义一阶逻辑实在不需要太多的集合论, 我们甚至可以先在元理论里面直接搭建出朴素的集合论. 然而, 在完整理论的边缘一直徘徊会给人一种急躁的情绪, 而且朴素集合论学得太多疑似更容易成为反公理化集合论的魔怔人, 所以笔者没有采取这个更常见的进路.
我们自然可以进行更多的诘难, 例如询问为何我们将要建造的一阶逻辑系统真的就是以上朴素逻辑的形式化版本, 这个问题其实就像是为什么 确实定义了集合论意义下的自然数一样. 我在这里照抄杨睿之老师的那一段回答:
“(一个概念) 在 (一个一阶理论中) 可定义” 是什么意思? 例如: 我们说, “自然数” 这个概念在 ZF 中可定义, 是指存在一个集合论语言的公式 , 我们认为 定义了自然数集. “我们认为 定义了自然数集” 不是一个严格的数学判断, 因而无法得到一个数学证明. 因为这里的 “自然数” 只是人们的一个直观. 但是, 我们可以通过在 ZF 中证明一些命题来让人们相信, 确实刻画了我们关于自然数的直观. 例如, ZF 可以证明, 、、…… 甚至证明 (注意, “+”、“1”、“2” 也是 ZF 中定义的, 并非集合论语言的初始符号) , 对应于我们关于 “1 是自然数”、“2 是自然数”…… 以及 “自然数的后继也是自然数” 这些直观. 这里, 我们又称诸如 “” 是 ZF 中所证明的关于自然数的一个定理. 在这个意义上, 我们宣称, 如, “一阶逻辑的公式” 这个概念在 ZF 中可定义, 等等. 也正是在这个意义上, 我们宣称几乎所有的经典数学概念都可以在集合论中定义. 这和丘奇论题宣称, “(函数 f) 可计算” 这个直观概念被 “(函数 f) 图灵机可计算的” (即某个一阶公式 ) 刻画, 是异曲同工的. 它不是一个数学判断, 但我们可以证明关于图灵可计算的一些定理, 让我们相信它确实刻画了我们关于 “可计算” 概念的直观. 在上述意义上, 我们说一阶逻辑的一些语法、语义概念在 ZF 中可定义, 也可以说 (狭义) 一阶逻辑这个句子集在 ZF 中可定义, 甚至可以说 ZF 这个句子集在 ZF 中可定义. 但反过来, 我们不能说这些概念在 (狭义) 一阶逻辑这个理论中可定义的, 因为这个理论证明不了的我们需要的一些定理. "
另一些读者可参考的书籍是 Raymond M. Smullyan 的 Theory of Formal Systems, 冯琦的集合论导引 (第二卷), Devlin 的 Constructibility 等.