[科普中国]-S5模态逻辑

S5是Clarence Irving Lewis和Cooper Harold Langford在其1932年出版的“象征逻辑”一书中提出的五种模态逻辑系统之一。 它是一种普通的模态逻辑，是任何类型的最古老的模态逻辑系统之一。 是最基本的模态逻辑，是由命题演算公式和重言式构成的，以及具有替换和模态推理的推理装置。

克里普克的语义就Kripke语义而言，S5的特征在于可访问性关系是等价关系的模型：它是自反的，传递的和对称的。

确定S5公式的可满足性是NP完全问题。硬度证明是微不足道的，因为S5包括命题逻辑。通过证明任何可满足的公式具有Kripke模型来证明成员资格，其中世界的数量在公式的大小上最多是线性的。

应用S5很有用，因为它避免了不同种类的限定符的多余迭代。例如，在S5下，如果X必然，可能，必然，可能是真的，那么X可能是真的。最终“可能”之前的无限制资格赛在S5中被修剪。虽然这对于保持命题合理地缩短是有用的，但也可能看起来反直觉，因为在S5下，如果可能需要某些东西，那么这是必要的1。

Alvin Plantinga认为S5的这个特征实际上并不违反直觉。为了证明这一点，他认为如果X可能是必要的，那么至少在一个可能的世界中是必要的;因此，在所有可能的世界中都是必要的，因此在所有可能的世界中都是如此。这种推理支持了本体论论证的“模态”表述。

本词条内容贡献者为:

李嘉骞 - 博士 - 同济大学