您的位置:首页 > 成果推介
国家社科基金项目结项优秀成果推介:模态可定义性理论研究
发布时间:2015-11-09 08:43:24    浏览次数:

我校政治与公共管理学院逻辑学专业马明辉副教授主持的2012年度国家社科基金青年项目“模态可定义性理论研究”(批准号:12CZX054)结项成果被鉴定为“优秀”等级。该项目已发表论文10篇(其中国内CSSCI论文4篇;逻辑学重要国际会议论文4篇;国际著名逻辑学SCI期刊论文2篇)。该项目结项成果为专著《模态可定义性理论研究》(24万字)。

模态可定义性理论、完全性理论和对偶理论并称模态逻辑三大基础理论。模态可定义性理论是逻辑基础理论研究的重要内容。该项目在整理、分析和研究国际逻辑界关于模态可定义性理论已有研究成果的基础上,掌握前沿研究成果,深入研究模态可定义性理论的各个方面,丰富和发展了模态可定义性理论体系,做出了新的研究成果,提出了新的研究方向。

从内涵方面看,该项目研究了模态对应理论、模态可定义性的刻画等方面。从外延方面看,该项目的研究涉及古典模态逻辑、古典模态逻辑的扩张、非古典逻辑等等。首先,对应理论是可定义性理论的一部分或特殊情况。它关心模态语言和一阶语言在谈论框架性质方面的对应问题。模态逻辑与古典逻辑之间的互动是对应理论研究的课题。该项目将古典模态逻辑的一些结论推广至更丰富的模态或非古典逻辑。其次,由戈德布拉特和托马森证明的框架类可定义性刻画定理,本质上是贝克霍夫关于代数类的等式可定义性定理在模态逻辑方面的推广。该项目在研究过程中将它推广至其它方面,初步探讨了特殊框架类上的可定义性问题。

该项目对模态可定义性理论的研究主要创新性结论如下:

1)确定古典模态逻辑的撒奎斯特公式中一个子类,使得它们都是子框架公式,即其有效性对取任意子框架满足,进而得到在 K4 基础上增加这些撒奎斯特公理得到的逻辑具有有穷模型性。这种方法实际上是模态逻辑中从句发角度研究元逻辑性质的具体体现。撒奎斯特对应定理和完全性定理是研究古典模态逻辑的初等性、典范性和完全性的句法方法。本项目中关于有穷模型性的句法研究是新的研究方向。

2)基本命题逻辑本质上是模态逻辑K4的严格蕴涵片段,它可以通过哥德尔翻译嵌入模态逻辑K4。该项目研究了基本命题逻辑的一些扩张,它们是一些古典模态逻辑的严格蕴涵片段。在模型类可定义性问题上,通过将典范模型构造转化为素滤子模型的构造,得到了可定义性定理的结论。

3)分析研究对应理论的最新成果——算法对应理论,将其推广至直觉主义模态逻辑和其它命题逻辑。撒奎斯特对应定理中使用的算法本质上上是对阿克曼引理的运用,从而将与撒奎斯特模态公式等价的二阶句子转化为等价的一阶句子。算法对应理论是近年来发展起来的一种广义对应理论,它对分配模态逻辑进行研究,利用典范扩张中关于伴随算子或剩余算子的一些性质以及阿克曼引理,形成一些句法公式使得它们等价于的一阶公式可以通过一种在完美代数(典范扩张)上统一的算法而自动得到。该项目成果不仅对这些理论进行了分析介绍,而且将它们应用于一些非古典逻辑的对应理论的研究,获得了一些结论。

4)首次引进一般性的分配格模态逻辑,它的代数是加算子分配格。将算法对应理论推广至分配格模态逻辑。对该逻辑构造显式演算,运用对应算法扩展初始不等式。这是算法对应理论在证明论方面的首例应用成果。分配格模态逻辑具有较强的一般性,不仅包括在分配格上增加蕴涵算子的各种严格蕴涵逻辑,也包括分配模态逻辑、古典模态逻辑、直觉主义模态逻辑等等。该项目研究的结果具有一般性,可以在具体逻辑理论中加以应用。

5)将加标矢列式系统推广至直觉主义模态逻辑、基本时态逻辑、US 时态逻辑、将对应理论中的几何公式推广至其它逻辑。模态逻辑的加标矢列式系统是将模态逻辑的语义与证明系统相结合产生的,它简化了证明系统中逻辑规则的负担,使证明过程可以按语义方式进行。对应理论与加标矢列式系统的结合就在于,使用对应于某个几何公式的模态公式得到的模态逻辑具有良好的加标矢列式系统,而且这样的系统具有切割消除定理。

6)首次引进有穷链分层模态逻辑,给出它的撒奎斯特公式、加标证明系统等理论。分次模态逻辑(有穷基数的模态逻辑)的模型论已经得到了一些研究。本项目所研究的有穷链分层的模态逻辑与分次模态逻辑是不同的。有穷链分层模态逻辑本质上是古典模态逻辑的一种扩张,从代数上看有穷链分层代数是加算子布尔代数类的一个子类(因为它要满足更多的条件)。分次模态逻辑中的有穷基数的模态算子不是可加的和正规的,因此这样的代数类不是加算子布尔代数类的子类。

项目研究对今后逻辑学基础理论研究具有一定的参考价值。该项目在研究过程中得到了国内外学者的广泛支持。日本北陆先端科学技术大学院大学的佐野勝彥助理教授(项目组成员)、荷兰代尔夫特理工大学Alessandra Palmingiano副教授均是项目负责人的合作研究者。特别感谢佐野博士邀请项目负责人赴日开展为期三个月的合作研究,Palmingiano博士邀请项目负责人赴荷兰开展为期一年的合作研究。在项目研究期间,项目负责人与模态逻辑对应理论的主要创始人之一、荷兰阿姆斯特丹大学逻辑、语言与计算研究所教授Johan van Benthem也进行了深入的交流。通过该项目的研究,项目负责人与国际逻辑学界建立了良好的学术合作关系,为未来模态逻辑领域的基础研究工作打下了坚实的基础。