Advanced Modal Logic 2022

高级模态逻辑（2022 春季） Advanced Modal Logic (关于钻石与盒子的故事)
教师：王彦晶，时间：每周二 3-4节周四 3-4节地点：地学楼205

其他相关课程请见: logic.pku.edu.cn

小报告安排如下:

– Algebraic Modal Logic
主要参考：Blue book Ch. 5.2 （参考 Ch 5.1 及 5.3）
李一朴 & 顾屹非 5.26

– Neighborhood semantics for modal logic:
主要参考: Brain Chellas: Modal Logic – An Introduction: Ch. 7.1-7.4
辅助参考(背景等): Eric Pacuit: Neighborhood Semantics for modal logic.
刘彬 & 王林峰 5.31

– Complexity of Modal Logics
主要参考：Blue book Ch. 6.7
唐雯豪 & 许涵 6.2

– Completeness via canonical formulas：

主要参考：Larry Moss: Finite Models Constructed From Canonical Formulas. Journal of Philosophical Logic, vol. 36, no. 6, 2007, 605–640.

蒋凡一 & 阮立清 6.7

– Lindström’s theorems for modal logic：
主要参考：JvB. Modal logic for open minds: Ch. 25.3 and The blue book Ch. 7.6
文章：JvB. A New Modal Lindström Theorem. Log. univers. 1, 125–138 (2007).
欧阳明晖 6.9

– Guarded fragments:
主要参考：Blue book Ch 7.4
文章：Andréka, H., Németi, I. & van Benthem, J. Modal Languages and Bounded Fragments of Predicate Logic. Journal of Philosophical Logic 27, 217–274 (1998).

Lecture 24 (Slides) 我们介绍了PDL的语形和语义，以及test-free PDL的完全性证明。注意test-free PDL的表达力比PDL要弱，因为 $^*$ 里面的tests是不是能被消去的。证明完全性时，我们首先注意到PDL是不紧致的，所以不可能有强完全性。证明弱完全性时，我们可以用标准的典范模型构造做出一个“伪模型”，里面有所有 $R_pi$ 的关系，相对于直接使用这些关系的模态语义有trivial的truth lemma. 接着我们希望在给定一个一致的 $phi$ 的情况下，造出一个有穷的模型使得其在PDL的语义下能满足 $phi$ 。构造的办法是做filtration，但是这里有几点和标准filtration不一样的地方：1 $phi$ 的闭包不仅仅是 $phi$ 的所有子公式，因为根据公理，除了子公式外还要包括一些其他公式，特别是 $[pi^*]phi$ 这样的公式还要包括 $[pi][pi^*]phi$ 这样一步的展开，这在后面是异常关键的。2 我们不能直接用filtration lemma因为语义也发生了变化，我们要证明filtration定义中的两个条件从而得到保持公式真值的结果。在证明这样的条件时，我们很本质的应用了filtration是有穷的性质，用一个公式描述[s]在filtration中能够通过 $pi$ 通达到的点，把能通达转换成满足特定公式，再用归纳公理去证明之。最关键的是在这个有穷模型中把在伪模型中本来不可能走同的 $pi^*$ 的路一步步通过 $pi$ 走出来，之所以能走通是因为现在几个点合成一个点了，本来断开的路可以连起来了。在证明另一个条件的时候，很本质的应用了 $[pi][pi^*]phi$ 也在闭包中的性质，不断地走一步展一层再走一步, 注意最后的induction是对 $[pi]psi$ 最外面的 $[pi]$ 的结构做的，所以 $[pi][pi^*]psi$ 比 $[pi^*]$ 复杂度低。

延伸阅读：

关于non-contingency logic的完全性可以看我们的文章

关于window modality的完全性，可以看我们的文章

Lecture 21 (slides, 5月17日) 我们说用框架来刻画模态逻辑不是万能的。首先我们证明了KL对于任何的框架类都不是既可靠又是强完全的。使用的证明思路是找到使得KL可靠的最大的框架类，然后说明如果这个最大的框架类都不能使得KL强完全那么比它小的框架类也不能使得KL完全。这样我们就只需要证明一个“不完全性”结果就可以得到想要的“不可完全”的结果了。证明中我们利用了不紧致＝>没有强完全的事实。注意KL是可以相对于某个框架类可靠且弱完全的（书上Thm 4.45）。接下来我们介绍了一个相对于任何框架类都不（弱）完全的模态逻辑KvB（在具有可靠性的前提下）。证明思路是1 找到一个公式MV, 使得MV和VB定义了同样的框架类（因而所有使得VB有效的框架类也使得MV有效）。2.证明MV是不能从系统KvB中推出的。要证明一个公式不能从一个系统中推出，我们一般要借助其他的语义，用找反模型的办法：定义一个语义的有效关系( $Vdash$ ) 使得对任意 $phi: vdash_{KvB} phi$ 蕴涵 $Vdash phi$ （可靠性）。这样如果 $phi$ 不在 $Vdash$ 的意义上有效，则phi不能在KVB中证明。我们可以基于一般框架（框架＋受限制的赋值集）定义 $Vdash$ 。我们首先要证明相对于 $Vdash$ ，KvB是可靠的。然后证明MV相对于 $Vdash$ 并非有效：注意在一般框架上，vB的有效性并不意味着MV的有效性。一般框架可以被认为是框架加上允许的赋值集。

