集合论和一阶逻辑的关系?


有朋友在知乎上问:

http://logic.fudan.edu.cn/doc/Course/2014/MathLogic/Lecture01.pdf 最后一段:

  • 集合论可以被看作是一种一阶逻辑理论
  • 一阶逻辑的语法、语义概念都可以在集合论中定义, 关于一阶逻辑的定理可以被看作是集合论的定理

建立一阶逻辑时貌似很多定义都用了集合论描述。而集合论本身又可以被看作是一种一阶逻辑理论。不是有循环定义的嫌疑吗?

我在知乎的回答如下:

链接中是上学期第一堂课的幻灯片,最后一张的标题是“集合论与一阶逻辑是什么关系?”,以问号结尾。关于这个问题,我给出了两则容易令人困惑的命题而没再做进一步的解答。目的是激发同学们的思考,希望大家带着这个问题,经过一个学期的学习,能形成自己的见解。

一来,对这个日常语言表达的问题很难说某个答案是完备且无争议;二来,对这个问题有意义的讨论需要一些知识和训练作前提(例如,一个学期的数理逻辑课程)。因此,在这里也只能很粗略地谈谈我的理解。

1. 一些澄清

我们先澄清几个相关概念以缩小讨论范围。有关概念的解释并非唯一。这里的“澄清”也并非严格的数学定义,限于篇幅,更谈不上完备。

1.1) 一阶逻辑

1.1.1) 一阶逻辑的语言。一种人工语言。我们人为规定了一些初始符号(逻辑符号、辅助符号、变元、等词、函数符号、谓词符号等),由这些符号组成(合规格的)公式、句子的规则。这些初始符号、公式在本体论上可以是符合一些条件(为保证唯一可读性)的任何东西,当然也可以是集合。通过定制不同的函数符号、谓词符号可以得到不同的一阶逻辑语言,如集合论的语言(只含有一个二元谓词符号,用以表示“属于”关系)、数论的语言(有加法符号、乘法符号等)等。

1.1.2)一阶逻辑的语法概念。一般我们用这个称谓囊括了一阶逻辑语言的“初始符号”、“公式”、“句子”、“逻辑公理”(一集一阶逻辑语言的句子集)、“证明”等概念。

1.1.3) (狭义的)一阶逻辑。指一些一阶逻辑语言句子组成的集合,它们是逻辑公理和仅从它们“可证”的句子。

1.1.4) 一阶逻辑的语义概念。指“(一个一阶语言公式)在(某个结构、赋值下)满足”、“(一个一阶句子)是(在某个结构下)真的”、“(一个一阶逻辑公式/句子)是有效的”、“(一个公式)定义了(一个结构论域上的某个子集或关系)”等。

1.1.5) 一阶(逻辑)理论。某个一阶语言的一集句子。有时候也可以加上在“可证”下封闭这个条件。

1.1.6) 关于一阶逻辑的定理,指一阶逻辑的唯一可读性、完全性定理、紧致性定理等等。

1.2) 集合论指某种公理化的集合论,如常见的 Zermelo-Fraenkel Set Theory(ZF)。这是一组一阶集合论语言(这是一种一阶逻辑语言。也有其他形式语言中的公理化集合论,如NBG,它可以被看作是一种 two-sorted language的理论)的句子,即所谓集合论公理,以及从它们“可证”的句子组成的集合。

不难看出,(狭义的)一阶逻辑与集合论都是一阶语言句子集。如果限定在集合论语言下,(狭义的)一阶逻辑是公理化集合论的一个子集。它们都是一种一阶理论。

1.3) (一个一阶理论)描述(一个一阶理论)。一般没这个说法。我们有关于用一个一阶理论“解释”(interpret)另一个一阶理论的说法。例如,把 PA(皮亚诺算术)翻译到 ZF中。我们也可以说,例如,PA(作为一个集合)在ZF中可定义。(见后文)

2. 基于上述澄清,我们说“集合论是一种一阶理论”。原命题中用了“可以”,是因为“集合论”还可以有别的解释。

3. “一阶逻辑的语法、语义概念都可以在集合论中定义, 关于一阶逻辑的定理可以被看作是集合论的定理”。

“(一个概念)在(一个一阶理论中)可定义”是什么意思?

例如:我们说,“自然数”这个概念在 ZF 中可定义,是指存在一个集合论语言的公式 \(\varphi(x)\),我们认为 \(\varphi(x)\) 定义了自然数集。“我们认为 \(\varphi(x)\) 定义了自然数集”不是一个严格的数学判断,因而无法得到一个数学证明。因为这里的“自然数”只是人们的一个直观。但是,我们可以通过在 ZF 中证明一些命题来让人们相信,\(\varphi(x)\) 确实刻画了我们关于自然数的直观。例如,ZF 可以证明,\(\varphi(1), \varphi(2), \ldots\) 甚至证明 \(\forall x \varphi(x) \rightarrow \varphi(x+1)\) (注意,“\(+\)”、“1”、“2”也是 ZF 中定义的,并非集合论语言的初始符号),对应于我们关于“1是自然数”、“2是自然数”……以及“自然数的后继也是自然数”这些直观。这里,我们又称诸如“\(\forall x \varphi(x) \rightarrow \varphi(x+1)\)”是 ZF 中所证明的关于自然数的一个定理。

