4月3日下午，来自荷兰格罗宁根大学哲学系的Barteld Kooi教授做了题为Completeness via correspondence for three-valued logic 的报告。

首先Barteld Kooi教授简单介绍了关于悖论的三值逻辑LP（Logic of Paradox）。与经典的模态逻辑不同，在三值逻辑中真值有三种情况，即真，假和i。一般而言，对于三值逻辑还没有给出完全的公理系统。Barteld Kooi教授借助经典模特逻辑的对应理论的方法给出了三值逻辑的完全的自然推演系统。经典模特逻辑的对应理论涉及模态逻辑公式和一阶逻辑公式的对应关系，包含模型论和证明论两方面的内容。例如，模特公式□φ →φ在框架F上有效，当且仅当一阶公式?xRxx在框架F上为真。并且将公式□φ →φ作为公理添加到系统K中后的系统相对具有一阶公式?xRxx所表达的性质的框架类是完全的。我们称这个模态逻辑公式刻画了这个一阶逻辑公式。与此相似，在三值逻辑中每一个算子确定一个真值函数f，每一个这样的真值函数有一个相对应的一阶公式?x?y ( f( x , y ) = 0 →f( x , 0) = 0)，和一个LP公式φ?(φ?ψ)/φ?ψ。Barteld Kooi教授证明了将这个LP公式作为公理加入到基本的自然推演系统后所得到的系统相对这个一阶逻辑公式所确定的框架类是可靠完全的，即这个LP公式刻画了这个一阶公式。这样就给出了一系列的三值逻辑的完全的自然推演系统。

接下来，来自印度数理科学研究所（IMSc）的Ramaswamy Ramanujam教授做了题为Decidable Fragments of First-order Logic的报告。在报告中，Ramanujam教授回顾了一阶逻辑可判断问题的历史，并介绍了相关研究的最近发展。

一阶逻辑的可判定性问题可以表述为：对于一个任意的一阶公式，是否存在一个算法，能够判定这个公式在某个模型上满足？在上世纪30年代初期，逻辑学家在一阶逻辑的某些片断上，得到了这个问题的肯定结果。但是1936年Church和Turing的工作证明了，对于整个一阶逻辑，可判定问题是算法不可解的。由此，研究者对于可判定性问题的兴趣转向了分类（classification）问题，即寻找一阶逻辑可判定性片断和不可判定片断之间的分界。常见的研究思路是在一阶逻辑的语法和语义上进行限制，考察一阶逻辑的某些片断在特定的模型类上是否可判定。如果可判定，还可以将这个片断扩张，再考察扩张之后的片断是否还能判定。这种扩张可以不局限在一阶逻辑的范围内，比如对于Monadic Second Order Logic的研究。语法上的限制的方式很多。逻辑学家成功地证明，对于一阶逻辑的前束类（Prefix Class），不管是其中可判断还是不可判断的片断，都能够予以刻画。也可以限制逻辑的字母表，考察一个特定的一阶理论的公式是否是可判定的。语义上的限制，则主要是着眼于一些具有特殊性质的模型类。比如某些一阶逻辑的片段在全部一阶模型类上是可判定的，但如果只考虑偏序模型，就会导致不可判定的结果。相比于一阶逻辑，模态逻辑具有良好的算法性质。有的研究者认为这是因为模态逻辑能翻译为一阶逻辑的某个只含有到两个变元的片断。最近的研究结果表明，对只含有两个变元的一阶逻辑的片段进行扩张，几乎都会得到不可判定的结果。但对模态逻辑进行类似扩展，却仍然能保持可判定性。因此，模态逻辑良好的算法性质或许是出于其他原因。比如，是因为它能翻译为一阶逻辑的某个安保片段（Guarded Fragment）。Ramanujam教授在介绍了一些关于Guarded Fragment的研究工作后，结束了此次报告。

本学期，Ramanujiam教授将在北京大学开设短期课程“一阶逻辑的可判定片段及扩张” 。本次讲座即是该课程的一个导论。来自北京大学以及北师大、清华等高校的师生参加了此次讲座，并在讲座结束后与Ramanujiam教授进行了交流。


（李延军、张力）