特别的，KMV相对于MV对应的框架类是完全的，而且KMV可以推出vB公式（vB的后件在 $Box bot$ 的前提下可以推出来）。一般的说, 如果在语言中可以用两个非常不一样的公式定义一个性质的时候, 要小心只加一个公式为公理的正规模态逻辑是不是完全的.

我们之后讲了一个一般性的完全性结果：所有正规模态逻辑都相对于使其有效的一般框架的框架类既可靠又完全（注意从任意admissible的赋值到典范赋值的切换）。之后我们简单说了说Sahlqvist完全性定理的基本证明思路。

Lecture 20（Slides, 5月12日). 我们介绍了可靠性和完全性的概念，点出了强完全和弱完全的关系，之后介绍了利用典范模型证明正规模态逻辑完全性的基本方法：将相对于某个框架类的完全性归结到一致公式集在这个框架类中的可满足性，然后用极大一致集构造这个逻辑的典范模型使得任何一个一致的公式集都在典范模型中相应的极大一致集的点上可满足，然后我们只需要证明这个典范模型确实是基于我们想要的框架类中的框架的即可。特别要注意的是在某个框架类中缺乏（模型）紧致性的逻辑是不可能相对这个框架类同时具有可靠性和强完全性的。另外注意，如果不要求完全性的时候证明可靠性，规则可能不保持有效性。我们把一个逻辑（公式集）称作是“典范的”如果它的典范模型是基于一个使得这个逻辑中的公式都有效的框架的。一个重要结果（之后讲证明）是将Salqvist公式作为公理加入到系统K中得到的逻辑是典范的，进而相对于具有这些公式所对应的一阶性质的框架类强完全。

Lecture 19（Slides，5月10日) 课上先总结了框架一章的内容，从抽象的语形角度看模态逻辑, 引入了正规模态逻辑的概念（注意书上对多元模态逻辑基本正规系统的定义有问题），用几种方式定义了语法后承，并介绍了这些定义背后的思想。注意一个系统的admissible 的推演规则未必在该系统的扩张中也成立。模态逻辑中与基于前提推演相关的问题: 语形和推演概念和语义的后承概念应该如何定义? 我们看到，模态逻辑是可以有演绎定理的，要注意的是诸如统一代入规则与必然性规则只能作用于系统的定理，而不能作用于通过假设得到的结果。从语义的角度看，这两个规则只保持全局的有效性，而不保持局部（点模型）的真值。之后我们定义了语义后承，注意通常我们使用的语义后承是局部保真的，否则会出奇奇怪怪的问题，不过在其他一些应用场景中，全局的语义后承也有一定作用。请参考下面几篇文章。

延伸阅读：Raul Hakli, Sara Negri.Does the deduction theorem fail for modal logic? Synthese (OF:29 March 2011).

文学锋：模态逻辑教学和教材中易犯的⼏个错误《逻辑学研究》2018冬季号特刊

Xuefeng Wen: Modal Logic via Global Consequence. WoLLIC 2021: 117-132

Lecture 18（Slides, 4月28日) 我们介绍了用Jankov-Fine公式刻画一个有穷传递点模型的基本思想，讨论了一个框架类模态可定义性的刻画结果的证明思路。限制在有穷传递框架上来说，一个框架类可以被一个模态公式集定义当且仅当它对（有穷）不交并，生成子模型以及有界态射的象封闭。基本思路如下：给定一个框架类K，我们先找到可能定义它的公式集Σ（在这个框架类上有效的所有公式），然后证明这个公式集就确实可以定义K。关键要证任给一个框架F如果F使得Σ有效，那么F一定在K中。证明的办法就是要把F和K中的某些框架用K的一些封闭操作给联系起来。

之后我们讲解了Goldblatt-Thomason 定理的证明。基本思路同有穷传递框架的技巧，只不过我们不能用有穷的公式或公式集来刻画框架了。大概证明如下：不失一般性，我们还是假设待考虑的框架F为点生成框架，然后给它的每个世界集一个名字，用一个新的原子命题符号来表示（这里要扩充模态语言），并给一个特别的赋值V使得那些原子命题只在对应的世界集上为真（其他原子命题可以都赋值假），这样我们在之后的讨论中其实可以用这些特殊命题字母代表所有公式去处理。之后我们考虑(F,V)所满足的所有（新语言的）模态公式的集合Δ。我们可以证明Δ在K中可有穷满足，因而Δ在K中可满足（因为K可被一阶定义，则K对超积封闭，用超积可以造模型）。这样我们也能得到F在K中的一个“内应”了（还有一个特殊赋值V’和特殊点w’），我们还可以使得这个模型变成饱和的G,V’，同时G,V’,w’也满足Δ。注意，这里不失一般性我们可以假设G是从w’生成的。然后（按书上的办法）我们可以定义从G,V’到F,V的超滤的一个有界态射f: 令f(s)为G,V’,s上为真的P_A的那些A的集合。我们首先要证明这个定义是良定义，即f(s)确实是一个ultrafilter。这里要用到一个重要结果即：F，V上有效的公式也是G，V’上有效的(需用到点生成的特性和Los theorem)。之后我们证明 $f(s)＝ u$ 当且仅当 s和u满足同样的模态逻辑公式（包含P_A的）。这样其实f也可以被看作一个模态等价关系，又因为模态等价在模态饱和模型上和互模拟等价，我们有f就是一个互模拟也是有界态射。同时f也可以被看作一个F到G的有界态射。最后我们需要证明这个有界态射是满的，这里还要用到生成子模型的特性以及构造G的饱和性（比m饱和要稍强些）。最后我们就把G和F的超滤扩张用满有界态射联系起来。因为K对超滤扩张反封闭，所以F也应该在K里。

