报告首先从ZF给出了刻划GL的更准确的框架类，其次运用Kit Fine的方法给出了一类时态传递逻辑的完全性，最后给出了一类时态GL逻辑的有穷模型性。
Q：表示提问 A：表示回答 S：表示补充
王彦晶Q：时态逻辑中谈两个方向的GL为何无法保证一般情况下的有穷模型性？
刘佶鑫A：的确用GL解释未来时会有点反直观。无法保证的有穷模型性是因为我们应该可以构造宽度为2的不可规约的无穷模型。而过去的.3是用来避免一类特殊的无穷模型的出现。
刘壮虎Q：K1 和 K2 不等价的模型是在ZFA中，那是否有ZF中有类似的模型？
刘佶鑫A：利用Jech-Sochor定理可以把一个ZFA模型嵌入到一个ZF模型中，并且这种嵌入在一定序数之下保持同构，也就是可以保持一定序数以下的真理，故ZF中也有K1,K2的不等价模型。
高 珂Q：为何关于K1 和 K2 不等价的模型考虑的时序数的情形，而不是基数的情形？
刘佶鑫A：Jech定理告诉我们ZFA到ZF的嵌入可以保持任意大的序数片段，当然也可以保持任意大的基数片段，只是不能保持全局性的信息。
整个报告总的来说，思路清晰，讲得浅显易懂。刘佶鑫将技术证明背后的直观用比较清楚的方式表达出来，并从是否运用选择公理角度讨论模态逻辑证明。可惜的是，本次报告的技术结果不如 Kit Fine 关于宽度有穷的传递逻辑结果漂亮，并且报告中有以下问题：
1、报告时间安排可以提高；
2、报告并没有介绍更新的关于模态逻辑有穷模型性的技术。
