数理逻辑中集合论、模型论、证明论、可计算性理论这四大领域的内在理论联系是什么？ 第1页

(抛砖引玉, 想到什么写什么, 段落之间并没有什么特别联系)

我在TA的时候喜欢用来给学生介绍逻辑的口号就是"logic is the study of truth preserving inferences".

这个口号在教学命题逻辑的时候尤其有效, 因为真值表对应着"什么是truth和truth-preserving"的研究, 而推理系统则对应"什么是inferences"的研究.

把这个说法拓展到一阶逻辑上来说, 那就是: 模型(论)对应着"什么是truth和truth-preserving"的研究, 推理系统(证明论)对应着"什么是inferences"的研究, 而集合论通过塔斯基满足关系的定义来使得"模型中为真"这一概念得到严格化. 可计算理论则是考虑形式公理系统作为可操作系统的限制.

当然, 上面只是比较简化的说法, 主要用于给第一次接触这些名词的学生介绍这几个子学科之间的部分关系. 要是细说的话, 各个学科之间比较fundamental的联系大概是:

现代模型论的开端始于塔斯基的满足关系定义, 而这个满足关系又是在集合论基础上表述的. 例如一个谓词P, 以及一个对象a, 我们想知道模型满不满足P(a), 就只需要看这个结构里a元素在不在这个集合对P的解释的这个集合里. 当然了, 满足关系中真正用上了比较nontrivial的集合论的地方是量词满足关系的定义(" "当且仅当对于所有的variable assignment, blablabla...)这里对variable assignment(也就是从变元集到结构论域的函数)进行量化, 最方便的理论框架也就是集合论.

模型与证明的关系由完备性定理给出: (对一阶逻辑来说) 一个理论存在模型当且仅当这个理论在证明论意义上一致.

与此同时, 哥德尔的不完备定理告诉我们, 如果一个理论{包含足够多的算术, 证明论意义上一致, 并且________}, 那么这个理论就不是完备的(即存在语句P使得理论既不证明P也不证伪P). 在哥德尔最初的证明中, "_______"部分只采取了一个不严谨的描述("effectively given formal system"). 哥德尔的决定多多少少是出于无奈, 因为当时并不存在一个严谨定义"effectively given formal system"的数学理论. 这个决定也给不完备定理的适用范围带来了不确定性(这个在研究哥德尔的文献中常被称作"the generality problem"). 丘奇 图灵等人开创的可计算性理论则回答了这一问题. 一个formal system是effectively given的当且仅当存在一个(图灵等价)的程序来"操作"这个system. 哥德尔本人对这个回答也十分满意:

When I first published my paper about undecidable propositions the result could not be pronounced in this generality, because for the notions of mechanical procedure and of formal system no mathematically satisfactory definition had been given at the time. This gap has since been filled by Herbrand, Church and Turing.

另一方面, Gentzen对PA一致性的证明则开创了序数分析这一方法, 使得集合论中非常基础的对象(序数)在证明论中起到了至关重要的作用.

哥德尔不完备定理还告诉我们理论的一致性可以被考虑作一个hierarchy (例如令T>S当且仅当T能证明S的一致性). 集合论中, 对于不同的大基数公理 , 形如ZFC+ 的理论到目前为止都可以通过这个一个hierarchy来测量它们的一致性强度. 在实际操作上, 我们往往会用到ZFC+ 的模型, 并且在其中构造出一个ZFC+ 的模型. 巧合的是, 目前数学中"自然出现"的独立于ZFC的命题, 都可以被证明与ZFC+某个大基数公理有着相等的一致性强度. 这一类的证明用到的方法(内模型法+力迫法)本质上也是模型论的方法.

令人惊讶的是, 可计算性理论中的一些构造方法可以被看作是forcing arguments的先驱, 参见Kunen集合论里面的remark:

力迫法的另外一个等价形式, 布尔代数模型, 则可以被看作对于经典二值模型论的一个推广.

内模型与可计算性理论的一个比较有趣的联系前几年被Koepke等人所发现. Koepke考虑了对于图灵机的推广, 使得程序运行时间可以有 的任意长度. 在这个"超限可计算理论"的框架下, 我们会得到一个令人深思的"丘奇图灵论题":

一个集合x是(允许有限个序数参数)"超限图灵"可计算的, 当且仅当

如果把可计算性理论看作"自然数的图灵可计算子集研究", 那么我们可以考虑更高的序数的"可计算子集", 或者考虑自然数的"带oracle的图灵可计算子集", 这一类研究统称higher recursion theory.

可计算性理论也常常会"反哺"集合论和模型论. 这样一个现象通常体现于在集合论和模型论常见的研究领域前加上"effective/computable"这样一个前缀, 就可以得到一个新的研究领域. 例如descriptive set theory ==> effective descriptive set theory; model theory ==> computable model theory.

集合论中, 许多大基数也有着等价的集合论刻画与模型论刻画. 例如一个基数 是strongly compact的, 当且仅当每一个 -complete filter都能被扩展成一个 -complete ultrafilter; 当且仅当对于语言 (即允许有小于 的任意长度的conjunction/disjunction/quantifiers)中的任意理论T, 如果T的每个小于 的子集都是可满足的, 那么T就是可满足的. (从这个角度上看, 就是一阶逻辑 的compactness cardinal).

我们不单止可以考虑compactness的推广, 我们还可以考虑一阶逻辑其他元定理在更强的逻辑上的推广. 例如我们可以说一个逻辑L的Lowenheim-Skolem-Tarski (LST) number是 , 当且仅当 是最小的基数使得: 如果M是一个L的模型, 那么M有一个大小小于 的L-初等子模型M'. LST number不单止可以"测量"一个逻辑与一阶逻辑有多"相似", 它们还可以刻画大基数或者本身就作为带有大基数性质的命题. 例如:

二阶逻辑的LST number存在当且仅当supercompact cardinal存在.
Vopenka's principle成立当且仅当每一个逻辑都有一个LST number.

这样一类研究方向叫做symbiosis, 见http://www.math.helsinki.fi/logic/people/jouko.vaananen/BaVa.pdf

有想到什么之后再继续补充