另外，ultrafilter extension （从小到大）不能保持模态公式的有效性所以不能到封闭性里：考虑L“ob formula和F=(N, >) 注意不是<关系，Ue(F)里non-principle 的ultrafilter是自返的，而Lob公式要求没有无穷下降链。

Lecture 17（Slides, 4月26日）我们希望找到Sahlqvist formula 在一阶中的对应片段（Kracht formula）：任给一个Sahlqvist formula 有一个Kracht formula和它相对应，同时任给一个Kracht formula 它对应于一个Sahlqvist formula （而且这个对应的Kracht formula 可以通过一定算法compute 出来）。在给定一个Kracht formula找Sahlqvist formula的时候，最关键的想法是要通过原子公式还原出POS及BOX－AT来，这个是有一定之规的，详情请请参考slides及蓝皮书。注意书上这节很多问题，不是每个Sahlqvist formula都可以变成一个书上定义的Kracht formula，另外对于普通量词适用的公式变换并不适用于受限制的量词, 特别的书上173页的3.20公式是不对的. 其实要求证证明，用书上的路子应该是走不通的，关于更一般的Sahlqvist片段和更一般的Kracht定理的证明可以参考这里的文章：

Stanislav Kikot (2012) An extension of Kracht’s theorem to generalized Sahlqvist formulas, Journal of Applied Non-Classical Logics, 19:2, 227-251, DOI: 10.3166/jancl.19.227-251

关于 Guarded Fragment可参见：

H. Andreka, I. Nemeti, and J. van Benthem. Modal logics and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, June 1998.

Lecture 16（Slides, 4 月 21 日）我们回顾了 Sahlqvist 片段的最核心的思想：找到满足前件的（所有）极小赋值，然后将赋值的定义带入公式替换一元谓词。之后我们定义了Sahlqvist蕴涵片段和更一般的Sahlqvist片段。给出了Sahlqvist算法的框架，回顾了这个算法中各个操作的直观，注意这里 $Diamond$ 可能出现嵌套的情况，要先把里面 $Diamond$ 对应的存在量词拿到整个implication外面去。最后我们介绍了一些负面的结果。我们也提到不是所有基本模态逻辑的结果都可以推广到任意元算子的模态逻辑上，比如Sahlqvist的片段对于 $Box$ 可以处理， $nabla$ 基本不行。

补充阅读：

Sahlqvist 的文章

一个推广

王心宇同学写的Sahlqvist自动转换程序（github，有建议或者bug请联系s2010404@jaist.ac.jp）

Boolos的文章For every A there is a B

Lecture 15（Slides, 4月19日) 我们开始研究什么样的模态公式有对应的一阶公式。基本的想法就是考虑在什么情况下可以消掉模态公式标准二阶翻译中的二阶量词。注意这和一阶理论的量词消去不同，我们没有预设特殊的数学理论。当然对不涉及命题变元的模态公式来说，这一定是可以的。稍微麻烦一点的是考虑每个命题变元都是以统一的正负形式出现的公式。这种公式相对于命题变元的赋值具有单调性：如果一个命题变元在公式中都是正出现，那么使得该命题变元在更多的世界上成立同时也能使得该公式在同样或更多的世界上成立；类似的如果一个命题变元在公式中都是负出现，那么使得该命题变元在更少的世界上成立也能使得该公式在同样或更多的世界上成立。利用这个特性，我们只考虑相应的最大最小赋值即可，反映在公式中我们可以在二阶翻译中删掉二阶量词并把每个Px换成neg x=x （若p在模态公式中正出现）, 然后把每个Qy换成x＝x（若q在模态公式中负出现）。注意，虽然公式的单调性要求“其他赋值不变”我们总可以从最大最小赋值开始逐渐变成任意的赋值而保持公式的真值不变。接着我们给出了一个模态逻辑公式翻译成一阶公式的例子，最核心的思想是找到满足前件的（所有）极小赋值，然后将赋值的定义带入公式替换一元谓词。之后我们又给出了很多模态逻辑公式翻译成一阶公式的例子。特别注意，极小赋值也许不止一个，这时要想办法通过一阶语言来概括所有这些极小赋值。对Diamond前件的公式这是可以做到的，可以用一阶量词来说二阶量词能说的事情。

关于Ceteris Paribus Laws
关于Lambda 抽象的哲学作用可以看Fitting and Mendelsohn的First-order Modal Logic和我们的文章（用assignment 替代lambda抽象）。