在这个意义上,我们宣称,如,“一阶逻辑的公式”这个概念在 ZF 中可定义,等等。也正是在这个意义上,我们宣称几乎所有的经典数学概念都可以在集合论中定义。这和丘奇论题(Church’s thesis)宣称,“(函数\(f\))可计算”这个直观概念被“(函数\(f\))图灵机可计算的”(即某个一阶公式\(\psi(f)\))刻画,是异曲同工的。它不是一个数学判断,但我们可以证明关于图灵可计算的一些定理,让我们相信它确实刻画了我们关于“可计算”概念的直观。

在上述意义上,我们说一阶逻辑的一些语法、语义概念在 ZF 中可定义,也可以说(狭义)一阶逻辑这个句子集在 ZF 中可定义,甚至可以说 ZF 这个句子集在 ZF 中可定义。但反过来,我们不能说这些概念在(狭义)一阶逻辑这个理论中可定义的,因为这个理论证明不了的我们需要的一些定理。

4. 数理逻辑中有关于理论的解释力(interpretability strength)的一些刻画,例如一致性强度(consistency strenth)。在这些刻画下,集合论的解释力都强于(狭义)一阶逻辑,即集合论可以解释一阶逻辑,反之则不行。没有循环。

5. 在逻辑学中,给定一个形式语言初始符号及其语义,我们可以把新的符号定义为初始符号的特定组合,新符号的语义可以归约为初始符号的语义。但如果把非初始符号 A 定义为包括了非初始符号 B 的一些符号的组合,而 B 又是包括了 A 的一些符号的组合,就出现了“循环定义”。这种情况下,我们没法把 A 和 B 还原为初始符号的组合,也没法通过对初始符号的解释准确得到对 A、B 的解释。

以上,我们在集合论中对诸概念的定义,都表现为把“初始符号”、“公式”、“证明”、“满足”、“真”、“一阶逻辑”、“ZF”还原为集合论语言初始符号的组合。不存在“循环定义”。

“循环定义”作为日常语言使用中的一个现象,普遍存在。在日常语言中,本就没有所谓初始符号或初始概念,许多概念都是相互解释模糊不清的,也就谈不上“循环定义”的错误了。

6. “建立”的问题。数学实在论(柏拉图主义)认为,数学对象都是独立于人而存在的,自然没有“建立”一说。数学直觉主义认为,数学(对象)都是由心灵构造的。按照直觉主义(布劳威尔)的路线,人的心灵是先通过所谓“二一性”(two-oneness)的直观,构造出各个自然数乃至自然数概念(部分),由此,我们可以构造出上面所涉及的各个逻辑学概念(并不一定要集合论这么强的理论)。特别地,“(狭义)一阶逻辑”、“ZF”概念也可以由此被构造出来,不会依赖对方才能被构造。值得一提的是,一些构造主义(包括直觉主义)的确基于一些概念的构造必须以彼此为前提来拒绝承认那些概念是有效的(见:Impredicativity)。这里并不涉及这种情况。

7. 就现实中的学习过程而言。我们的确会在数理逻辑的课程中穿插着讲很多集合论的内容;在集合论的课程中又讲很多关于一阶逻辑的知识。并且这是必要的,即对彼此的理解依赖对方。注意,这里的集合论、一阶逻辑的意义不再限于前面的澄清。此外,如果在哲学上采纳柏拉图主义立场,即这些数学对象都是独立于我们而存在的,它们彼此联系。如此,更不难解释为什么我们对它们的认识理解必须这样穿插着进行了。

我个人对这个回答不是很满意。限于篇幅,很多断言缺乏论证。回答中避免使用一些专业术语,因为若不给出大量定义、定理,一些术语的日常理解容易引起误解。因此,只能尽量选择日常语言中较易理解又不易产生误解的说法。但这样可能既不能完全避免误解,又显得不专业,很难把握。所以,我还是建议对相关问题感兴趣的读者,花时间系统学习一下数理逻辑与集合论课程。这方面优秀的教材很多,这里就不谦虚地推荐一下我们的《数理逻辑·证明及其限度》《集合论:对无穷概念的探索》

====2015.5.9更新=============

因为我原本试图在不预设任何哲学立场的前提下回答这个问题。站在不同的哲学立场上,答案是简单而直接的。

如果采取实在论(柏拉图主义)的立场。那么无论集合论还是一阶逻辑都是我们有限的人类关于那个无穷的概念世界之规律的描述。就如同物理定律是对物理世界规律的描述一样。因为是对一个客观世界的描述,那就无所谓谁先谁后,谁建立谁的问题了。

如果站在形式主义的立场。ZFC 公理系统是一阶逻辑公理系统的扩张。我们在 ZFC 公理系统里演绎出一些符号串。至于这些符号串是不是表达关于一阶逻辑或 ZFC 公理系统本身的一些事情,严格的形式主义者根本不关心。

Leave a Reply

Your email address will not be published. Required fields are marked *

19 + eighteen =