2023年10月24日，应中心主任郭美云教授邀请，挪威卑尔根大学教授、长江学者、教育部A类专家、西南大学客座教授、山西大学兼职教授Thomas Ågotnes到访我中心，在天辅逻辑论坛上为中心师生带来了题为“模态逻辑中的有人知道与弱合取公理”的报告。本次报告由熊作军副教授主持，李章吕教授、孙洋博士、中心在读研究生及学院部分本科生参与了此次报告。

报告伊始，Ågotnes教授介绍了“群体知道的推理（reasoning about group knowledge）”这一术语的含义。他指出，在日常生活中，我们几乎每天都会使用到“群体知道的推理”：像“学生们知道讲座何时开始”“我的父母知道这个周末我要去看他们”这样的句子便是一种“群体知道”的命题形式。随后，Ågotnes教授结合日常生活中的例子，生动形象地解释了四种“群体知道”类型的定义：普遍知道（general knowledge）、公共知道（common knowledge）、有人知道（somebody knows）与分布式知道（distributed knowledge）。其中，“有人知道”要弱于“普遍知道”，但要强于“分布式知道”。

讨论完四种“群体知道”的定义和关系后，Ågotnes教授接着介绍了基本认知逻辑中的语言与语义解释，着重强调不同框架下认知模态词的各种属性以及多主体认知逻辑中分布式知道、普遍知道和公共知道所具有的逻辑性质。随后，Ågotnes教授以“至少一个歹徒知道团伙内有人知道密码”这一命题为例，指出尽管我们可以用其他的认知模态词来等价地表达这一命题，但使用“有人知道”作为认知模态词可以在不牺牲语言表达力的情况下让命题的形式表达更加简洁。

在强调了“有人知道”这一认知模态词的重要性之后，Ågotnes教授给出了一个包含“有人知道”和K算子作为模态词的认知模态逻辑的语言与关系语义下的语义解释。他指出，在S5框架下，“有人知道”的负自省公理（negative introspection）不是一个有效式；而在一般情形下，“有人知道”的合取公理C也不是一个有效式，而“有人知道”的弱合取公理Bⁿ是一个有效式。因此，这一认知逻辑系统是一个非正规模态逻辑，也就不宜在关系框架下讨论。

Ågotnes教授强调，尽管在关系语义中“有人知道”的认知逻辑是非正规模态逻辑，但我们可以使用标准的邻域语义来刻画这一逻辑系统。由于K算子可以被“有人知道”定义，他将这一系统的语言简化为仅以“有人知道”作为模态词的版本。随后，他介绍了“有人知道”这一逻辑系统在邻域语义下的语义解释，并探讨了邻域框架EMNBⁿ的可靠性和弱完全性的证明策略。在探讨邻域框架EMNKⁿ和EMNBⁿ的关系时，Ågotnes教授指出，“有人知道”逻辑类似于Vardi（1986）的n度局部推断逻辑（the logic of n-bounded local reasoning）。在此基础上，他应用弱合取公理反驳了Allen（2005）关于EMNKⁿ在n度局部推断模型下可靠且完全的结论，继而得出EMNKⁿ真包含于EMNBⁿ的结论。在报告过程中，熊作军副教授就EMNBⁿ的弱完全性等技术问题同Ågotnes教授进行了深入的讨论，Ågotnes教授指出，由于邻域语义的特点，该系统现在还只是证明了弱完全性，其强完全性还是一个开问题。

报告结束时，与会师生以热烈的掌声感谢Ågotnes教授的报告。与会师生进一步结合自身研究兴趣，就不同类型“群体知道”之间的关系、高概率模态算子是否适用于邻域框架等问题同Ågotnes教授进行了深入的交流，进一步深化了关于多主体推理系统的理解。

（李斌/文，图；熊作军/审核，发布）