Lecture 14（Slides, 4月14日）我们就讲了两个模态可定义而一阶不可定义的框架类的例子：Löb公式和McKinsey公式。证明一个模态公式定义了一个框架类不是一件特别简单的事，关键在于造反模型的时候要考虑所有的情况，不能只对特殊情况定义一个赋值，一般来讲可以试着找到一个统一的赋值一揽子生成所有不满足性质的框架上的反模型。特别的，需要考虑几个点重合的情况。另外，证明一个模态可定义的框架类不可一阶定义，可以利用一阶逻辑的性质，比如紧致性和洛文海姆斯库伦性质。例如，对于McKinsey公式，我们可以找一个框架使得该公式有效，根据向下的洛文海姆斯库伦性质，就有一个包含特定可数集的可数子框架与原始框架初等等价，但是可以证明这种可数子模型一定不会使得McKinsey公式有效。注意：这里可利用一个简单的基数 argument，我们可以说明原始的不可数模型变成一个可数模型之后肯定有两个互补的“子集”点都不在那个可数模型中。之后我们把模型上的构造推广到框架上，然后强调了他们保持模态公式有效性的方向（直观是“从大到小”），利用这些模型变换我们可以证明一系列框架的一阶性质是模态不可定义的，同时也有模态逻辑和一阶逻辑都不能定义的框架性质，这样我们就理清了模态逻辑和一阶逻辑在跨框架可定义性方面的关系。

关于可证性逻辑，也可见Modal Logic for Open Minds第二十一章

Lecture 13（Slides, 4 月 12 日）课上介绍了对于框架的研究的缘起。按照局部／全局以及模型／框架的维度组合，我们列举了模态逻辑的各种有效性概念，通过这些概念，我们可以试图用模态逻辑定义各种结构和结构类。特别的，任意一个模态公式都定义了一个点模型类或框架类，但是并非每个模态公式都可以定义一个模型（在一定等价关系的意义下）。我们特别提到，一个框架类可定义并非等价于基于这个框架类的模型类可定义，这样我们不能把框架类的可定义问题简单划归为模型类的可定义问题。之后我们还引入了相对可定义的概念，并强调它不等价于两个类的交的可定义概念。课上我们看到模态逻辑在框架有效的层面上其实对应于二阶逻辑的一个片段，不过很多模态逻辑的公式从定义框架类的角度讲也有对应的一阶逻辑公式。我们下面就要看是不是所有模态可定义的框架类都是一阶可定义的。

补充材料：关于MSO 可参考这个slides，和王一廷的 slides，如果感兴趣的话，可以看这篇文章.

Lecture 12（Slides, 4月7日) 我们讲了两个模型类直接可定义定理，基本上的想法是把一阶的可定义性刻画定理中的isomorphism换成bisimulation即可。注意补类封闭性的应用：如果没有关于complement的条件，定理不成立，只有对ultraproduct和bisimulation封闭还不能保证能定义。证明一个点模型里类能够被模态逻辑定义时先要划一个范围，大概这个定义公式集是啥样的，然后再证明这个公式集确实可以定义K。最后这个刻画定理，可以用更模态的方式给出，用ultrafilter union 替代ultraproduct，用ultrafilter extension替代ultrapower。之后我们串讲了模型这块的基本概念。Slides里没有强调的是很多重要的证明思想，比如先划范围再逼出一个东西（van Benthem 定理第一部分）、“曲线救国”（van Benthem 定理第二部分）、 “里应外合”（模型类可定义性定理）、“没有枪没有炮我们自己造”（ultrafilter extension 定理里面造后继先做个胚子再扩张），可以用任意给定模型的性质等等。

延伸阅读：Yde Venema, Ultrafilter Unions: an exercise in modal definability

Yanjing Wang, Francien Dechesne: On Expressive Power and Class Invariance

Lecture 12（Slides, 3月31日)。这节课我们先回顾了van Benthem定理的证明，之后证明一阶公式是否在bisimulation下保持的问题是不可判定的，所以，一般而言，即使有了刻画也不能用一个统一的办法看每个公式是不是对应于模态公式。接下来我们讲解了Rosen刻画定理的证明。Rosen的结果把有穷模型上的模态逻辑从有穷模型上的一阶逻辑里通过互模拟不变性刻画出来。大家要注意，很多逻辑性质，在只考虑有穷模型的时候就不成立了，比如一阶逻辑的紧致性。另外，一个公式在有穷模型的互模拟下保持不变并不一定意味着它在互模拟下保持不变（比如考虑一个只有无穷模型的公式）。为完成Rosen刻画定理的证明，先证明了在k－互模拟下保持不变的一阶公式肯定等价于某个模态度为k的模态公式：模态深度最多为k的模态公式可以定义所有由k-互模拟等价类组合而成的模型类。通过研究互模拟下保持不变的一阶逻辑公式的局部性，我们知道这些一阶逻辑公式在某个足够大的k-互模拟下也会保持不变（k>＝2^q-1，其中q是一阶逻辑公式量词的quantifier rank）。用到的技巧是EF-game和“危险区”的想法：defender的策略就是保证已经选择的点周围危险区内的点都能够形成partial isomorphism，而如果在已选择的点的危险区外，我们就不用和已选择的点作联系了。这样就完成了Rosen刻画定理的证明。这个证明其实也可以被用来证明原始的van Benthem刻画定理。

另外Rosen定理中的证明也适合于van Benthem的原始定理（相对于基本模态语言来说）。其中对的similarity type O 及 propositional letter 集P的有穷也可去掉（基于一阶逻辑和模态逻辑公式的真值不依赖于公式中不出现的符号所对应的语义结构）。大家可以试试如果利用基于有穷P，O的Rosen定理怎么能推出基于不受限制的P，O的Rosen定理。

本课讲解的证明基于Martin Otto下面这篇文章（但是Otto没有最后的细节证明）：

延伸阅读 Matin Otto: Elementary proof of the van Benthem-Rosen characterisation theorem
Eric Rosen: Modal logic over finite structures, Journal of Logic, Language and Information 6(4):427-439, 1997

