一、    报告概况

顾涛的报告主要论证明了一个基于克里普克语义学的knowing what 逻辑，其证明方法是对每个常项都引入一个二元模态词，使得这个模态词与某个Conditionally knowing what 逻辑的算子对应。通过证明含有这类二元模态词的逻辑的较为简单的完全性间接地证明了Conditionally knowing what 逻辑的完全性。

二、问答记录

Q：表示提问         A：表示回答           S：表示补充

李大柱Q：在Conditionally knowing what 的 first-order Kripke model 中 non-rigid 是什么意思。

顾涛A：是指非严格指示词，即这个常项在不同的可能世界下可能解释不同。

刘壮虎Q：在定义语言时我们的记法用到的符号其实是上层语言的符号，是types，应当与我们语言中的符号有区别。

顾涛A：是的，这种记法来源于计算机，其写起来比较方便。

王彦晶S：是的，这种记法被称为dnf，但我们用到的排版软件不方便讲希腊字母加粗。

刘壮虎Q：为什么我们总要讨论S5系统，为何在目前做完极小的系统后直接讨论S5系统。

顾涛A：可以去做当中的，比如KD45。

王彦晶S：S5是在实际中能用的，比如计算机，但如果要刻划实际的人，用模态逻辑都太强了。

李大柱Q：MLKVr+系统中，三角形那里的证明有对称更简单吗？

顾涛A：有对称之后其实更强。

刘佶鑫Q：在该系统中某些公理不是Shalquist的，那怎么证明完全性？

顾涛A：还是用典范模型证明。