以MLp为公理的已知模态逻辑是否存在？（含符号定义及S7参考）

嘿，这个问题问得相当到位——确实存在以MLp作为公理的已知模态逻辑系统，它就是Lewis模态逻辑家族里的S8系统，和你提到的S7有着直接的关联！

让我拆解一下细节：

• 先回顾你说的S7：它是在Lewis的S3系统公理基础上，添加公理MMp（也就是“可能可能p”，等价于¬L¬Mp，直白点说就是“没有什么命题是必然不可能的”）得到的非正规模态 시스템。
• 而S8呢？它是在S3的框架下，把S7里的MMp替换成更强的MLp（“可能必然p”，等价于¬L¬Lp，即“不存在必然不必然的命题”）作为新增公理得到的。
• 从强度上看，MLp是比MMp更强的断言：因为模态逻辑里有定理Lp → Mp（必然p一定蕴含可能p），所以从MLp可以直接推出MMp，但反过来S7里的MMp没法推出MLp——这意味着S8是S7的真扩展，包含S7的所有定理，但还能得出更多结论。
• 从语义角度理解，MLp要求：对于任意命题p，至少存在一个可能世界，在这个世界里p是必然为真的。这比MMp的要求更严苛，后者只需要p有“可能的可能”，而前者要求p能达到“可能的必然”层级。

顺带提一句，S8和S7、S6都属于非正规模态系统，和我们更熟悉的S1-S5这类正规系统的核心区别是：它们不遵循“必然化规则”（也就是如果p是逻辑定理，那么Lp也自动成为定理），这类系统主要用来探索一些更边缘的模态直觉，比如允许“可能存在必然为真的命题，但这个必然性本身又是可能的”这类场景。

内容的提问来源于stack exchange，提问作者Justin