关于EF game的winning strategy可以参考这里的相关证明

关于一阶逻辑的 Locality Theorem，可以参考这个简短的 abstract

Lecture 11 （Slides, 3月29日）我们介绍了超滤的第二个直观：定义一个集合中“大子集”的集合。每个“大子集”都可以看成一个包括原来集合中“绝大多数”元素的集合（考虑非主滤的超滤）。超滤在数学中应用很多，我们举了0-1有穷可加测度以及阿罗不可能定理的例子。我们之后定义了超积与超幂，介绍了L o’s 定理并用它证明了模态逻辑的紧致性。L o’s 定理可以保证超幂能保持一阶公式的真值，我们继而可以通过 $omega$ -饱和性证明了基于可数不完全超滤的超幂一定是m饱和的。这样我们就可以“曲线救国”证明van Benthem的刻画定理。然而，这个证明是非构造的，复杂的，依赖于紧致性和一阶逻辑模型论的各种无穷构造。下节课我们讲一个有穷的，模态的证明方法。

延伸阅读：David Galvin：Ultrafilters, with applications to analysis, social choice and combinatorics

关于社会选择理论阿罗定理详细的介绍可看魏来同学的 slides

Countably incomplete ultrafilter的ultraproduct的饱和性的证明请见Chang和Keisler的Model Theory的定理6.1.1。

关于计算社会选择理论（Computational Social Choice）

Lecture 10（Slides 同上， 3月24日）我们开始研究模态逻辑和一阶逻辑的比较。首先我们可以把克里普克模型也看成一阶结构 (其实一阶结构也可以看成克里普克模型..). 我们给出了从模态逻辑到一阶逻辑的标准翻译（如果是基本模态逻辑语言，则可以只用两个变元就够了）。这个翻译某种意义上是“语境依赖”的(角标 $x$ )，子公式的翻译要取决于它在公式中的位置，可能同样的子公式出现在不同的公式中他的翻译是不一样的（这个不同体现在变元上面，比如同样的基本命题变元p在翻译时可能变成Px或者Py）。我们可以证明在标准翻译下，一个模态逻辑的公式与它所对应的一阶逻辑公式等价，也就是说它们在任何模型上同真同假（或者说使它们定义了同样的模型类）。基于这个结果，模态逻辑从一阶逻辑那里继承了紧致性及勒文海姆-斯科伦性质。

接着我们开始讲将模态逻辑从一阶逻辑公式里刻画出来的van Benthem定理。我们首先证明了一个相对简单的刻画定理：模态逻辑恰好是一阶逻辑的在模态等价下保持不变的片段。这里面用了两个重要思想：1 证存在性可先划定范围，再从这个范围内逼出存在性；2 如果假设什么东西存在那么可以从这个东西上挖掘信息辅助证明（模型上成立的公式）。这个结果说明，在有紧致性的前提下，对于逻辑区分能力的度量可以帮助刻画逻辑的表达能力。

Lecture 9（Slides, 3月22日）助教首先讲评了作业，之后在录像中我们首先证明了超滤扩张能够保持模态公式的真值（注意：有时候为了证明一个结论需要证明一个更强的结论，因为更容易应用归纳假设）。在证明Box phi的情况时，我们需要在超滤扩张中找到合适的后继，这时我们用了构造的办法，先看看这个后继要满足什么条件，然后根据这些条件做一个“胚子”，之后再根据有穷相交性说明这个集合可以扩充成一个超滤子。类似的证明超滤扩张是模态饱和模型我们也要用到类似的构造。这里要理解超滤扩张中“应有尽有”，“应连尽连”的直观。

之后我们总结了不同逻辑间区分能力与表达能力的比较(在同样的模型类上)，表达能力的比较更细致，但有的时候区分能力的强弱关系也可以决定表达能力有同样的强弱关系（比如我们未来要讲的van Benthem刻画定理就是用区分能力的限制刻画表达能力）。

补充信息:

从模态逻辑的角度看一阶逻辑：
Johan van Benthem, Modal Foundations for Classical Logic, Chapter 27, Modal Logic for Open Minds, CSLI
Yde Venema, A Modal Logic For Quantification And Substitution, Logic Journal of the IGPL 2 (1)

Lecture 8（Slides, 3月17日) 我们首先讲了滤模型的定义，在其中我们对关系提出了两个要求，凡是满足这两个要求的关系都可以构成滤模型中的关系，因而基于一个给定的模型和一个公式（看成子公式封闭的公式集）我们可以有多个滤模型。注意在涉及等价类的定义中，要证明代表元的选取不会影响定义。另外，语言中初始符号的选择会影响定义和证明，要小心（见补充材料）。之后，我们引入了最后一种重要的模型构造方法：超滤扩张。我们希望可以把一个克里普克模型加一些点变成一个模态逻辑等价的模态饱和模型。我们先介绍了超滤子的第一个直观：一个可能世界集上的超滤子可以被看成“潜在公式”的一个极大一致集。特别的，主滤子是那些由一个点生成的超滤子，另外还有一些不是主滤子的超滤子，将在我们的超滤扩张中起到重要作用：他们是增加的可能世界。我们定义了超滤扩张，特别强调了超滤扩张中关系定义的直观。

补充：

文学锋老师关于 Box / Diamond 做初始符号的常见问题的文章。
模型检测不可判定但可满足性可判定的逻辑（注意这里模型检测是在epistemic model上不可判定，在extended model上可判定）

