S5（模态逻辑）

在逻辑和哲学中，S5是克拉伦斯-欧文-刘易斯和库珀-哈罗德-兰福德在1932年的《符号逻辑》一书中提出的五个模态逻辑系统之一。它是一种正常的模态逻辑，也是任何一种模态逻辑中最古老的系统之一。它是用命题微积分公式和同义词形成的，推理装置有替换和模态，但用模态运算符扩展语法必然是

就克里普克语义而言，S5的特点是模型中的可及性关系是一种等价关系：它是反身的、转折的和对称的。确定一个S5公式的可满足性是一个NP-complete问题。硬度证明是微不足道的，因为S5包括命题逻辑。成员资格的证明是通过表明任何可满足的公式都有一个Kripke模型，其中世界的数量最多就是公式的大小的线性。应用S5是有用的，因为它避免了对不同种类的限定词进行多余的迭代。例如，在S5下，如果X是必然、可能、必然、可能是真的，那么X就可能是真的。在S5中，最后的"可能"之前的非折叠限定词被修剪掉。虽然这对保持命题的合理简短很有帮助，但它也可能显得反直觉，因为在S5下，如果某物可能是必要的，那么它就是必要的。

阿尔文-普兰丁格（AlvinPlantinga）认为，S5的这一特征事实上并不是反直觉的。为了证明这一点，他的理由是：如果X可能是必要的，那么它至少在一个可能的世界中是必要的；因此它在所有可能的世界中都是必要的，因此在所有可能的世界中都是真的。这种推理是本体论证的"模态"表述的基础。S5等同于邻接关系莱布尼茨用这个公理提出了一个关于上帝存在的本体论论证。用他的话说，如果一个必要的存在是可能的，那么它就会实际存在。S5也是圣人托马斯-阿奎那的形而上学的模态系统，特别是五种方法。