报告基于 Kit Fine 等人证明某些传递逻辑有穷模型性问题时用到的方法，讨论包含宽度公式 In 的S4 正规扩充的有穷模型性问题。我们由特定 S4In 正规扩充的弱典范模型，通过 p-态射得到满足特定公式的有穷模型。在规约中我们发现所谓的 tough points 是构造有穷模型时遇到的难点。最后我们运用上诉方法证明，任意不包含无穷 tough 链的 S4In 正规扩充都具有有穷模型性。
Q：表示提问 A：表示回答 S：表示补充
王彦晶Q： 为什么对点生成的典范模型作操作的时候需要加新的关系？
李楷A：在本次报告中遇不到这种情况，但一般说来，如果考虑更加复杂的情况，如我硕士论文中的结论，则需要加入关系来保持特定的性质。
王彦晶Q：骨架框架的定义是否有些问题，是否需要保持其它关系不变？
李楷A：是的，slides上的定义不够完整，需要加上。
刘佶鑫Q：我们说Fine定理能说明S4的有穷宽度逻辑的框架都是诺特性的，而Grz的框架恰好也是诺特性的，是否说明这里Grz实质上和S4一样？
李楷A：Grz和S4依旧是不同的逻辑，但如果有有穷宽度的限制，那么从已知结论能得到有穷宽的S4和Grz的逻辑是相同的。可以尝试在内定理中证明这一点。
王彦晶Q：为什么我们考虑tough points时是考虑极大的那类点？
李楷A：极大的点需要保留到小的模型中。
刘壮虎Q：证据集是否需要要求诺特性才能取出，因为要求极大点？
李楷A：即使不是诺特性的框架，按照定义，可能证据集为空。
王彦晶Q：这个没有无穷tough chain的条件看上去比较奇怪，是否能说明哪些已知结论是这个结论的推论？
刘壮虎SQ：是否有具体的逻辑例子满足此条件？
李楷A：我们之所以考虑tough chain，是强调Fine这种模型方法所面对的困难，而这个条件也是可以削弱从而推广现有结论的，限于篇幅不好详述。我们的最终目标想办法刻画有穷模型性。具体的例子可以参考S4宽度为二的逻辑中的结论。
徐超Q：这个宽度公理的直观涵义不是特别清楚。
李楷A：嗯，具体证明其对应于宽度的性质比较繁琐，所以省略了。
刘壮虎S：这个公式本质是说N个后继中至少有2个相互可以比较。
徐超Q：这个策略图中的初始模型和最终模型具体是什么关系？
李楷A：我们从典范模型出发，经过操作，得到最终模型需要满足三个条件：有穷，L的模型，满足特定公式。
周北海S：(具体画图解释了每个步骤的操作过程。)
刘佶鑫Q：结论中的条件: 刻画框架中没有infinite tough chain框架，和L的框架中没有infinite tough chain，两者是否在这里是等价的？
李楷A：需要进一步思考，与主题关系也不大。
王彦晶Q：p-morphism存在的证明似乎不是很显然。
李楷A：这里为了方便省略了证明，但从之前的观察中能看出，出现的几种情况都显然可以用p-morphism压缩。
刘佶鑫S：需要说明出现的情况只有这几种。
李楷同学的报告是模态逻辑方面的内容，主要论述了如何利用Kit Fine的策略来证明一类有穷宽度的自返传递逻辑的有穷模型性，从而说明Fine的策略所具有的特点和限制，其中的关键在于一类特殊点的处理，李楷称之为tough points。有几点可以改进：
1、在时间分配上，似乎有些内容讲的过快，有些地方需要进一步说明的讲的有些粗略。
2、应该更加注重对报告主题的强调：重要的是方法以及其遇到的问题如何处理。
3、有一些输入上的笔误，还是应该尽量避免。
总的来说报告清楚明白，问题也解释的较为清楚，且是报告人自己的技术工作，希望能够更加考虑听众的背景，讲述的更加细致与直观。
报告总体上是比较好的，评论人的评论也不错，但两方面都有需要改进的地方。
报告的讲解方式应该更加考虑背景不是模态逻辑的听众，采用更加形象与直观的讲述方式，开头应该综述的更加细致。而评论人应该更加注重帮助报告人完善其讲的不够仔细的地方，帮助听众深入的理解报告内容。报告中对于tough chain这一关键概念的说明需要更加直观和具体，最好加入例子来说明这种框架和逻辑的特殊性。
综合来看，报告的核心内容是报告人自己的工作，而且是技术方面的工作，对于模态逻辑研究也有一些推进作用，所以总的说来是值得肯定和大家借鉴的报告形式与内容，但细节上海要做的更好，主要是多考虑别的研究方向的听众的背景。
slidestemplate145691638989.pdf