Lecture 7（Slides, 3月15日, 3月29日上午10:10前交第二次作业）我们开始介绍模型构造和转换的一些办法。我们可以证明通过这些构造得到的新的点模型，使得它和原点模型间是互模拟的，从而证明这些构造不会改变模态公式在特殊点上的真值。利用这些模态公式在这些构造下保持不变的结果，我们可以证明一系列模态不可定义性的结果。通过对模型的树展开进行深度和广度的“修剪”证明了模态逻辑具有有穷模型性。这种方法有一个缺点：我们通过树展开和修剪枝杈得到的有穷模型未必具有我们希望的性质（从而不见得属于特定模型类）。我们其实还可以对任给一个公式的模型做相对于公式中出现的有穷符号片段做k-bisimulation或者ML_k的contraction，也能得到有穷模型。我们还提了各种把点之间关系变成点集之间关系的lifting的方法，请注意量词的使用。

Lecture 6（Slides, 3月10日) 课上我们总结了bisimilarity与模态等价之间的关系以及与之相对应的各种bisimulation games。希望大家至少能够熟悉Game、自动机或者语义图中的一种方法，会对处理很多逻辑的判定性问题有帮助。我们主要讨论了互模拟和逻辑等价性之间的关系。我们引入了模态深度的概念，证明了当命题变元只有有穷多个，模态词也只有有穷多个的情况下，模态度最大为n的模态公式在逻辑等价的意义上最多有有穷个（用命题逻辑真值表有穷的思路）。利用这个结果我们在有穷多个命题变元的情况下证明了n-互模拟＝ML_n的逻辑等价，继而证明了 $omega$ －互模拟＝模态逻辑等价。我们开始考虑在什么样的情况下，bisimilarity等同于模态的逻辑等价关系。我们首先证明了在像有穷的模型类上，bisimilarity和模态等价是一回事，之后我们又引入了一个比像有穷更一般性的模型性质：模态饱和性。我们证明了在模态饱和模型类上互模拟与模态逻辑等价性是一样的。事实上，m饱和性的定义可以很自然的bridge证明中的gap。它也可以被看成一阶逻辑模型论中的饱和概念在模态逻辑中的应用（以后的课也会谈到）。它的重要性主要体现在之后重要结果的证明中，例如，我们在后面的课将会看到任何一个模型都能被转换成一个与之模态等价的m饱和模型，所以m饱和模型可以被看成普通模型的“理想代表”。之后的作业中会让大家证明m饱和模型类是至少包含它自己的模型类里具有Hennessy–Milner性质的最大的模型类，也就是说它不可能再被扩充了。

补充阅读:

关于Dialogue games

PS 无穷轮的bisimulation也是determined (source: Johan van Benthem, by Gale-Stewart Theorem 这个定理可以参考这个文档)

Lecture 5（Slides, 3月8日）我们首先简述了集合论领域对于互模拟的发现：在非良基的集合论里，集合可以被看成图属于关系看成边，而集合间一个自然的等价关系恰恰是他们对应图的互模拟关系。非良基的集合论可以用来直观地定义无穷的stream和无穷树，对于计算机科学很重要。bisimulation特别适合处理带环的图的等价性。很多带环的图可以体现结构主义的精神：一个点的意义在于其与其他点的关系，比如google的page rank。在结构主义数学基础中也有一派是做Synthetic Math。我们之后从游戏的角度去看互模拟。首先我们引入了比较抽象的 Game 的概念，其实很多逻辑中的概念都可以和游戏建立起比较精确的联系，事实上按照 Hintikka 的说法，逻辑的产生还和 Game 有渊源：是亚里士多德在给柏拉图学院编制对话游戏的手册的时候发现有些话之间有很有意思的关联，说了一句之后，后面有些话就不能说了，否则感觉就矛盾了，这起发了他的三段论的工作。我们讨论了二人有穷深确定性完美信息胜负游戏的判定性定理的证明。可以通过自下而上的标记或逻辑公式的否定（及排中律）来证明游戏双方中肯定有一个人有必胜策略。我们还举例说明了“二人”、“确定性”以及“完美信息”条件的重要性，并与Hintikka的Independence friendly logic（IF-logic）做了联系：IF-logic里的公式可能包含不受前面量词辖域限制的量词，这些公式的语义恰恰是通过不完美信息的博弈给出的。我们还讨论判定性定理在国际象棋上的应用。之后我们证明了互模拟和互模拟游戏中Defender存在winning strategy的对应关系。n-互模拟对应n轮的互模拟游戏， $omega$ -互模拟对应任意有穷轮的互模拟游戏，标准互模拟对应无穷多轮的互模拟游戏。特别的，游戏的角度是有一些特点的，比如要证两个模型不是互模拟的我们很多时候只需要找到一个 spoiler 的winning strategy 即可，按照原始定义的话，要说明任何的 bisimulation 都不 work。

关于Logic and Games 的一个综述
关于 Abelard and Eloise
博弈语义（Game Semantics）的起源
关于计算机里对无穷游戏、（二阶、不动点）逻辑和自动机关系的讨论见 Automata, Logics, and Infinite Games
特定无穷游戏的判定性（determinacy）也可以用来构建数学基础
关于 Game transformation 和 equivalence

Lecture 4（Slides, 3月 3 日）课上我们回顾了互模拟在模态逻辑里的发现过程，研究了它的定义，指出了一个看似简单的替代定义是循环的。我们强调了互模拟的局部性，余归纳性的特点。粗略地说归纳定义的特点是要找满足特定不等式（封闭条件）最小的解，可以从最小的集合构造；而余归纳是要找满足特定条件最大的解，可以从最大的集合“破坏”得到（不断剔除不属于的）。同时余归纳的定义一个集合可以通过归纳定义其补集实现（因而叫余归纳）。一个模型中的互模拟等价关系（Bisimilarity）可以被看成某个作用在二元关系上的函数f的最大不动点，由Knaster-Tarski定理保证这样的最大不动点存在，可以通过函数从全集开始的超穷迭代得到（Kleene不动点定理保证）。这也给了我们一个在有穷模型中找互模拟等价关系一个办法：从全关系开始进行有穷次迭代总能找到那个最大不动点。每个互模拟关系R都是不等式R包含于 $f(R)$ 的一个解，而互模拟等价恰是那个最大的解。从不动点的角度看互模拟也是计算机界之所以能发现互模拟的原因。标准的互模拟不能用简单的归纳方式定义，不过我们可以用 $n$ －互模拟逼近标准的互模拟（不过所有 $n$ －互模拟等价的交并非就是互模拟）。

延伸阅读(包含本课讲的不动点的内容)：

D. Sangiorgi, On the origins of Bisimulation and Coinduction. ACM Transactions on Programming Languages and Systems, Vol.31, No.4, 2009.

关于bisimulation的算法可参考这篇文章

这几节课的内容基本上在教材上没有，还请大家看老师给的参考文献。另外，也请大家及时阅读教材里涉及模态逻辑语义以及 bisimulation 的章节。

Lecture 3 （Slides, 3 月 1 日) 第一次作业 3.15 10:10am前在课程网本研合上课中提交（ $\text{[math]}$ 模板，如何画图可以参考模版里的第三题里的图，可以用xy-pics这个包）。课上我们先回顾了上节课的内容。之后我们考虑模型间等价关系的两种定义方式：1 通过模型间的结构关系定义 2 通过某种逻辑下的等价关系定义：两个模型被视作等价如果他们不能被某种逻辑语言中的公式区分（即不存在一个该逻辑的公式在这两个模型上分别为真和假）。对于模型间的每种结构等价关系我们希望通过某种逻辑的等价性来刻画。我们解释了为什么希望要有刻画的结果：1. 如果先有一个逻辑，可以试图用一个结构等价关系刻画其逻辑等价关系，从而对这个逻辑的区分能力（甚至表达能力）有更清楚的认识。2. 如果先有一个结构等价关系，可以试图用一个逻辑等价关系来刻画这个结构等价关系，从而能更清楚的看到这个结构等价有什么意义：什么样的性质（用逻辑语言表达）能在这个结构等价关系下得到保持。

之后我们看了一些简单例子，比如考虑有多个一元模态词的语言，每个模态词 $Box_x$ 在模型中对应关系二元 $R_x$ . 我们可以定义trace等价：看两个点模型里能走出来的路（abc这种有穷序列,…）是否一样. 这个结构等价关系，对应的是模态逻辑的一个小片段，里面只有 $diamond_x diamond_y…diamond_z top$ 这种公式。之后我们接着看一些更复杂一点的例子。课上这些例子来源于进程代数，在那里研究者关心的是各种进程（process）表现出来的行为 (behavior) 即能观察到的表现。根据不同的可观测能力，进程之间可以定义有不同的等价关系，可以用模态逻辑进行刻画。我们举了一个例子，说明在证明逻辑等价刻画结构等价的时候，对公式作结构归纳证明是最自然的，但是这时要注意应用归纳假设的条件是否适用（回忆课上的例子，可称为“ $omega$ -手观音”大战“如来佛”）。

我们之后梳理了模态逻辑中互模拟这个概念的发现过程，从数学中常见的同态开始加“当且仅当”条件得到强同态，再为了保持模态公式考虑满射强同态，因为满射条件太强又把第三个条件拆成Zig-Zag条件得到有界态射（也叫p-morphism），最后把函数换成关系就得到了互模拟。我们下节课继续理解互摸拟定义的特点，并且从另外两个领域看互模拟概念被发现的历史。

关于structural equivalence在理论计算机中应用的延伸阅读：
R. J. van Glabbeek The linear time – branching time spectrum CONCUR ’90 Lecture Notes in Computer Science, 1990, Volume 458/1990, 278-297

Lecture 2（Slides，2月24日）课上我们介绍了模态逻辑的语言、克里普课模型和克里普克语义。注意：克里普克模型里面的点可以有多种解释，不同的解释可能会带来技术上的不同发展与限制；零元模态词可以对应框架世界集的一个子集；模态语言的similarity type给出的是逻辑符号，不像一阶逻辑的字母表是非逻辑符号；克里普克模型中每个点的意义来源于上面成立的基本命题变元以及这个点和其他点的关系；注意多元模态词的定义中的量词。我们还给出了全局模型检测的labelling方法，提示了基于矩阵表示的模型检测算法的基本想法。之后我们定义了模态公式的点模型可满足，模型全局可满足，点框架有效，框架有效的概念（按模型／框架，局部／全局分四种情况）

补充材料：

关于逻辑常项的技术讨论，可以看这篇文章，可以自己搜索 logical constant in modal logic 的文章
关于模型检测 (Model Checking)
宇宙的原子个数
初始符号用Diamond 还是Box 在证明系统那里是有区别的，可参考文学峰老师的文章，等讲到后面再细讲。
可以用Context-free grammar 画画
Worlds vs. Possibilities/states的早期文章

关于可能世界语义起源的文章可见（请自己试图找到文章的pdf）：

B. Jack Copeland: The Genesis of Possible Worlds Semantics. J. Philosophical Logic 31(2): 99-137 (2002)
Max Cresswell: Modal Logic before Kripke. Organon F 26(3),(2019)
B. Jack Copeland: Meredith, Prior, and the History of Possible Worlds Semantics. Synthese 150(3): 373-397 (2006)

Lecture 1（课程介绍，Slides，2月22日正月初二星期二）在课程介绍之后，我们从对模态逻辑的不同描述出发，试图从不同角度认识模态逻辑：模态逻辑作为非经典逻辑起源于C刘对于严格蕴含的讨论，由此引出“可能”与“必然”；模态逻辑作为一个领域是关于各种模态词的逻辑的总称；命题模态逻辑的语言是通过命题逻辑语言加上各种模态算子得到的；模态逻辑在克里普克语义下是讨论关系模型／框架性质的逻辑；模态逻辑在模型类定义能力的意义上是一阶逻辑的一个片段，在框架类定义能力的意义上是（一元）二阶逻辑（MSO）的一个片段；最后模态逻辑的可满足性问题是可判定的。在本课中，我们通常是从（抽象）模型论的角度谈论具体的逻辑，一个逻辑指的是一个三元组<逻辑语言，模型类，可满足关系>。基本模态逻辑即为<命题模态逻辑语言，关系模型类，克里普克语义>。它具有如下三方面的优点：1. 关于模态词的语言简单直观，2. 关系模型应用范围广泛，3. 在克里普克语义下模态逻辑是一阶逻辑的一个性质良好的片段（就点模型可定义性而言）：紧致性，有穷模型性，互模拟下的不变性，以及可判定性等等。正是基于这些优点，模态逻辑较好的平衡了语言的表达力和复杂性，在诸多不同领域里发挥了很大的作用。我们将对模态逻辑的这些良好性质进行细致的讨论。

注：本节课仅仅作为一个导言，如果对上述诸多名词概念不是很清楚请不必担心，我们将在后面的课程中放慢速度，仔细讲解。

补充：

2001年版Modal Logic教材的勘误表
提到的 $\text{[math]}$ 在线写作的网站：Overleaf.com，它上面也有一个30分钟教程，LaTeX相关系统性教程可参考这个文档.
An (Incomplete) Map of Logic，还在更新中，请勿传播
关于BNF形式的语法，关于context-free grammar。
关于计算复杂度（Computational complexity）
Googlism
逻辑灯谜1 逻辑灯谜2

大概内容（Contents）：

基础理论：模型与框架，正规模态逻辑，典范模型与完全性；表达力与不变性：互模拟，对应理论；有穷模型性与可判定性；代数语义学：表示定理，模态代数与一般框架；

(若有时间) 邻域语义学，非经典逻辑的克里普克语义, 一阶模态逻辑，模态逻辑的一些应用，模态逻辑与自动机的对应等。

本课的主题是模态逻辑, 但是也会介绍很多适用于逻辑学各种分支的问题和技术想法。无论你是否上过模态逻辑课或是否用过本课的教材，相信本课能带给你一些新的东西. 课堂上有超过三分之一的内容不在教材上, 由教师补充。

目标（Objectives）：

知识储备：知道模态逻辑的基本结果和重要定理的证明策略。
逻辑技能：对新的模态逻辑知道问什么问题并能解决一些，至少对问题难易程度及关键点有正确评估。
学术技能：熟练阅读英文教材及文献，能用 $\text{[math]}$ 写作业做slides，能独立清晰地做学术报告。
态度培养：一种看各种问题的“模态视角”，不畏惧复杂问题，愿意用逻辑工具形式化地分析问题，对学术问题具有较开放的心态。

教材（Course material）：

P. Blackburn, M. de Rijke and Y. Venema. Modal Logic, Cambridge University Press, 2001

参考书：
Handbook of Modal Logic, P. Blackburn, J. van Benthem, F. Wolter Eds. Elsevier, 2006
J. van Benthem. Modal Logic for Open Minds, CSLI Publications, 2010
R. Girle. Modal Logics and Philosophy (2 ed.), McGill-Queen’s, 2010
周北海，《模态逻辑导论》，北京大学出版社，1996
文学锋，《模态逻辑教程》，科学出版社，2021
Boxes and Diamonds: An Open Introduction to Modal Logic, Remixed by Richard Zach, 2020

考核（Grading）：
1. 作业（80%）：原则上两周一次，用 $\text{[math]}$ 写，挑成绩最好的 $n-1$ 次取平均分计入总成绩（ $nleq 7$ ）。
2. 当堂学术报告（20%）：补充内容

大致安排（Plan）：
第一周至十四周老师讲，第十五周同学分组报告

预备知识（Prerequisites）：
命题逻辑及一阶逻辑基本知识，模态逻辑的基础知识。

Office hours：
周四课后办公室2139，请提前预约。

意见、建议或其它问题请发email：y.wang艾特pku.edu.cn

Yanjing Wang

Department of Philosophy Peking University

Recent Posts

Advanced Modal Logic 2022